From f07b9926b1b9746dccfae68632c97f58941917dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Feb 2021 10:27:34 -0800 Subject: [PATCH] feat: unfold coercions and `coeFun`, `coeSort`, `coeM`, `liftCoeM` TODO: `coe` --- src/Lean/Elab/App.lean | 6 +++--- src/Lean/Elab/Term.lean | 12 +++++++----- src/Lean/Meta/Coe.lean | 3 ++- tests/lean/scopedunifhint.lean.expected.out | 16 ++++++++-------- 4 files changed, 20 insertions(+), 17 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index c799586220..091fe157ec 100644 --- a/src/Lean/Elab/App.lean +++ b/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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 64e1baf0ab..0a6a0e51a5 100644 --- a/src/Lean/Elab/Term.lean +++ b/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 diff --git a/src/Lean/Meta/Coe.lean b/src/Lean/Meta/Coe.lean index fedf0e19b0..82131807a6 100644 --- a/src/Lean/Meta/Coe.lean +++ b/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 := diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out index 8a83fed6f0..93ba13507a 100644 --- a/tests/lean/scopedunifhint.lean.expected.out +++ b/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.α