Need help converting code from 4.3.0 to 4.26.0

Stream: new members

[Kevin Cheung]

I'm new to metaprogramming. I am trying to update some code written for 4.3.0 to 4.26.0. Below is the smallest example I could come up with that illustrates my problem:

import Mathlib.Tactic.Linarith

open Lean.Meta Qq Mathlib.Meta.NormNum

def foo (n : ℤ) : Prop := n = 2

@[norm_num foo _ ] def evalFoo : NormNumExt where eval (e : Q(Prop)) := do
  let .app f (n : Q(ℤ)) ← whnfR e | failure
  guard <|← withNewMCtxDepth <| isDefEq f q(foo)
  let rn : Result n ← derive n
  let i : Q(Ring ℤ) := q(Int.instRingInt)
  let ⟨zn, _, _⟩ ← rn.toInt
  sorry

Lean 4.3.0 was happy with the above, just highlighting the sorry as a warning.

My attempt to make it work in 4.26.0 first made me change Int.instRingInt to Int.instRing:

import Mathlib.Tactic.Linarith

open Lean.Meta Qq Mathlib.Meta.NormNum

def foo (n : ℤ) : Prop := n = 2

@[norm_num foo _ ] def evalFoo : NormNumExt where eval (e : Q(Prop)) := do
  let .app f (n : Q(ℤ)) ← whnfR e | failure
  guard <|← withNewMCtxDepth <| isDefEq f q(foo)
  let rn : Result n ← derive n
  let i : Q(Ring ℤ) := q(Int.instRing)
  let ⟨zn, _, _⟩ ← rn.toInt
  sorry

However, Lean 4.26.0 now gives an error right before sorry:

Type mismatch
  Result.toInt ?m.60 rn
has type
  Option (ℤ × (lit : Q(ℤ)) × Q(IsInt «$n» «$lit»))
but is expected to have type
  MetaM ?m.56

I cannot figure out what is wrong since the error is not present in the 4.3.0 version. Help greatly appreciated.

[Aaron Liu]

Do you understand what the error message is saying?

[Kevin Cheung]

I know there is a type mismatch. toInt is returning something that is not MetaM something.

[Kevin Cheung]

Otherwise, I'm baffled because I don't understand how the code could possibly work in 4.3.0.

[Aaron Liu]

Do you know what MetaM is?

[Kevin Cheung]

Only vaguely. It's a monad.

[Aaron Liu]

  let ⟨zn, _, _⟩ ← rn.toInt

In this snippet I can see that you are pulling out three elements from rn.toInt, which should be returning a monadic computation since we have the ← which means to run a monadic computation.

[Kevin Cheung]

Right. But somehow that was legal in 4.3.0.

[Aaron Liu]

From the error message I can see the actual type of rn.toInt is

  Option (ℤ × (lit : Q(ℤ)) × Q(IsInt «$n» «$lit»))

[Aaron Liu]

so there are still three values in there, but they are not behind a monadic computation anymore

[Aaron Liu]

instead, it's just an Option

[Kevin Cheung]

I just tried Gemini. It suggests let some ⟨zn, _, _⟩ := rn.toInt | failure

[Aaron Liu]

yes, that's what I would have suggested too

[Kevin Cheung]

So 4.3.0 must be doing something weird.

[Aaron Liu]

so probably what happened is that at some point the function was changed from being monadic to returning an Option value

[Aaron Liu]

and the reason your old code failed is because you are still using ← with your let which means "run this monadic computation and get the value out"

[Aaron Liu]

and that failed because rn.toInt isn't a monadic computation anymore

[Kevin Cheung]

I see.

[Kevin Cheung]

This is what I found in the old code:

def Result.toInt {α : Q(Type u)} {e : Q($α)} (_i : Q(Ring $α) := by with_reducible assumption) :
    Result e → Option (ℤ × (lit : Q(ℤ)) × Q(IsInt $e $lit))

[Kevin Cheung]

Doesn't seem monadic here.

[Aaron Liu]

then, I guess the other option is that there could've been a coercion to interpret a value of type Option as a MetaM computation, and this coercion was turned off

[Kevin Cheung]

I see. In any case, looks like my problem is solved. With the change, things seem to work now. Thanks.