+Note [Equality predicates]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+ forall a b. (a :=: S b) => a -> b
+could be represented by
+ ForAllTy a (ForAllTy b (FunTy (PredTy (EqPred a (S b))) ...))
+OR
+ ForAllTy a (ForAllTy b (ForAllTy (c::PredTy (EqPred a (S b))) ...))
+
+The latter is what we do. (Unlike for class and implicit parameter
+constraints, which do use FunTy.)
+
+Reason:
+ * FunTy is always a *value* function
+ * ForAllTy is discarded at runtime
+
+We often need to make a "wildcard" (c::PredTy..). We always use the same
+name (wildCoVarName), since it's not mentioned.
+