feat: make sure MetaM also implements new unifier approximation

src/Init/Lean/Meta/Basic.lean

@@ -59,10 +59,14 @@ end TransparencyMode
 
 structure Config :=
 (opts               : Options := {})
--- TODO: merge all *Approx flags.
 (foApprox           : Bool    := false)
 (ctxApprox          : Bool    := false)
 (quasiPatternApprox : Bool    := false)
+/- When `constApprox` is set to true,
+   we solve `?m t =?= c` using
+   `?m := fun _ => c`
+   when `?m t` is not a higher-order pattern and `c` is not an application as -/
+(constApprox        : Bool    := false)
 /-
   When the following flag is set,
   `isDefEq` throws the exeption `Exeption.isDefEqStuck`
@@ -707,7 +711,7 @@ abbrev whnfD := whnfUsingDefault
 
 /-- Execute `x` using approximate unification. -/
 @[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
-adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, .. ctx.config }, .. ctx })
+adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, constApprox := true, .. ctx.config }, .. ctx })
   x
 
 @[inline] private def withNewFVar {α} (fvar fvarType : Expr) (k : Expr → MetaM α) : MetaM α := do

src/Init/Lean/Meta/ExprDefEq.lean

@@ -628,6 +628,29 @@ private def simpAssignmentArg (arg : Expr) : MetaM Expr := do
 arg ← if arg.getAppFn.hasExprMVar then instantiateMVars arg else pure arg;
 simpAssignmentArgAux arg
 
+private def checkTypesAndAssign (mvar : Expr) (v : Expr) : MetaM Bool :=
+traceCtx `Meta.isDefEq.assign.checkTypes $ do
+  -- must check whether types are definitionally equal or not, before assigning and returning true
+  mvarType ← inferType mvar;
+  vType    ← inferType v;
+  condM (usingTransparency TransparencyMode.default $ isExprDefEqAux mvarType vType)
+    (do assignExprMVar mvar.mvarId! v; pure true)
+    (do trace `Meta.isDefEq.assign.typeMismatch $ fun _ => mvar ++ " : " ++ mvarType ++ " := " ++ v ++ " : " ++ vType;
+        pure false)
+
+private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
+let mvarId := mvar.mvarId!;
+v? ← checkAssignment mvarId #[] v;
+match v? with
+| none   => pure false
+| some v => do
+  mvarDecl ← getMVarDecl mvarId;
+  forallBoundedTelescope mvarDecl.type numArgs $ fun xs _ =>
+    if xs.size != numArgs then pure false
+    else do
+      v ← mkLambda xs v;
+      checkTypesAndAssign mvar v
+
 private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) (v : Expr) : Nat → Array Expr → MetaM Bool
 | i, args =>
   if h : i < args.size then do
@@ -636,8 +659,10 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
     arg ← simpAssignmentArg arg;
     let args := args.set ⟨i, h⟩ arg;
     let useFOApprox : Unit → MetaM Bool := fun _ =>
-      if cfg.foApprox then
+      if cfg.foApprox && v.isApp then
         processAssignmentFOApprox mvar args v
+      else if cfg.constApprox then
+        processConstApprox mvar args.size v
       else
         pure false;
     match arg with
@@ -654,6 +679,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
     cfg ← getConfig;
     v ← instantiateMVars v; -- enforce A4
     if cfg.foApprox && args.isEmpty && v.getAppFn == mvar then
+      -- using A6
       processAssignmentFOApprox mvar args v
     else do
       let useFOApprox : Unit → MetaM Bool := fun _ =>
@@ -678,11 +704,11 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
           /- We need to type check `v` because abstraction using `mkLambda` may have produced
              a type incorrect term. See discussion at A2 -/
           condM (isTypeCorrect v)
-            (finalize ())
+            (checkTypesAndAssign mvar v)
             (do trace `Meta.isDefEq.assign.typeError $ fun _ => mvar ++ " := " ++ v;
                 useFOApprox ())
         else
-          finalize ()
+          checkTypesAndAssign mvar v
 
 /-- Tries to solve `?m a₁ ... aₙ =?= v` by assigning `?m`.
     It assumes `?m` is unassigned. -/

tests/lean/run/meta2.lean

@@ -361,10 +361,25 @@ do print "----- tst22 -----";
 def test1 : Nat := (fun x y => x + y) 0 1
 
 def tst23 : MetaM Unit :=
-do print "----- tst22 -----";
+do print "----- tst23 -----";
    cinfo ← getConstInfo `test1;
    let v := cinfo.value?.get!;
    print v;
    print v.headBeta
 
 #eval tst23
+
+def tst24 : MetaM Unit :=
+do print "----- tst24 -----";
+   m1 ← mkFreshExprMVar (mkArrow nat (mkArrow type type));
+   m2 ← mkFreshExprMVar type;
+   zero ← mkAppM `HasZero.zero #[nat];
+   idNat ← mkAppM `Id #[nat];
+   let lhs := mkAppB m1 zero m2;
+   print zero;
+   print idNat;
+   print lhs;
+   check $ approxDefEq $ isDefEq lhs idNat;
+   pure ()
+
+#eval tst24