Skip to content

feat: update mkCoe, ensureHasType, and elabTermEnsuringType to allow MessageData headers #11390

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
thorimur wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

feat: update mkCoe, ensureHasType, and elabTermEnsuringType to allow MessageData headers #11390

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
93a9745
feat: update `mkCoe`, `ensureHasType`, and `elabTermEnsuringType` to …
thorimur Nov 26, 2025
ec74322
feat: experiment with `MessageData` in `SyntheticMVarKind.coe`
thorimur Nov 26, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions src/Lean/Elab/Term/TermElabM.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ inductive SyntheticMVarKind where
If `header?` is not provided, the default header is "type mismatch".
If `f?` is provided, then throws an application type mismatch error.
-/
| coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
| coe (header? : Option MessageData) (expectedType : Expr) (e : Expr) (f? : Option Expr)
(mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData))
/--
Use tactic to synthesize value for metavariable.
Expand Down Expand Up @@ -1183,7 +1183,8 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
else
throwNamedError lean.synthInstanceFailed "failed to synthesize instance of type class{indentExpr type}{extraErrorMsg}{useTraceSynthMsg}"

def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none)
def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none)
(errorMsgHeader? : Option MessageData := none)
(mkErrorMsg? : Option (MVarId → (expectedType e : Expr) → MetaM MessageData) := none)
(mkImmedErrorMsg? : Option ((errorMsg? : Option MessageData) → (expectedType e : Expr) → MetaM MessageData) := none) : TermElabM Expr := do
withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
Expand Down Expand Up @@ -1219,7 +1220,7 @@ If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally
Argument `f?` is used only for generating error messages when inserting coercions fails.
-/
def ensureHasType (expectedType? : Option Expr) (e : Expr)
(errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr := do
(errorMsgHeader? : Option MessageData := none) (f? : Option Expr := none) : TermElabM Expr := do
let some expectedType := expectedType? | return e
if (← isDefEq (← inferType e) expectedType) then
return e
Expand Down Expand Up @@ -1772,7 +1773,7 @@ by inserting coercions if necessary.
If `errToSorry` is true, then if coercion insertion fails, this function returns `sorry` and logs the error.
Otherwise, it throws the error.
-/
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option MessageData := none) : TermElabM Expr := do
let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
try
withRef stx <| ensureHasType expectedType? e errorMsgHeader?
Expand Down
Loading