Term has type 1

Stream: general

[Eric Wieser]

A particularly weird error message from this code:

meta instance sigma.reflect {α : Type*} (β : α → Type)
  [reflected α] [reflected β] [hα : has_reflect α] [hβ : Π i, has_reflect (β i)] :
  has_reflect (Σ a, β a) :=
λ ⟨a, b⟩, (`(sigma.mk.{0 0}).subst (hα a)).subst (hβ _ b)

meta instance sigma.reflect₂ {α β : Type} (γ : α → β → Type)  -- error on the second α
  [reflected α] [reflected β] [reflected γ] [hα : has_reflect α] [hβ : has_reflect β]
  [hγ : Π i j, has_reflect (γ i j)] :
  has_reflect (Σ a b, γ a b) :=
@sigma.reflect _ (λ a, Σ b, γ a b) _ _ _ $ λ a,
  @sigma.reflect _ (λ b, γ a b) _ _ _ $ λ b, hγ a b

gives the punchline

type expected at
  α
term has type
  1

[Eric Wieser]

A smaller mwe:

meta example {α β : Type} (a : α) (γ : α → β → Type)
  [reflected β] [reflected γ] [has_reflect α] : reflected (λ (b : β), γ a b) :=
by apply_instance

[Eric Rodriguez]

why is there no reflected instances that are universe polymorphic?

[Eric Wieser]

No idea

[Eric Wieser]

I think the limitation is in the elaborator

[Eric Wieser]

`(@id.{37}) works, but not `(@id.{u})

[Mario Carneiro]

I don't think expr quotations can have variables at all (universe variables are just a particularly common special case)

[Eric Wieser]

Ah indeed, this works:

meta example {α β : Type} (a : α) (γ : α → β → Type)
  [reflected β] [reflected γ] [has_reflect α] : reflected (λ (b : β), γ a b) :=
`(γ).subst `(a)

(regarding the non-variable case)

[Eric Wieser]

So it looks look like by apply_instance is inventing an illegal instance on the spot

[Eric Wieser]

This solves my original puzzle:

meta instance sigma.reflect₂ {α β : Type} (γ : α → β → Type)
  [reflected α] [reflected β] [reflected γ] [hα : has_reflect α] [hβ : has_reflect β]
  [hγ : Π i j, has_reflect (γ i j)] :
  has_reflect (Σ a b, γ a b) :=
@sigma.reflect _ _ _ _ _ $ λ a, @sigma.reflect _ _ _ (`(γ).subst `(a)) _ $ λ b, hγ a b

[Eric Wieser]

Is it possible to write meta code along the lines of the following?

meta def {u} reflect_univ : level := sorry

[Gabriel Ebner]

I think you could do something with type classes:

meta class {u} reflected_univ := (lvl : level)
meta def {u} reflect_univ [reflected_univ.{u}] : level := reflected_univ.lvl
meta instance reflect_univ.zero : reflected_univ.{0} := ⟨level.zero⟩
@[instance] meta def {u} reflect_univ.succ [reflected_univ.{u}] : reflected_univ.{u+1} :=
  ⟨level.succ reflect_univ.{u}⟩
#eval (reflect_univ.{20}).to_string

[Eric Wieser]

Ah nice. I guess the remaining question is whether there's a nice way to provide a reflected (foo.{u}) instance in a generalized way

[Eric Wieser]

I suppose that should be easy to do with a tactic

[Eric Wieser]

Filed a bug report for the original issue at https://github.com/leanprover-community/lean/issues/731, so that I can reference it in workarounds

[Eric Wieser]

Eric Rodriguez said:

why is there no reflected instances that are universe polymorphic?

Fixed in #14766 using @Gabriel Ebner's idea above

[Eric Wieser]

Ugh, this doesn't actually work very well where I wanted to use it; while you can now happily declare these has_reflect instances, lean gets immediately stuck when it needs to synthesize things like reflected _ (α → β) when α and β live in reflected universes