diff --git a/doc/README/Design/LevelPolymorphism.md b/doc/README/Design/LevelPolymorphism.md
new file mode 100644
index 0000000000..59436fe4a3
--- /dev/null
+++ b/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.
diff --git a/src/Data/Empty.agda b/src/Data/Empty.agda
index 990a9a1632..19754e8c7d 100644
--- a/src/Data/Empty.agda
+++ b/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 #-}
diff --git a/src/Data/Unit.agda b/src/Data/Unit.agda
index 2e3464c7f4..73f269d9d6 100644
--- a/src/Data/Unit.agda
+++ b/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 #-}
diff --git a/src/Relation/Unary.agda b/src/Relation/Unary.agda
index 9f3ea16633..0f8a7534fd 100644
--- a/src/Relation/Unary.agda
+++ b/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 = λ _ → ⊤