Type inference failure

Stream: lean4

[Jovan Gerbscheid]

I encountered a piece of code where I believe Lean should be able to infer the types, but it isn't able to. Here's a minimised version:

def f (a : α) : α := Id.run do
  let (b) ←
    (fun _ => do
      if true then pure () else pure ()
      return a
      ) ()
  -- invalid match-expression, type of pattern variable 'b' contains metavariables
  -- ?m.494
  return b

It can be fixed by removing the brackets around b, because with the brackets it is interpreted as a pattern, but this fix doesn't work if you're working with a non-trivial pattern like this:

def f (a : α) : α := Id.run do
  let (b, _) ←
    (fun _ => do
      if true then pure () else pure ()
      return (a,a)
      ) ()
  return b

[Eric Wieser]

This works fine:

def f (a : α) : α := Id.run do
  let (b) ← do
    if true then pure () else pure ()
    pure a
  return b

[Jovan Gerbscheid]

I went a bit far with minimizing the example, what about this:

def f (a : α) (A : Array Unit) : Option α := do
  let (b) ← A.foldr (init := none) fun _ x => (do
    if true then pure () else pure ()
    return a
    ) <|> x
  return b

[Jovan Gerbscheid]

By the way, the problem can be solved by writing an extra type annotation somewhere, but it is quite frustrating to get an error message and to need to "fix" a piece of code when it is perfectly valid.

[Kyle Miller]

Weird, adding a variable line gets rid of the error, and adding {α : Type _} as an extra argument doesn't suffice.

variable {α : Type _}

def f (a : α) (A : Array Unit) : Option α := do
  let (b) ← A.foldr (init := none) fun _ x => (do
    if true then pure () else pure ()
    return a
    ) <|> x
  return b

[Eric Wieser]

(not that it's really {α : Type} here, since the Unit forces everything to live in Type 0)

[Jovan Gerbscheid]

Here is another type inference failure, this time in the presence of a type class diamond, which causes trySynthInstance to return .none instead of .undef. This causes the expected type to not be propagated properly.

class AA (α : Type) where
  asNum : α → Nat
  p : α → Prop

class AB (α : Type) extends AA α
class BA (α : Type) extends AA α
class BB (α : Type) extends AB α, BA α

class X (α : Type) (f : α → Nat)

instance [AB α] : X α AA.asNum where

theorem X_rfl [BA α] [X α AA.asNum] {a : α} : AA.p a ↔ AA.p a := Iff.rfl

/-
failed to synthesize instance
  X ?m.234 AA.asNum
-/
example {α : Type} [BB α] (a : α) : AA.p a → AA.p a := X_rfl.mpr