Some design documentation (here: level polymorphism)

doc/README/Design/LevelPolymorphism.md

@@ -0,0 +1,15 @@
+* Level polymorphism
+
+`⊥` in `Data.Empty` and `⊤` in `Data.Unit` are not `Level`-polymorphic as that
+tends to lead to unsolved metas (see discussion at issue #312).  This is understandable
+as very often the level of (say) `⊤` is under-determined by its surrounding context,
+leading to unsolved metas. This is frequent enough that it makes sense for the default
+versions to be monomorphic (at Level 0).
+
+But there are other cases where exactly the opposite is needed.  for that purpose,
+there are level-polymorphic versions in `Data.Empty.Polymorphic` and
+`Data.Unit.Polymorphic` respectively.
+
+The same issue happens in `Relation.Unary` which defines `Ø` and `U` at `Level` 0, else
+a lot of unsolved metas appear (for example in `Relation.Unary.Properties`). For that
+purpose, `Relation.Unary.Polymorphic` exists.

src/Data/Empty.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Empty type, judgementally proof irrelevant
+-- Empty type, judgementally proof irrelevant, Level-monomorphic
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

src/Data/Unit.agda

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- The unit type
+-- The unit type, Level-monomorphic version
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

src/Relation/Unary.agda

@@ -42,6 +42,8 @@ Pred A ℓ = A → Set ℓ
 -- Special sets
 
 -- The empty set.
+-- Explicitly not level polymorphic as this often causes unsolved metas;
+-- see `Relation.Unary.Polymorphic` for a level-polymorphic version.
 
 ∅ : Pred A 0ℓ
 ∅ = λ _ → ⊥
@@ -52,6 +54,7 @@ Pred A ℓ = A → Set ℓ
 ｛ x ｝ = x ≡_
 
 -- The universal set.
+-- Explicitly not level polymorphic (see comments for `∅` for more details)
 
 U : Pred A 0ℓ
 U = λ _ → ⊤