cryptic error

Stream: general

[Jon Eugster]

I've come across a user mistake which corresponds to the following MWE:

#check (1 : ∀ (n : Nat), True) -- error: invalid universe level, ?u.5 is not greater than 0

Writing 1 : here is nonsense, but does somebody understand why the error messages says what it says? Why is it about universes?

[Shreyas Srinivas]

It says that the universe of your type is 0 I.e. you have a Prop.

[Yaël Dillies]

Is it trying to apply docs#Pi.instOne and failing to unify f : ι → Type v₁ with fun _ : Nat ↦ True?

[Shreyas Srinivas]

Yaël Dillies said:

Is it trying to apply docs#Pi.instOne and failing to unify f : ι → Type v₁ with fun _ : Nat ↦ True?

Would that also cause the same error on #check (2 : ∀ (n : Nat), True)

[Shreyas Srinivas]

I think basically it complains because you are giving it a value that is data, which is at least universe 1 or higher and the type is a Prop

[Shreyas Srinivas]

I am guessing that the part of the typechecker that performs universe unification runs early into typechecking, but I could be wrong.

[Shreyas Srinivas]

My guess is wrong. This produces a normal type error :

#check ("some_string": ∀ (n : Nat), True)

[Jon Eugster]

Yaël Dillies said:

Is it trying to apply docs#Pi.instOne and failing to unify f : ι → Type v₁ with fun _ : Nat ↦ True?

That's not quite it, because it's also triggered without import Mathlib the following snippet shows that the error message from docs#One are a bit better:

import Mathlib

/-
application type mismatch
  One (ℕ → True)
argument
  ℕ → True
has type
  Prop : Type
but is expected to have type
  Type ?u.1 : Type (?u.1 + 1)
-/
#synth One <| (∀ (n : Nat), True)

The error invalid universe level, {u} is not greater than 0 comes apparently from docs#Lean.Meta.decLevel core

[Shreyas Srinivas]

A little more debugging later:

import Qq
import Lean
open Qq Lean Meta

#check (1 : ∀ (n : Nat), True) -- error: invalid universe level, ?u.5 is not greater than 0


#eval q(1 : ∀ (n : Nat), True) -- produces the message below

Lean.Expr.app
  (Lean.Expr.app
    (Lean.Expr.const `sorryAx [Lean.Level.zero])
    (Lean.Expr.forallE
      Lean.Name.anonymous
      (Lean.Expr.const `Nat [])
      (Lean.Expr.const `True [])
      (Lean.BinderInfo.default)))
  (Lean.Expr.const `Bool.true [])

[Jon Eugster]

Thanks for the insight, both of you!

[Shreyas Srinivas]

Lean is interpreting the 1 as a level expression for some unknown reason. EDIT:
My mistake. I was looking at this ((Lean.Expr.const sorryAx [Lean.Level.zero]))

[Jon Eugster]

Ah I understand now:

Writing 1 triggers docs#Lean.Elab.Term.elabNumLit and on this line in core this calls docs#Lean.Meta.getDecLevel with an expected type of level 0 thus it triggers the error.

[Shreyas Srinivas]

And this doesn't happen with strings because elabStrLit directly calls mkStrLit?

[Shreyas Srinivas]

What is passed to the expectedType? parameter of elabNumLit here?

[Jon Eugster]

Shreyas Srinivas said:

And this doesn't happen with strings because elabStrLit directly calls mkStrLit?
What is passed to the expectedType? parameter of elabNumLit here?

Looks like it. I think expectedType? here is some (Nat → True).

FWIW I've create a PR lean4#4366 which adds a more verbose error message.

[Shreyas Srinivas]

Could the error message also show the expected type?

[Jon Eugster]

it could, I just didnt know how to do that without either an additional match statement or a superfluous some floating around.

Do you have a suggestion for the ideal wording? Kyle made a very good suggestion, as always :)

[Shreyas Srinivas]

Oh. I don't see Kyle's suggestion, but I do see that Leo added more fine grained error reporting

[Jon Eugster]

Indeed that was way fast of Leo :octopus: