Unification failure in simp

Stream: lean4

[Tomas Skrivan]

I'm having a trouble figuring out why one simp theorem is not being applied. There is unification failure and I'm having hard time reading the trace.

The main unification that fails is:

      [Meta.isDefEq] ❌ fun (i : Fin 10 × Unit) =>
            (?inst : (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i))
              i.2 =?= fun (i : Fin 10 × Unit) => NonUnitalNormedRing.toNormedAddCommGroup

Here is the part of the trace corresponding to this failure

trace

      [Meta.isDefEq] ❌ fun (i : Fin 10 × Unit) =>
            (?inst : (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i))
              i.2 =?= fun (i : Fin 10 × Unit) => NonUnitalNormedRing.toNormedAddCommGroup
        [Meta.isDefEq] ✅ Fin 10 × Unit =?= Fin 10 × Unit
        [Meta.isDefEq] ❌ (?inst : (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i))
              i.2 =?= NonUnitalNormedRing.toNormedAddCommGroup
          [Meta.isDefEq] (?inst : (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i))
                i.2 [assignable] =?= NonUnitalNormedRing.toNormedAddCommGroup [nonassignable]
          [Meta.isDefEq.foApprox] (?inst :
                (i : (?I : Type)) →
                  NormedAddCommGroup ((?EI : (?I : Type) → Type) i)) [i.2] := NonUnitalNormedRing.toNormedAddCommGroup
          [Meta.isDefEq] ❌ i.2 =?= NonUnitalNormedCommRing.toNonUnitalNormedRing
            [Meta.isDefEq] ❌ i.2 =?= NonUnitalNormedCommRing.toNonUnitalNormedRing
              [Meta.isDefEq] ❌ i.2 =?= NormedCommRing.toNonUnitalNormedCommRing.1
                [Meta.isDefEq] ❌ i.2 =?= NonUnitalNormedRing.mk ⋯ ⋯
                  [Meta.isDefEq] ❌ Unit =?= NonUnitalNormedRing R
                    [Meta.isDefEq] ❌ Unit =?= NonUnitalNormedRing R
                      [Meta.isDefEq] ❌ PUnit.{1} =?= NonUnitalNormedRing R
                        [Meta.isDefEq.onFailure] ❌ PUnit.{1} =?= NonUnitalNormedRing R
                  [Meta.isDefEq] ❌ PUnit.{1} =?= NonUnitalNormedRing R
                  [Meta.isDefEq.onFailure] ❌ i.2 =?= NonUnitalNormedRing.mk ⋯ ⋯
          [Meta.isDefEq.foApprox] (?inst :
                (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i)) [i.2] := NormedAddCommGroup.mk ⋯
          [Meta.isDefEq] ❌ i.2 =?= NonUnitalNormedRing.dist_eq
            [Meta.isDefEq] ❌ i.2 =?= NonUnitalNormedRing.dist_eq
              [Meta.isDefEq] ❌ PUnit.{1} =?= ∀ (x y : R), dist x y = ‖x - y‖
                [Meta.isDefEq.onFailure] ❌ PUnit.{1} =?= ∀ (x y : R), dist x y = ‖x - y‖
              [Meta.isDefEq.onFailure] ❌ i.2 =?= NonUnitalNormedRing.dist_eq
          [Meta.isDefEq.constApprox] (?inst :
                (i : (?I : Type)) →
                  NormedAddCommGroup ((?EI : (?I : Type) → Type) i)) [i.2] := NonUnitalNormedRing.toNormedAddCommGroup
          [Meta.isDefEq.foApprox] (?inst :
                (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i)) [i.2] := NormedAddCommGroup.mk ⋯
          [Meta.isDefEq] ❌ i.2 =?= NonUnitalNormedRing.dist_eq
          [Meta.isDefEq.constApprox] (?inst :
                (i : (?I : Type)) → NormedAddCommGroup ((?EI : (?I : Type) → Type) i)) [i.2] := NormedAddCommGroup.mk ⋯

Here is a minimized version of the unification itself

import Mathlib

open Lean Meta Qq in
#eval show MetaM Unit from do

  let I? ← mkFreshExprMVarQ q(Type)
  let EI? ← mkFreshExprMVarQ q($I? → Type)
  let inst? ← mkFreshExprMVarQ q((i : $I?) → NormedAddCommGroup.{0} ($EI? i))
  let lhs :=
    Expr.lam `i q(Fin 10 × Unit) (inst?.app (Expr.app q(Prod.snd : Fin 10 × Unit → Unit) (.bvar 0))) default


  withLocalDeclQ `R default q(Type) fun R => do
  withLocalDeclQ `R .instImplicit q(RCLike $R) fun instR => do
  let rhsBody := q(inferInstance : NormedAddCommGroup $R)
  let rhs := q(fun (i : Fin 10 × Unit) => $rhsBody)

  -- I?.mvarId!.assignIfDefeq q(Unit)
  -- EI?.mvarId!.assignIfDefeq q(fun _ : Unit => $R)
  -- inst?.mvarId!.assignIfDefeq q(fun _ : Unit => $rhsBody)

  if ← isDefEq lhs rhs then
    IO.println "unification succeeded"
  else
    throwError "unification failed"

If you uncomment all the assignIfDefeq i.e. assign the metavariables manually then the final defeq test succeeds.

I would like this unification to succeed. How can I achieve that? Can I write an unification hint?

Ideally I would not run into this problem at all, but I'm unable to minimize the simp call :( I'm thinking that reordering the simp theorem arguments might cause different unification order. Any other tip would be welcome.