You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
When I implement pure and bind of Monad, I get a missing fields error, prompting me to implement map, mapConst, seq, seqLeft as well.
If I extract the code for bind, the error goes away.
-------------------------------------------
-- Guarded recursion and the Later modality
universe u v
axiom Later : Sort u → Sort u
axiom next {α : Sort u} (a : PUnit → α) : Later α
axiom ap {α β : Sort u} (f : Later (α → β)) (a : Later α) : Later β
axiom gfix {α : Sort u} (f : Later α → α) : α
axiom DLater : Later (Sort u) → Sort u
axiom DLater.next_eq {α : Sort u} : Later α = DLater (next (fun () => α))
----------------------------------------
-- Repro
inductive T.F (α : Type u) (τ : Later (Type u)) : Type u where
| ret : α → T.F α τ
| step : DLater τ → T.F α τ
def T α := gfix (T.F α)
theorem T.unfold : T α = T.F α (next (fun () => T α)) := sorry
def T.ret (x : α) : T α := sorry
def T.step (tl : Later (T α)) : T α := sorry
instance : Monad T where
pure := T.ret
bind {α β} t k :=
let loop loop' t : T β := match cast T.unfold t with
| .ret a => k a
| .step tl => T.step (ap loop' (cast DLater.next_eq.symm tl))
gfix loop t
Expected behavior: No error.
Actual behavior: An error in the instance : Monad T where line:
Now extract the RHS of bind into a separate definition:
noncomputable def T.bind {α β} (t : T α) (k : α → T β) : T β :=
let loop loop' t : T β := match cast T.unfold t with
| .ret a => k a
| .step tl => T.step (ap loop' (cast DLater.next_eq.symm tl))
gfix loop t
noncomputable instance : Monad T where
pure := T.ret
bind := T.bind
No error, as expected. (noncomputable is needed because I omitted several definitions in the reproducer.)
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
When I implement
pure
andbind
ofMonad
, I get a missing fields error, prompting me to implementmap
,mapConst
,seq
,seqLeft
as well.If I extract the code for
bind
, the error goes away.Steps to Reproduce
Check this file (live.lean-lang.org):
Expected behavior: No error.
Actual behavior: An error in the
instance : Monad T where
line:Now extract the RHS of
bind
into a separate definition:No error, as expected. (
noncomputable
is needed because I omitted several definitions in the reproducer.)Versions
4.10.0-rc2
Windows + live.lean-lang.org
Impact
Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: