8424ddbb3e
This PR improves the “expected type mismatch” error message by omitting the type's types when they are defeq, and putting them into separate lines when not. I found it rather tediuos to parse the error message when the expected type is long, because I had to find the `:` in the middle of a large expression somewhere. Also, when both are of sort `Prop` or `Type` it doesn't add much value to print the sort (and it’s only one hover away anyways).
56 lines
1.2 KiB
Text
56 lines
1.2 KiB
Text
import Lean.Elab.Command
|
|
|
|
set_option pp.mvars false
|
|
|
|
/--
|
|
error: Application type mismatch: In the application
|
|
⟨Nat.lt_irrefl (?_ n), Fin.is_lt ?_⟩
|
|
the argument
|
|
Fin.is_lt ?_
|
|
has type
|
|
↑?_ < ?_
|
|
but is expected to have type
|
|
?_ n < ?_ n
|
|
-/
|
|
#guard_msgs in
|
|
def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
|
|
|
|
/--
|
|
error: type mismatch
|
|
Fin.is_lt ?_
|
|
has type
|
|
↑?_ < ?_
|
|
but is expected to have type
|
|
?_ < ?_
|
|
---
|
|
error: unsolved goals
|
|
case a
|
|
⊢ Nat
|
|
|
|
this : ?_ < ?_
|
|
⊢ True
|
|
-/
|
|
#guard_msgs in
|
|
def test : True := by
|
|
have : ((?a : Nat) < ?a : Prop) := by
|
|
refine Fin.is_lt ?_
|
|
done
|
|
done
|
|
|
|
open Lean Meta
|
|
/--
|
|
info: Defeq?: false
|
|
---
|
|
info: fun x_0 x_1 => x_1
|
|
-/
|
|
#guard_msgs in
|
|
run_meta do
|
|
let mvarIdNat ← mkFreshExprMVar (.some (.const ``Nat []))
|
|
let mvarIdFin ← mkFreshExprMVar (.some (.app (.const `Fin []) mvarIdNat))
|
|
-- mvarIdNat.assign (.app (.const ``Fin.val []) mvaridFin))
|
|
let b ← isDefEq mvarIdNat (mkApp2 (.const ``Fin.val []) mvarIdNat mvarIdFin)
|
|
logInfo m!"Defeq?: {b}" -- prints true
|
|
-- Now mvaridNat occurs in its own type
|
|
-- This will stack overflow
|
|
let r ← abstractMVars mvarIdFin (levels := false)
|
|
logInfo m!"{r.expr}"
|