Rename TypeError -> UnsatisfiedConstraint

Author: jespercockx

lib/base/Haskell/Prelude.agda

@@ -6,7 +6,7 @@ open Haskell.Prim public using
   ( Type;
     Bool; True; False; Char; Integer;
     List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; lengthNat;
+    UnsatisfiedConstraint; ⊥; iNumberNat; lengthNat;
     IsTrue; IsFalse; NonEmpty;
     All; allNil; allCons;
     Any; anyHere; anyThere;

lib/base/Haskell/Prim.agda

@@ -124,7 +124,7 @@ data IsFalse : Bool → Type where
 data NonEmpty {a : Type} : List a → Type where
   instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)
 
-data TypeError (err : AgdaString) : Type where
+data UnsatisfiedConstraint (err : AgdaString) : Type where
 
 it : ∀ {@0 ℓ} {@0 a : Type ℓ} → ⦃ a ⦄ → a
 it ⦃ x ⦄ = x

lib/base/Haskell/Prim/Int.agda

@@ -103,7 +103,7 @@ showInt a = showInteger (intToInteger a)
 
 @0 IsNonNegativeInt : Int → Type
 IsNonNegativeInt a@(int64 _) =
-  if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
+  if isNegativeInt a then UnsatisfiedConstraint (primStringAppend (primStringFromList (showInt a)) " is negative")
                      else ⊤
 
 intToNat : (a : Int) → @0 ⦃ IsNonNegativeInt a ⦄ → Nat

lib/base/Haskell/Prim/Integer.agda

@@ -103,4 +103,4 @@ isNegativeInteger (negsuc _) = True
 @0 IsNonNegativeInteger : Integer → Type
 IsNonNegativeInteger (pos _)      = ⊤
 IsNonNegativeInteger n@(negsuc _) =
-  TypeError (primStringAppend (primShowInteger n) (" is negative"))
+  UnsatisfiedConstraint (primStringAppend (primShowInteger n) (" is negative"))