Segfault with monad inference

[digama0]

Prerequisites

• [X] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The following code produces a segfault:

meta def M1 := state_t unit tactic
meta def F (n : name) : M1 unit := sorry
meta def M2 := state_t unit tactic

meta instance : monad M2 := state_t.monad
meta instance : has_monad_lift M1 M2 :=
⟨λ α ⟨c⟩, ⟨λ tr, do a ← c (), return a⟩⟩

meta def T : M2 unit := monad_lift (F n) >>= _

[PS: Not sure if this qualifies as a bug worth fixing since 3.4 is frozen. Feel free to ignore or fix only in lean 4.]

Versions

Lean v3.4.0 (dd6e91f)