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)