Segfault with monad inference - Githubissues

leanprover / lean3

Lean Theorem Prover

http://leanprover.github.io/

Apache License 2.0

2.15k stars 217 forks source link

Segfault with monad inference #1958

Open digama0 opened 6 years ago

digama0 commented 6 years ago

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)