universe polymorphism weirdness

Stream: general

[Eric Wieser]

What's going on here?

inductive plist (T : Sort*)
| nil : plist
| cons (hd : T) (tl : plist) : plist

-- ok for 0, 1, 2, ...
meta instance plist.reflect {α : Sort 2} [has_reflect α] [reflected α] : has_reflect (plist α)
| plist.nil     := `(plist.nil)
| (plist.cons h t) := `(λ t, plist.cons h t).subst (plist.reflect t)

-- fails with a wildcard
meta instance plist.reflect' {α : Sort*} [has_reflect α] [reflected α] : has_reflect (plist α)
| plist.nil     := `(plist.nil)
| (plist.cons h t) := `(λ t, plist.cons h t).subst (plist.reflect t)
``