stray metavariable in goal, looks like a bug?

Stream: lean4

[Kim Morrison]

def SatisfiesM {m : Type u → Type v} [Functor m] (p : α → Prop) (x : m α) : Prop :=
  ∃ x' : m {a // p a}, Subtype.val <$> x' = x

/-- A monad is "satisfying" if we can lift `SatisfiesM` to a monadic value in `Subtype`. -/
class Satisfying (m : Type u → Type v) [Monad m] where
  lift (p : α → Prop) (x : m α) (h : SatisfiesM (m := m) p x) :
    { y : m {a // p a} // Subtype.val <$> y = x }

instance : Satisfying Option where
  lift (p) x? h :=
  { val := x?.attach.map fun ⟨x, w⟩ => ⟨x, by
      obtain ⟨a?, rfl⟩ := h
      match a? with
      | none => simp at w
      | some a =>
        simp at w
        simp [← w]
        exact a.2⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp } -- Why is there a metavariable in the goal???

At the final simp I see a goal of the form ⊢ (?m.651 (some x) h ⟨x, ⋯⟩).val = x, i.e. with a stray metavariable. This is a bug, right?

I can work around this by extracting out the value of val into a helper function.

[Daniel Weber]

Even just extracting the proof in val to another function works, but using by exact doesn't:

def SatisfiesM {m : Type u → Type v} [Functor m] (p : α → Prop) (x : m α) : Prop :=
  ∃ x' : m {a // p a}, Subtype.val <$> x' = x

/-- A monad is "satisfying" if we can lift `SatisfiesM` to a monadic value in `Subtype`. -/
class Satisfying (m : Type u → Type v) [Monad m] where
  lift (p : α → Prop) (x : m α) (h : SatisfiesM (m := m) p x) :
    { y : m {a // p a} // Subtype.val <$> y = x }

theorem extracted_1.{u_1} {α : Type u_1} (p : α → Prop) (x? : Option α) (h : SatisfiesM p x?) (x : α) (w : x ∈ x?) :
    p x := by
  obtain ⟨a?, rfl⟩ := h
  match a? with
  | none => simp at w
  | some a =>
    simp at w
    simp [← w]
    exact a.2

instance : Satisfying Option where
  lift (p) x? h :=
  { val := x?.attach.map fun ⟨x, w⟩ => ⟨x, extracted_1 p x? h x w⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp } -- Works

instance : Satisfying Option where
  lift (p) x? h :=
  { val := x?.attach.map fun ⟨x, w⟩ => ⟨x, by exact extracted_1 p x? h x w⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp } -- Why is there a metavariable in the goal???

[Daniel Weber]

I think it's because by delays elaboration, so val isn't fully determined when you prove property

[Daniel Weber]

Minimized:

def lift (p : α → Prop) (x? : Option α) : { y : Option {a // p a} // Subtype.val <$> y = x? } :=
  { val := x?.attach.map fun ⟨x, w⟩ => ⟨x, sorry⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp } -- OK

def lift2 (p : α → Prop) (x? : Option α) : { y : Option {a // p a} // Subtype.val <$> y = x? } :=
  { val := x?.attach.map fun ⟨x, w⟩ => ⟨x, by sorry⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp } -- Why is there a metavariable in the goal???

[Kim Morrison]

(Just did some poking around, this has always been a problem, it's not a regression.)

[Kyle Miller]

It seems like it could have to do with the implicit match in that fun definition postponing things as well. Using projection notation is a way to fix it:

def lift3 (p : α → Prop) (x? : Option α) : { y : Option {a // p a} // Subtype.val <$> y = x? } :=
  { val := x?.attach.map fun x => ⟨x.1, by sorry⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp }

[Kyle Miller]

instance : Satisfying Option where
  lift (p) x? h :=
  { val := x?.attach.map fun x => ⟨x.1, by
      have w := x.2
      obtain ⟨a?, rfl⟩ := h
      match a? with
      | none => simp at w
      | some a =>
        simp at w
        simp [← w]
        exact a.2⟩
    property := by
      cases x? with
      | none => simp
      | some x => simp }