@@ -40,8 +40,11 @@ private partial def recProjTarget (e : Expr) (nm : Name := e.getAppFn.constName!
4040 else
4141 return nm
4242
43- /-- Expand coercions occurring in `e` -/
44- partial def expandCoe (e : Expr) : MetaM Expr :=
43+ /--
44+ Expands coercions occurring in `e` and return the result together with a list of applied
45+ `Coe` instances.
46+ -/
47+ partial def expandCoe (e : Expr) : MetaM (Expr × List Name) := StateT.run (s := ([] : List Name)) do
4548 withReducibleAndInstances do
4649 transform e fun e => do
4750 let f := e.getAppFn
@@ -55,8 +58,18 @@ partial def expandCoe (e : Expr) : MetaM Expr :=
5558 should still appear after unfolding (unless there are unused variables in the instances).
5659 -/
5760 recordExtraModUseFromDecl (isMeta := false ) (← recProjTarget e)
58- if let some e ← unfoldDefinition? e then
59- return .visit e.headBeta
61+ if let some e' ← unfoldDefinition? e then
62+ /-
63+ If the unfolded coercion is an application of `Coe.coe` and its third argument is
64+ an application of a constant, record this constant's name.
65+ -/
66+ if declName = ``Coe.coe then
67+ if let some inst := e.getAppArgs[2 ]? then
68+ let g := inst.getAppFn
69+ if g.isConst then
70+ let instName := g.constName!
71+ StateT.set (instName :: (← StateT.get))
72+ return .visit e'.headBeta
6073 return .continue
6174
6275register_builtin_option autoLift : Bool := {
@@ -65,20 +78,27 @@ register_builtin_option autoLift : Bool := {
6578}
6679
6780/-- Coerces `expr` to `expectedType` using `CoeT`. -/
68- def coerceSimple ?do
81+ def coerceSimpleRecordingNames ?( Expr × List Name) ) := do
6982 let eType ← inferType expr
7083 let u ← getLevel eType
7184 let v ← getLevel expectedType
7285 let coeTInstType := mkAppN (mkConst ``CoeT [u, v]) #[eType, expr, expectedType]
7386 match ← trySynthInstance coeTInstType with
7487 | .some inst =>
7588 let result ← expandCoe (mkAppN (mkConst ``CoeT.coe [u, v]) #[eType, expr, expectedType, inst])
76- unless ← isDefEq (← inferType result) expectedType do
77- throwError "Could not coerce{indentExpr expr}\n to{indentExpr expectedType}\n coerced expression has wrong type:{indentExpr result}"
89+ unless ← isDefEq (← inferType result. 1 ) expectedType do
90+ throwError "Could not coerce{indentExpr expr}\n to{indentExpr expectedType}\n coerced expression has wrong type:{indentExpr result.1 }"
7891 return .some result
7992 | .undef => return .undef
8093 | .none => return .none
8194
95+ /-- Coerces `expr` to `expectedType` using `CoeT`. -/
96+ def coerceSimple? (expr expectedType : Expr) : MetaM (LOption Expr) := do
97+ match ← coerceSimpleRecordingNames? expr expectedType with
98+ | .some (result, _) => return .some result
99+ | .none => return .none
100+ | .undef => return .undef
101+
82102/-- Coerces `expr` to a function type. -/
83103def coerceToFunction? (expr : Expr) : MetaM (Option Expr) := do
84104 -- constructing expression manually because mkAppM wouldn't assign universe mvars
@@ -87,7 +107,7 @@ def coerceToFunction? (expr : Expr) : MetaM (Option Expr) := do
87107 let v ← mkFreshLevelMVar
88108 let γ ← mkFreshExprMVar (← mkArrow α (mkSort v))
89109 let .some inst ← trySynthInstance (mkApp2 (.const ``CoeFun [u,v]) α γ) | return none
90- let expanded ← expandCoe (mkApp4 (.const ``CoeFun.coe [u,v]) α γ inst expr)
110+ let ( expanded, _) ← expandCoe (mkApp4 (.const ``CoeFun.coe [u,v]) α γ inst expr)
91111 unless (← whnf (← inferType expanded)).isForall do
92112 throwError m!"Failed to coerce{indentExpr expr}\n to a function: After applying `CoeFun.coe`, result is still not a function{indentExpr expanded}"
93113 ++ .hint' m!"This is often due to incorrect `CoeFun` instances; the synthesized instance was{indentExpr inst}"
@@ -101,7 +121,7 @@ def coerceToSort? (expr : Expr) : MetaM (Option Expr) := do
101121 let v ← mkFreshLevelMVar
102122 let β ← mkFreshExprMVar (mkSort v)
103123 let .some inst ← trySynthInstance (mkApp2 (.const ``CoeSort [u,v]) α β) | return none
104- let expanded ← expandCoe (mkApp4 (.const ``CoeSort.coe [u,v]) α β inst expr)
124+ let ( expanded, _) ← expandCoe (mkApp4 (.const ``CoeSort.coe [u,v]) α β inst expr)
105125 unless (← whnf (← inferType expanded)).isSort do
106126 throwError m!"Failed to coerce{indentExpr expr}\n to a type: After applying `CoeSort.coe`, result is still not a type{indentExpr expanded}"
107127 ++ .hint' m!"This is often due to incorrect `CoeSort` instances; the synthesized instance was{indentExpr inst}"
@@ -190,7 +210,10 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
190210 let saved ← saveState
191211 if (← isDefEq m n) then
192212 let some monadInst ← isMonad? n | restoreState saved; return none
193- try expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e]) catch _ => restoreState saved; return none
213+ try
214+ let (result, _) ← expandCoe (← mkAppOptM ``Lean.Internal.coeM #[m, α, β, none, monadInst, e])
215+ pure result
216+ catch _ => restoreState saved; return none
194217 else if autoLift.get (← getOptions) then
195218 try
196219 -- Construct lift from `m` to `n`
@@ -217,7 +240,7 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
217240 let v ← getLevel β
218241 let coeTInstType := Lean.mkForall `a BinderInfo.default α <| mkAppN (mkConst ``CoeT [u, v]) #[α, mkBVar 0 , β]
219242 let .some coeTInstVal ← trySynthInstance coeTInstType | return none
220- let eNew ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
243+ let ( eNew, _) ← expandCoe (mkAppN (Lean.mkConst ``Lean.Internal.liftCoeM [u_1, u_2, u_3]) #[m, n, α, β, monadLiftVal, coeTInstVal, monadInst, e])
221244 let eNewType ← inferType eNew
222245 unless (← isDefEq expectedType eNewType) do return none
223246 return some eNew -- approach 3 worked
@@ -227,17 +250,34 @@ def coerceMonadLift? (e expectedType : Expr) : MetaM (Option Expr) := do
227250 else
228251 return none
229252
230- /-- Coerces `expr` to the type `expectedType`.
231- Returns `.some coerced` on successful coercion,
253+ /--
254+ Coerces `expr` to the type `expectedType`.
255+ Returns `.some (coerced, appliedCoeDecls)` on successful coercion,
232256`.none` if the expression cannot by coerced to that type,
233- or `.undef` if we need more metavariable assignments. -/
234- def coerce? (expr expectedType : Expr) : MetaM (LOption Expr) := do
257+ or `.undef` if we need more metavariable assignments.
258+
259+ `appliedCoeDecls` is a list of names representing the names of the `Coe` instances that were
260+ applied.
261+ -/
262+ def coerceCollectingNames? (expr expectedType : Expr) : MetaM (LOption (Expr × List Name)) := do
235263 if let some lifted ← coerceMonadLift? expr expectedType then
236- return .some lifted
264+ return .some ( lifted, [])
237265 if (← whnfR expectedType).isForall then
238266 if let some fn ← coerceToFunction? expr then
239267 if ← isDefEq (← inferType fn) expectedType then
240- return .some fn
241- coerceSimple? expr expectedType
268+ return .some (fn, [])
269+ coerceSimpleRecordingNames? expr expectedType
270+
271+ /--
272+ Coerces `expr` to the type `expectedType`.
273+ Returns `.some coerced` on successful coercion,
274+ `.none` if the expression cannot by coerced to that type,
275+ or `.undef` if we need more metavariable assignments.
276+ -/
277+ def coerce? (expr expectedType : Expr) : MetaM (LOption Expr) := do
278+ match ← coerceCollectingNames? expr expectedType with
279+ | .some (result, _) => return .some result
280+ | .none => return .none
281+ | .undef => return .undef
242282
243283end Lean.Meta
0 commit comments