feat: unfold coercions and coeFun, coeSort, coeM, liftCoeM

TODO: `coe`

src/Lean/Elab/App.lean

@@ -73,11 +73,11 @@ private def tryCoeFun? (α : Expr) (a : Expr) : TermElabM (Option Expr) := do
   let mvarId := mvar.mvarId!
   try
     if (← synthesizeCoeInstMVarCore mvarId) then
-      pure $ some $ mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar]
+      expandCoe <| mkAppN (Lean.mkConst `coeFun [u, v]) #[α, γ, a, mvar]
     else
-      pure none
+      return none
   catch _ =>
-    pure none
+    return none
 
 def synthesizeAppInstMVars (instMVars : Array MVarId) : TermElabM Unit :=
   for mvarId in instMVars do

src/Lean/Elab/Term.lean

@@ -10,6 +10,7 @@ import Lean.Meta.ExprDefEq
 import Lean.Meta.AppBuilder
 import Lean.Meta.SynthInstance
 import Lean.Meta.CollectMVars
+import Lean.Meta.Coe
 import Lean.Meta.Tactic.Util
 import Lean.Hygiene
 import Lean.Util.RecDepth
@@ -613,6 +614,7 @@ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eTyp
       let coeTInstType := mkAppN (mkConst `CoeT [u, v]) #[eType, e, expectedType]
       let mvar ← mkFreshExprMVar coeTInstType MetavarKind.synthetic
       let eNew := mkAppN (mkConst `coe [u, v]) #[eType, expectedType, e, mvar]
+      -- TODO: MODIFY
       let mvarId := mvar.mvarId!
       try
         withoutMacroStackAtErr do
@@ -757,7 +759,7 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
   let some (m, α) ← isTypeApp? eType | tryPureCoeAndSimple
   if (← isDefEq m n) then
     let some monadInst ← isMonad? n | tryCoeSimple
-    try mkAppOptM `coeM #[m, α, β, none, monadInst, e] catch _ => throwMismatch
+    try expandCoe (← mkAppOptM `coeM #[m, α, β, none, monadInst, e]) catch _ => throwMismatch
   else
     try
       -- Construct lift from `m` to `n`
@@ -769,17 +771,17 @@ private def tryLiftAndCoe (errorMsgHeader? : Option String) (expectedType : Expr
       let eNew := mkAppN (Lean.mkConst `liftM [u_1, u_2, u_3]) #[m, n, monadLiftVal, α, e]
       let eNewType ← inferType eNew
       if (← isDefEq expectedType eNewType) then
-        pure eNew -- approach 2 worked
+        return eNew -- approach 2 worked
       else
         let some monadInst ← isMonad? n | tryCoeSimple
         let u ← getLevel α
         let v ← getLevel β
         let coeTInstType := Lean.mkForall `a BinderInfo.default α $ mkAppN (mkConst `CoeT [u, v]) #[α, mkBVar 0, β]
         let coeTInstVal ← synthesizeInst coeTInstType
-        let eNew := mkAppN (Lean.mkConst `liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e]
+        let eNew ← expandCoe (← mkAppN (Lean.mkConst `liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
         let eNewType ← inferType eNew
         unless (← isDefEq expectedType eNewType) do throwMismatch
-        pure eNew -- approach 3 worked
+        return eNew -- approach 3 worked
     catch _ =>
       /-
         If `m` is not a monad, then we try to use `tryPureCoe?` and then `tryCoe?`.
@@ -1057,7 +1059,7 @@ private def tryCoeSort (α : Expr) (a : Expr) : TermElabM Expr := do
   try
     withoutMacroStackAtErr do
       if (← synthesizeCoeInstMVarCore mvarId) then
-        pure $ mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar]
+        expandCoe <| mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar]
       else
         throwError "type expected"
   catch

src/Lean/Meta/Coe.lean

@@ -18,7 +18,8 @@ def isCoeDecl (declName : Name) : Bool :=
   declName == ``coeTC || declName == ``coeFun || declName == ``coeSort ||
   declName == ``Coe.coe || declName == ``CoeTC.coe || declName == ``CoeHead.coe ||
   declName == ``CoeTail.coe || declName == ``CoeHTCT.coe || declName == ``CoeDep.coe ||
-  declName == ``CoeT.coe || declName == ``CoeFun.coe || declName == ``CoeSort.coe
+  declName == ``CoeT.coe || declName == ``CoeFun.coe || declName == ``CoeSort.coe ||
+  declName == ``liftCoeM || declName == ``coeM
 
 /-- Expand coercions occurring in `e` -/
 partial def expandCoe (e : Expr) : MetaM Expr :=

tests/lean/scopedunifhint.lean.expected.out

@@ -5,7 +5,7 @@ argument
 has type
   Nat
 but is expected to have type
-  coeSort ?m
+  ?m.α
 scopedunifhint.lean:29:7-29:24: error: application type mismatch
   mul (x, x) (x, x)
 argument
@@ -13,7 +13,7 @@ argument
 has type
   Nat × Nat
 but is expected to have type
-  coeSort ?m
+  ?m.α
 scopedunifhint.lean:33:7-33:10: error: application type mismatch
   x*x
 argument
@@ -21,9 +21,9 @@ argument
 has type
   Nat
 but is expected to have type
-  coeSort ?m
-x*x : coeSort Nat.Magma
-x*x : coeSort Nat.Magma
+  ?m.α
+x*x : Nat.Magma.α
+x*x : Nat.Magma.α
 scopedunifhint.lean:39:7-39:24: error: application type mismatch
   (x, x)*(x, x)
 argument
@@ -31,8 +31,8 @@ argument
 has type
   Nat × Nat
 but is expected to have type
-  coeSort ?m
-(x, x)*(x, x) : coeSort (Prod.Magma Nat.Magma Nat.Magma)
+  ?m.α
+(x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
 scopedunifhint.lean:56:7-56:22: error: application type mismatch
   (x, x)*(x, x)
 argument
@@ -40,4 +40,4 @@ argument
 has type
   Nat × Nat
 but is expected to have type
-  coeSort ?m
+  ?m.α