"Check (nat : Type) : Set." now fails with universe inconsistency (polyproj)

[JasonGross]

Check (nat : Type) : Set.
(* Error:
The term "nat:Type" has type "Type" while it is expected to have type
"Set" (Universe inconsistency). *)

[mattam82]

This makes sense, that Type has a rigid universe level and hence can't be coerced to Set. This is backwards-compatible as well.

[mattam82]

Also, how am I supposed to disallow the unification of @eq Type A B and @eq Set A B from another bug report if this is allowed?

[JasonGross]

Er, right. I think this worked in HoTT/coq, but I agree now that it shouldn't. Feel free to move the corresponding test case from opened to closed, leaving the Fail in place, so that we have a test that this shouldn't work.