isDefEq failing on unifiable types

Stream: lean4

[Jeremy Salwen]

See the following MWE:

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Lean.Meta.Simp
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def upLemma (f : Expr) : MetaM Expr := do
 let template ← mkArrow (mkApp (mkConst ``List []) (← mkFreshTypeMVar)) (← mkFreshTypeMVar)
 logInfo (← inferType f)
 logInfo template
 if ¬ (← isDefEq (← inferType f) template) then
      throwError "Failed isDefEq"
 pure f

elab "upLemma% " f:term : term => do
  upLemma (← elabTerm f none)

def z := upLemma% List.toArray

the `isDefEq is failing, despite the types looking equal to me, after unification:

List ?m.4500 → Array ?m.4500
List ?m.4801 → ?m.4803

Maybe this is universe related? Both metavariables in the first expression are of typeType, but the metavariables in the second expression are of type Sort?

[Henrik Böving]

How do these types look unifiable to you at all? One is a function from List the other is a function from Nat

[Jeremy Salwen]

Ah, apologies, I introduce that mistake when minimizing the example, let me fix it.

[Jeremy Salwen]

Ok, fixed it.

[Gabriel Ebner]

mkConst ``List [] does not type check because it's missing a universe parameter. It should be mkConst ``List [u].

[Jeremy Salwen]

Ah ok, again it was a failure of minimizing the example. Here is something much closer to my original code. The weird behavior is that ftype will not unify with template2 (the actual thing I am trying to fix), but it will unify with template1, however, template1 will unify with template2. So isDefEq is not behaving transitively?

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Lean.Meta.Simp
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def upLemma (f w : Expr) : MetaM Expr := do
 mapForallTelescope' (fun ty e => do
  match ty.getAppFnArgs with
  | (``Eq, #[α, _, _]) => do
    let ftype ← inferType f
    let template1 ← mkArrow (mkApp (mkConst ``List [← mkFreshLevelMVar]) (← mkFreshTypeMVar)) (← mkFreshTypeMVar)
    let template2 ← mkArrow α (← mkFreshTypeMVar)

    if ¬ (← isDefEq ftype template2) then
      throwError "Failed to unify"
    pure e
  | x => throwError ""
 ) w

elab "upLemma% " f:term " x " e:term: term => do
  upLemma (← elabTerm f none) (← elabTerm e none)

def z := upLemma% List.toArray x @Array.push_data

[Jeremy Salwen]

I'm investigating some more, and I realize that this is probably related to mapForallTelescope' turning the universe parameter to Array.push_data into a concrete parameter, which may be causing weirdness. I'm going to investigate further.

[Jeremy Salwen]

Ok, I think what is going on is that it is refusing to unify a metavariable with a free variable. Here is my MWE:

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Lean.Meta.Simp
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic
def upLemma (f : Expr) : MetaM Expr := do
  withLocalDecl `α BinderInfo.default (mkSort levelOne) (λ x => do
    let listTypeMetavar := f.getAppArgs[0]!
    logInfo listTypeMetavar
    logInfo x
    if ¬ (← isDefEq listTypeMetavar x) then
      throwError "wtf"
    pure (mkConst ``Nat [])
 )

elab "upLemma% " f:term : term => do
  upLemma (← elabTerm f none)

def z := upLemma% List.toArray

listTypeMetavar will happily unify with Nat, but it won't unify with α. I am not 100% sure what is going on here, but it seems like the problem is that the metavariable was introduced too early, so it cannot depend on free variables that were introduced later.

So I need to replace my metavariable in f with a fresh metavariable for this to work?

[Jeremy Salwen]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.E2.9C.94.20Unification.20with.20.60isDefEq.60
seems to confirm that this is not allowed.

I was looking for a helper function in mathlib to substitute metavariables with fresh ones., but couldn't find it. Does something like this exist?

[Jeremy Salwen]

Ok, I seem to have fixed it! I had to write the helper function to refresh the metavariables` myself:

import Lean
import Std.Data.Array.Init.Lemmas
import Mathlib.Lean.Meta.Simp
import Lean.Elab.Term

open Lean Meta Elab Term Lean.Meta Tactic

def replaceRecM [Monad M] [MonadLiftT MetaM M] [MonadControlT MetaM M] (f? : (Expr → M Expr) → Expr → M (Option Expr)) : Expr → M Expr
  | expr => do
    memoFix (fun r e ↦  do
      match ← f? r e with
      | some x => pure x
      | none   => traverseChildren (M := M) r e) expr


partial def replaceMvarsWithFreshMVars: Expr → MetaM Expr :=
  replaceRecM (λ _ term => do
    match term with
    | .mvar id => some <$> (mkFreshExprMVar (← id.getType))
    | _ => pure none
  )

def upLemma (f w : Expr) : MetaM Expr := do
 mapForallTelescope' (fun ty e => do
  let fnew ← replaceMvarsWithFreshMVars f
  match ty.getAppFnArgs with
  | (``Eq, #[α, _, _]) => do
    let ftype ← inferType fnew
    let template1 ← mkArrow (mkApp (mkConst ``List [← mkFreshLevelMVar]) (← mkFreshTypeMVar)) (← mkFreshTypeMVar)
    let template2 ← mkArrow α (← mkFreshTypeMVar)

    if ¬ (← isDefEq ftype template2) then
      throwError "Failed to unify"
    pure e
  | x => throwError ""
 ) w


elab "upLemma% " f:term " x " e:term: term => do
  upLemma (← elabTerm f none) (← elabTerm e none)

def z := upLemma% List.toArray x @Array.push_data

[Jannis Limperg]

I'm a bit suspicious of this solution. Why can't you create the mvar with the correct local context (i.e. such that it has access to all relevant local variables) in the first place?

[Jeremy Salwen]

Jannis Limperg said:

I'm a bit suspicious of this solution. Why can't you create the mvar with the correct local context (i.e. such that it has access to all relevant local variables) in the first place?

In this case it was due to the metavariables being created outside of the function call. I can simplify things later, I just wanted to verify that I was actually understanding the cause of the failure.

[Jannis Limperg]

Fair. Your diagnosis seems correct to me. You can verify it by inspecting the local contexts of the mvars, which contain exactly the fvars which can be used in expressions assigned to the mvars.