MetaM and Option

Stream: mathlib4

[Damiano Testa]

Dear All,

I was confused by the behaviour below. Lean seems to first accept something and then rejects it as failed.

import Mathlib.Tactic.NormNum.Basic
open Lean

--  What seems to be the culprit instance
#synth MonadLift Option MetaM

--attribute [-instance] Mathlib.Meta.NormNum.instMonadLiftOptionMetaM

def ex (b : Bool) : MetaM (Option Expr) := do
if b then
  return some default  -- note the `return` on `some`
else
  none  --note just the `none` with no `return`

#eval do -- some (Lean.Expr.bvar 0)
  ex true

#eval do -- failed
  ex false

I believe that the failure should have happened earlier, at the none with no return. Unsetting the instance, Lean does indeed fail at the else none, complaining about a type mismatch.

Anyway, as I do not really understand what the instance is doing, I am happy to leave this as is. However, if someone is willing to explain what is going on, I would be very grateful!

Thanks!

[Eric Wieser]

The none here is being cast to failure

[Eric Wieser]

I think #print ex should make that more obvious

[Damiano Testa]

Ah, ok, looking at #print explains what you said. I tried replacing none with default, but then the effect is that the error message disappears, while the error stays.

Anyway, thank you for the explanation. I hope that I will realise more quickly, next time that I forget to write a return and later I get failure messages! :upside_down:

[Damiano Testa]

For completeness:

#print ex
/-
def ex : Bool → MetaM (Option Expr) :=
fun b ↦ if b = true then pure (some default) else liftM none
-/