failed to use `unit`

Stream: new members

[Alex Zhang]

What does using unit fail in this case?

universe u
example : ∃ (I : Type u), true :=
begin
  use unit,
end

error failed to instantiate goal with unit

[Alex Zhang]

universe u
example : ∃ (I : Type u), true :=
begin
  refine ⟨ unit, _⟩,
end

error :

type mismatch at application
  Exists.intro unit
term
  unit
has type
  Type : Type 1
but is expected to have type
  Type u : Type (u+1)

[Eric Rodriguez]

punit is the universe polymorphic version of unit

[Alex Zhang]

I found

example : ∃ (I : Type*), true :=
begin
  refine ⟨ (unit : Type 0), _⟩,
end

is fine.

[Alex Zhang]

The thing I don't understand is, in the second error message, I thought Type : Type 1 should be able to match Type u : Type (u+1). Can't u be 0?

[Eric Rodriguez]

the previous version is kind of ∀ u, ∃ I : Type u, true, whilst the second is more like ∃ u, ∃ I : Type u, true; the universe is a "metavariable" in the Type* example and is allowed to be filled in to what's needed later

[Eric Rodriguez]

okay, but actually it gets more interesting; do it as a lemma/theorem and it fails again, whilst as a def it's fine. I'm not too sure why that is.

[Alex Zhang]

Eric Rodriguez said:

okay, but actually it gets more interesting; do it as a lemma/theorem and it fails again, whilst as a def it's fine. I'm not too sure why that is.

Yeah, I also found this! That is confusing.

[Alex Zhang]

I guess punit does not have enough APIs, lean even doesn't know matrix punit punit ℚ has one..

[Eric Wieser]

example behaves like a def

[Eric Wieser]

In that it's type is affected by the implementation

[Eric Wieser]

Whereas lemmas the type is known before looking at the proof

[Eric Wieser]

Which is why def trivial' := trivial works fine, but lemma trivial' := trivial fails

[Eric Rodriguez]

so in a lemma Type* gets instantly evaluated to Type u for some u, whilst in a def it becomes Type ?u_1, and gets filled in by the proof?

[Eric Wieser]

Type * means "guess the universe level based on how I use it"

[Eric Wieser]

So essentially your description is correct, but lemma fills in the universe metavariables when it reaches the :=