Typing Error with Option Monad

Stream: new members

[Arjun Viswanathan]

I have a function that looks like this, which is well-typed in Lean:

def test : option ℕ → option ℕ :=
  λ on₁, do n₁ ← on₁, some n₁

I have a similar one, that is ill-typed:

def test2 : option ℕ → list ℕ :=
  λ on₁, do n₁ ← on₁, [n₁]

For test2, Lean complains with:

type mismatch at application
  bind on₁
term
  on₁
has type
  option ℕ
but is expected to have type
  list ℕ

Why is on₁ expected to have type list ℕ, instead of option ℕ? As far as I can understand, on₁ is the input of type option ℕ, and I'm returning [n₁] which is the output of type list ℕ. Any help would be appreciated.

[Yakov Pechersky]

In your test2, once you start the do n₁ ← on₁, that is expected to return an list nat, since the first bind is on an list nat

[Yakov Pechersky]

Because you told lean that the function will return a list

[Yakov Pechersky]

Let's say that lean inferred the type based on the argument on the left side of the arrow. Then where does your option go? Once you'd be in the option monad, your output value would be of type option (list nat) (if you did pure [n1])

[Yakov Pechersky]

docs#option.to_list to see an example without using do

[Arjun Viswanathan]

Makes sense that I'd need an option (list nat) now, thanks!