43ef70db63
This PR fixes an issue where the `pp.universes` option would cause constants with no universes to not use unexpanders or dot notation. For example, `p ↔ q` would pretty print as `Iff p q` even though `Iff` has no universe levels.
87 lines
1.8 KiB
Text
87 lines
1.8 KiB
Text
/-!
|
||
# Localized error messages with unassigned metavariables
|
||
-/
|
||
|
||
set_option pp.mvars false
|
||
|
||
|
||
/-!
|
||
Test: now reports "don't know how to synthesize implicit argument" rather than an error on the `example` command.
|
||
-/
|
||
|
||
/--
|
||
error: don't know how to synthesize implicit argument `α`
|
||
@none ?_
|
||
context:
|
||
⊢ Type _
|
||
---
|
||
error: failed to infer `let` declaration type
|
||
-/
|
||
#guard_msgs in
|
||
example : IO Unit := do
|
||
let x := none
|
||
pure ()
|
||
|
||
|
||
/-!
|
||
Test: now reports that the universe levels are not assigned at the 'let' rather than an error on the `example` command.
|
||
-/
|
||
|
||
/--
|
||
error: failed to infer universe levels in `let` declaration type
|
||
PUnit.{_}
|
||
-/
|
||
#guard_msgs in
|
||
def foo : IO Unit := do
|
||
let x : PUnit := PUnit.unit
|
||
pure ()
|
||
|
||
-- specializes to 0 on error
|
||
/--
|
||
info: def foo : IO Unit :=
|
||
have x := PUnit.unit.{0};
|
||
pure.{0, 0} ()
|
||
-/
|
||
#guard_msgs in set_option pp.universes true in #print foo
|
||
|
||
|
||
/-!
|
||
Test: Works for `have` too.
|
||
-/
|
||
|
||
/--
|
||
error: failed to infer universe levels in `have` declaration type
|
||
PUnit.{_}
|
||
-/
|
||
#guard_msgs in
|
||
def foo' : IO Unit := do
|
||
have x : PUnit := PUnit.unit
|
||
pure ()
|
||
|
||
|
||
/-!
|
||
Test: Works for `fun` binders.
|
||
-/
|
||
|
||
/--
|
||
error: Failed to infer universe levels in type of binder `x`
|
||
PUnit.{_}
|
||
-/
|
||
#guard_msgs in
|
||
example : Nat := (fun x : PUnit => 2) PUnit.unit
|
||
|
||
|
||
/-!
|
||
Test: A failure not in a binder, right now reports an error on `example`.
|
||
A change is that before the error was about level parameters rather than metavariables since
|
||
the def elaborator would turn all metavariables into parameters before this analysis.
|
||
-/
|
||
|
||
/--
|
||
error: declaration `_example` contains universe level metavariables at the expression
|
||
Function.const.{1, imax (_ + 1) _} ({α : Sort _} → α → α) 2 @id.{_}
|
||
in the declaration body
|
||
Function.const.{1, imax (_ + 1) _} ({α : Sort _} → α → α) 2 @id.{_}
|
||
-/
|
||
#guard_msgs in
|
||
example : Nat := Function.const _ 2 @id
|