Fields missing error while defining Monad

Stream: new members

[Ichinoe]

I'm learning Monad Operations of Functional Programming in Lean, and writing codes like this:

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

instance : Monad <| WithLog logged where
  pure val := ⟨[], val⟩
  bind item next :=
    let nextItem := next item.val
    ⟨item.log ++ nextItem.log, nextItem.val⟩

and it says fields missing: 'map', 'mapConst', 'seq', 'seqLeft'.

But if I write as what the textbook does, there would be no error:

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

instance : Monad <| WithLog logged where
  pure val := ⟨[], val⟩
  bind item next :=
    let {log := nextOut, val := nextRes} := next item.val
    ⟨item.log ++ nextOut, nextRes⟩

Why is this happening? I found a similar post but it doesn't seems to be of help to this problem.

[Yuyang Zhao]

#mwe

def Option' := Option

instance : Monad Option' where
  pure := Option.some
  bind a f :=
    let b := Option.bind a f
    b

[Yuyang Zhao]

It looks like let makes Lean fail to assign default values to fields.

[Utensil Song]

It's weird that the following works despite that it didn't use let destructuring:

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α

set_option trace.Meta.synthInstance true
set_option synthInstance.checkSynthOrder true

instance : Pure <| WithLog logged where
  pure val := ⟨[], val⟩

instance : Bind <| WithLog logged where
  bind item next :=
    let nextItem := next item.val
    ⟨item.log ++ nextItem.log, nextItem.val⟩

/-
failed to synthesize
  Monad (WithLog logged)
-/
variable (logged : Type) in
#synth Monad <| WithLog logged

-- empty body works
instance : Monad <| WithLog logged where

-- success
variable (logged : Type) in
#synth Monad <| WithLog logged

[Utensil Song]

or the shorter working version for @Yuyang Zhao 's (intentially) non-working #mwe:

def Option' := Option

instance : Pure Option' where
  pure := Option.some

instance : Bind Option' where
  bind a f :=
    let b := Option.bind a f
    b

instance : Monad Option' where

[Yuyang Zhao]

I think Bind is already defined in this example when defining Monad (and then assigning default values to its fields). It will not be expanded to a let expression.

[Utensil Song]

def Option' := Option

instance : Monad Option' where
  pure := Option.some
  bind := fun a f =>
    let rec b := Option.bind a f
    b

let rec works, for both #mwe and the original example.

[Utensil Song]

But why doesn't this further minimized #mwe fail with let?

class A (t : Type) where
  a : t → t

class B (t : Type) extends A t where
  b : t → t

class C (t : Type) extends B t where
  b := fun x ↦ A.a x

structure D (t : Type) where
  d : t → t

instance : C <| D t0 where
  a := fun x ↦
    let xd := x.d
    ⟨xd⟩

[Utensil Song]

I want to note that this case is still a mystery to me. let, let rec and let fun are implemented in very different ways despite the syntax similarity, so even though I suspect the issue is in the let implementation, I have no clue.

[Mario Carneiro]

let fun doesn't exist

[Mario Carneiro]

oh you mean let_fun

[Mario Carneiro]

which is basically the same as have

[Mario Carneiro]

What's the issue in the above code? I get no errors, and it sounds like this is expected

[Utensil Song]

The issue is with the #mwe in the 2nd message.

As it seems that let makes Lean fail to assign default values to fields.

Comparing that with this:

def Option' := Option

instance : Monad Option' where
  pure := Option.some
  bind := Option.bind

which would work without the error about missing fields.

[Arthur Adjedj]

This is lean4#3146, fixed in lean4#3152.

[Utensil Song]

Thanks for the fix!

The fix looks subtle to me, as the original code looks innocent and aligns with other match branches. Is it possible that the issues applies to not only let and the cause is rooted somewhere else where this lingering of metavariables could be treated altogether for all applied constructs?

[Arthur Adjedj]

I'm not sure I understand what you're proposing. What causes the metavariables to linger in the first place is that reduce, which serves (among other things) to instantiate metavariables doesn't do so in the subexpressions bound in lets. Because the system relies on checking whether there are still some unsolved metavars to know whether default fields have been effectively elaborated, this looks like the most sensible solution to me.

[Arthur Adjedj]

Though now that I think about this again, it might be possible to find such lingering mvars in the type of variables in the local context, and not just in their values. I believe I couldn't manage to trigger an error in such situations when testing back when I made my PR, but I might as well take another look.

[Utensil Song]

Yes, the fix is sensible for fixing the let issue. My concern was merely that the other match branches are only doing a mk...reduce combo, is it that let is special, or other branches might need the same treatment for the metavariables.

[Arthur Adjedj]

let is special in that it is the only branch which introduces a new term (and its type) in the local context, the other special cases would be lambda and forall, which introduce new types in the local context

[Utensil Song]

(deleted)

[Utensil Song]

I see, thanks for the explanation.