Crash related to add_ginductive

Reported by @CohenCyril on Zulip. This code (which relies on the add_ginductive hook added in #3), crashes the latest nightly:

open expr tactic

run_cmd do
  let ty : expr := sort level.zero,
  updateex_env $ λe,
    e.add_ginductive options.mk [] [ty] [(("test", ty), [])] ff

This assert:

https://github.com/leanprover-community/lean/blob/014fd370b128a20076fa4fdb743829fbe01f40ce/src/kernel/abstract.cpp#L33

fails when running the debug build. The backtrace indicates that it results from this:
https://github.com/leanprover-community/lean/blob/014fd370b128a20076fa4fdb743829fbe01f40ce/src/library/vm/vm_environment.cpp#L142-L144
(I'm still using lldb so I can't provide too much more info on the variables.)

The following is fine (deleting the first ty from the final line):

open expr tactic

run_cmd do
  let ty : expr := sort level.zero,
  updateex_env $ λe,
    e.add_ginductive options.mk [] [] [(("test", ty), [])] ff

Reproduce the supplied add_ginductive example in a debug build, comparing it with the working variant that omits the first ty. Start at the assertion in src/kernel/abstract.cpp:33 and inspect the environment handling at src/library/vm/vm_environment.cpp:142-144. Done means the failing example no longer crashes while the working case remains valid.