Zulip Chat Archive

Stream: general

Topic: universe polymorphism weirdness


view this post on Zulip Eric Wieser (Feb 18 2021 at 14:01):

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)
``

Last updated: May 11 2021 at 00:31 UTC