The expected type of elabTerm

Stream: lean4

[Joachim Breitner]

I am surprised that this works:

import Mathlib.Tactic.RunCmd
open Lean Elab Term Command Meta

run_cmd liftTermElabM do
    let t ← elabTerm (← `(term|true)) (some (.sort (← mkFreshLevelMVar)))
    IO.println t

I was expecting by saying that I expect something of type Sort _, it will reject to elaborate true (as true : Bool). Is that now how the expectedType parameter works? The docstring didn’t say.

[Joachim Breitner]

Ah, there exists elabTermEnsuringType

[Kyle Miller]

Yeah, the expected type is a hint for what type you want from the elaborated term, but you need something like docs#Lean.Elab.Term.elabTermEnsuringType to elaborate with that hint and then try to insert a coercion if there's a type mismatch.

[Kyle Miller]

This function does elabTerm followed by docs#Lean.Elab.Term.ensureHasType

[Joachim Breitner]

Thanks! Reading through the code gave me a glimpse. Maybe I’ll PR a slight docstring addition, pointing to elabTermEnsuringType.

[Kyle Miller]

Watch out that there's also docs#Lean.Elab.Tactic.elabTermEnsuringType, which doesn't insert a coercion. (It also does Term.synthesizeSyntheticMVars before unifying the type of the term with the expected type, which seems like it might be a bug -- I think this accounts for many problems with refine and its failure to synthesize instances.)

[Joachim Breitner]

Hmm, not sure if I at this point can PR a better docstring than “It’s complicated, read the code” :-D