diff --git a/docs/source/features.md b/docs/source/features.md
index 4b540cc1..f3455447 100644
--- a/docs/source/features.md
+++ b/docs/source/features.md
@@ -31,7 +31,7 @@ Standard data type declarations have a simple equivalent in Agda.
 
 Agda:
 ```agda
-data Nat : Set where
+data Nat : Type where
     Zero : Nat 
     Suc : Nat → Nat
 
@@ -43,11 +43,13 @@ Haskell:
 data Nat = Zero | Suc Nat
 ```
 
+In the definition above, we have to explicitly indicate that `Nat` is a data `Type` by writing the signature `Nat : Type`.
+
 You can also use polymorphic types in the data declarations.
 
 Agda:
 ```agda
-data Tree (a : Set) : Set where
+data Tree (a : Type) : Type where
     Leaf   : a → Tree a
     Branch : a → Tree a → Tree a → Tree a
     
@@ -62,13 +64,15 @@ data Tree a = Leaf a
 
 **UNSUPPORTED: term-indexed datatypes**
 
+(For Agda users: We have renamed `Set` to `Type` in order to follow nomenclature in Haskell.)
+
 ### Records
 
 Data definitions with fields are represented by records on the Agda side.
 
 Agda:
 ```agda
-record Citation : Set where
+record Citation : Type where
     field
         id     : Int
         author : String
@@ -93,19 +97,19 @@ Data declaration using the `newtype` keyword can be created by adding a `newtype
 Agda:
 ```agda
 -- data newtype
-data Indexed (a : Set) : Set where
+data Indexed (a : Type) : Type where
     MkIndexed : Int × a → Indexed a
 
 {-# COMPILE AGDA2HS Indexed newtype #-}
 
 -- data newtype with deriving
-data Pair (a b : Set) : Set where
+data Pair (a b : Type) : Type where
     MkPair : a × b → Pair a b
 
 {-# COMPILE AGDA2HS Pair newtype deriving ( Show, Eq ) #-}
 
 -- record newtype
-record Identity (a : Set) : Set where
+record Identity (a : Type) : Type where
     constructor MkIdentity
     field
         runIdentity : a
@@ -114,7 +118,7 @@ open Identity public
 {-# COMPILE AGDA2HS Identity newtype #-}
 
 -- record newtype with erased proof
-record Equal (a : Set) : Set where
+record Equal (a : Type) : Type where
     constructor MkEqual
     field
         pair : a × a
@@ -144,7 +148,7 @@ Unfortunately, Agda does not allow the constructor name to be the same as the da
 However, it _is_ possible to achieve this with Agda2HS if you do not explicitly add a constructor name to a record definition (this requires the use of `record { ... }` syntax on the Agda side):
 
 ```agda
-record Duo (a : Set) : Set where
+record Duo (a : Type) : Type where
     field
         duo : a × a
 open Duo public
@@ -243,7 +247,7 @@ The type signatures of both `if_then_else_` and `case_of_` on the Agda side cont
 
 This allows for the following Agda code to type check:
 ```agda
-data Range : Set where
+data Range : Type where
     MkRange : (low high : Int)
             → {{ @0 h : ((low <= high) ≡ True) }}
             → Range
@@ -303,7 +307,7 @@ Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default
 
 Agda:
 ```agda
-data GhostInt : Set where
+data GhostInt : Type where
     MakeGhostInt : @0 Int → GhostInt
 
 -- fails
@@ -327,7 +331,7 @@ addGhostInts MakeGhostInt MakeGhostInt = MakeGhostInt
 
 Agda:
 ```agda
-data Stream (a : Set) (@0 i : Size) : Set where
+data Stream (a : Type) (@0 i : Size) : Type where
     Nil : Stream a i
     Cons : a → Thunk (Stream a) i → Stream a i
 {-# COMPILE AGDA2HS Stream #-}
@@ -351,7 +355,7 @@ To construct an instance of a type class, you can simply do the following:
 
 Agda:
 ```agda
-record Circle : Set where
+record Circle : Type where
     constructor MkCircle
     field
         radius : Int
@@ -379,7 +383,7 @@ In this case, you can also implement the `IsLawful` instance for the data type a
 
 Agda:
 ```agda
-record Equal (a : Set) : Set where
+record Equal (a : Type) : Type where
     constructor MkEqual
     field
         pair : a × a
@@ -425,17 +429,17 @@ constructEqualCircle c d = constructEqual c d
 
 Agda:
 ```agda
-record Class1 (a : Set) : Set where
+record Class1 (a : Type) : Type where
     field
         field1 : a
 {-# COMPILE AGDA2HS Class1 class #-}
 
-record Class2 (a : Set) : Set where
+record Class2 (a : Type) : Type where
     field
         field2 : a
 {-# COMPILE AGDA2HS Class2 class #-}
 
-class1-implies-class2 (a : Set) : Class1 a → Class2 a
+class1-implies-class2 (a : Type) : Class1 a → Class2 a
 class1-implies-class2 _ class1 = record { field2 = class1.field1 }
 {-# COMPILE AGDA2HS class1-implies-class2 #-}
 ```
@@ -456,12 +460,12 @@ instance Class1 a => Class2 a where
 
 Agda:
 ```agda
-record Class1 (a : Set) : Set where
+record Class1 (a : Type) : Type where
     field
         field1 : a
 {-# COMPILE AGDA2HS Class1 class #-}
 
-record Class2 (a : Set) : Set where
+record Class2 (a : Type) : Type where
     field
         overlap ⦃ super ⦄ : ClassA b
         field2 : a
@@ -481,18 +485,18 @@ class Class1 a => Class2 a where
 
 Agda:
 ```agda
-record Ord (a : Set) : Set where
+record Ord (a : Type) : Type where
   field
     _<_ _>_ : a → a → Bool
 
-record Ord₁ (a : Set) : Set where
+record Ord₁ (a : Type) : Type where
   field
     _<_ : a → a → Bool
 
   _>_ : a → a → Bool
   x > y = y < x
 
-record Ord₂ (a : Set) : Set where
+record Ord₂ (a : Type) : Type where
   field
     _>_ : a → a → Bool
 
@@ -530,7 +534,7 @@ used to define fields of typeclass instances, for example:
 
 Agda:
 ```agda
-record HasId (a : Set)  : Set where
+record HasId (a : Type) : Type where
     field id : a → a
 {-# COMPILE AGDA2HS HasId class #-}
 
@@ -553,7 +557,7 @@ instance HasId () where
 If the derived instance is not needed on the Agda side and needs to only be generated in Haskell, the deriving clause can simply be added to the compilation pragma (this also works with the `newtype` pragma):
 
 ```agda
-data Planet : Set where
+data Planet : Type where
   Mercury : Planet
   Venus   : Planet
   Earth   : Planet
@@ -618,7 +622,7 @@ This is also possible with more complicated instance definitions, such as in the
 
 Agda:
 ```agda
-data Optional (a : Set) : Set where
+data Optional (a : Type) : Type where
   Of    : a → Optional a
   Empty : Optional a
 
@@ -645,7 +649,7 @@ postulate instance iPlanetShow : Show Planet
 
 {-# COMPILE AGDA2HS iPlanetShow derive stock #-}
 
-record Clazz (a : Set) : Set where
+record Clazz (a : Type) : Type where
   field
     foo : a → Int
     bar : a → Bool
@@ -658,7 +662,7 @@ postulate instance iPlanetClazz : Clazz Planet
 
 {-# COMPILE AGDA2HS iPlanetClazz derive anyclass #-}
 
-data Duo (a b : Set) : Set where
+data Duo (a b : Type) : Type where
   MkDuo : (a × b) → Duo a b
 
 {-# COMPILE AGDA2HS Duo newtype #-}
@@ -734,7 +738,7 @@ Agda
 ```agda
 mutual
 
-  data Map (k : Set) (a : Set) : Set where
+  data Map (k : Type) (a : Type) : Type where
     Bin : (sz : Nat) → (kx : k) → (x : a)
           → (l : Map k a) → (r : Map k a)
           → {{@0 szVal : sz ≡ (size l) + (size r) + 1}}
@@ -742,7 +746,7 @@ mutual
     Tip : Map k a
   {-# COMPILE AGDA2HS Map #-}
 
-  size : {k a : Set} → Map k a → Nat
+  size : {k a : Type} → Map k a → Nat
   size Tip = 0
   size (Bin sz _ _ _ _) = sz
   {-# COMPILE AGDA2HS size #-}
@@ -762,7 +766,7 @@ size (Bin sz _ _ _ _) = sz
 
 Agda
 ```agda
-record ImplicitField (a : Set) : Set where
+record ImplicitField (a : Type) : Type where
     field
         aField : a
         @0 {anImplicitField} : a
diff --git a/docs/source/index.md b/docs/source/index.md
index 87ced1f1..93d2af2f 100644
--- a/docs/source/index.md
+++ b/docs/source/index.md
@@ -7,10 +7,10 @@ the following Agda program encodes well-formed binary search trees:
 ```agda
 open import Haskell.Prelude
 
-_≤_ : {{Ord a}} → a → a → Set
+_≤_ : {{Ord a}} → a → a → Type
 x ≤ y = (x <= y) ≡ True
 
-data BST (a : Set) {{@0 _ : Ord a}} (@0 lower upper : a) : Set where
+data BST (a : Type) {{@0 _ : Ord a}} (@0 lower upper : a) : Type where
   Leaf : (@0 pf : lower ≤ upper) → BST a lower upper
   Node : (x : a) (l : BST a lower x) (r : BST a x upper) → BST a lower upper
 
diff --git a/docs/source/tutorials.md b/docs/source/tutorials.md
index cb818eaf..8f3da393 100644
--- a/docs/source/tutorials.md
+++ b/docs/source/tutorials.md
@@ -43,7 +43,7 @@ open import Haskell.Prelude
 Entry = Int × List String
 
 --defining a datatype
-data Tree (a : Set) : Set where
+data Tree (a : Type) : Type where
     Leaf   : a → Tree a
     Branch : a → Tree a → Tree a → Tree a
 
@@ -120,7 +120,7 @@ Let's say we want to have a data type describing a triangle. A first attempt mig
 ```agda
 open import Haskell.Prelude
 
-data Triangle : Set where
+data Triangle : Type where
     MkTriangle : (alpha beta gamma : Nat)
            → Triangle
 
@@ -136,7 +136,7 @@ countBiggerThan xs b = length (filter (λ x → (x >= b)) xs)
 
 {-# COMPILE AGDA2HS countBiggerThan #-}
 
-data Triangle : Set where
+data Triangle : Type where
     MkTriangle : (alpha beta gamma : Nat)
         → ⦃ @0 h₁ : (((alpha + beta + gamma) == 180) ≡ True )⦄
         → @0 ⦃ ((countBiggerThan
@@ -210,7 +210,7 @@ isAscending (x ∷ y ∷ xs) = if x <= y then isAscending
 This function can be compiled to Haskell without any issue, however, when you try using it in proofs you can notice that it is not the most handy definition: since the different cases are anonymous, invoking them is not straightforward and might require defining more proof cases with additional assertions about the values input data (an example of which can be found [further in the tutorial](function-example)) A better definition might be a predicate, instead:
 
 ```agda
-data IsAscending₂ {a : Set} ⦃ iOrdA : Ord a ⦄ : List a → Set where
+data IsAscending₂ {a : Type} ⦃ iOrdA : Ord a ⦄ : List a → Type where
     Empty : IsAscending₂ []
     OneElem : (x : a) →  IsAscending₂ (x ∷ [])
     ManyElem : (x y : a) (xs : List a) 
diff --git a/lib/Haskell/Control/Exception.agda b/lib/Haskell/Control/Exception.agda
index 5c4323ae..5b9ed8ca 100644
--- a/lib/Haskell/Control/Exception.agda
+++ b/lib/Haskell/Control/Exception.agda
@@ -5,7 +5,7 @@ open import Haskell.Prim
 open import Haskell.Extra.Dec
 open import Haskell.Extra.Refinement
 
-assert : (@0 b : Set ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
+assert : (@0 b : Type ℓ) → {{Dec b}} → (@0 {{b}} → a) → a
 assert _ {{True  ⟨ p ⟩}} x = x {{p}}
 assert _ {{False ⟨ _ ⟩}} x = oops
   where postulate oops : _
diff --git a/lib/Haskell/Data/Maybe.agda b/lib/Haskell/Data/Maybe.agda
index e8353cd6..6a5a7ee5 100644
--- a/lib/Haskell/Data/Maybe.agda
+++ b/lib/Haskell/Data/Maybe.agda
@@ -14,7 +14,7 @@ fromJust : (x : Maybe a) → @0 {IsJust x} → a
 fromJust Nothing  = error "fromJust Nothing"
 fromJust (Just x) = x
 
-fromMaybe : {a : Set} → a → Maybe a → a
+fromMaybe : {a : Type} → a → Maybe a → a
 fromMaybe d Nothing = d
 fromMaybe _ (Just x) = x
 
diff --git a/lib/Haskell/Extra/Dec.agda b/lib/Haskell/Extra/Dec.agda
index dcc88e24..316b06a1 100644
--- a/lib/Haskell/Extra/Dec.agda
+++ b/lib/Haskell/Extra/Dec.agda
@@ -6,9 +6,9 @@ open import Agda.Primitive
 
 private variable
   ℓ : Level
-  P : Set
+  P : Type
 
-@0 Reflects : Set ℓ → Bool → Set ℓ
+@0 Reflects : Type ℓ → Bool → Type ℓ
 Reflects P True  = P
 Reflects P False = P → ⊥
 
@@ -31,11 +31,11 @@ mapReflects : ∀ {cond} → (a → b) → (b → a)
 mapReflects {cond = False} f g x = x ∘ g
 mapReflects {cond = True}  f g x = f x
 
-Dec : ∀ {ℓ} → @0 Set ℓ → Set ℓ
+Dec : ∀ {ℓ} → @0 Type ℓ → Type ℓ
 Dec P = ∃ Bool (Reflects P)
 {-# COMPILE AGDA2HS Dec inline #-}
 
-mapDec : {@0 a b : Set}
+mapDec : {@0 a b : Type}
        → @0 (a → b)
        → @0 (b → a)
        → Dec a → Dec b
diff --git a/lib/Haskell/Extra/Delay.agda b/lib/Haskell/Extra/Delay.agda
index 8f59c7ad..75f2c5ce 100644
--- a/lib/Haskell/Extra/Delay.agda
+++ b/lib/Haskell/Extra/Delay.agda
@@ -14,11 +14,11 @@ private variable
   x y z : a
   @0 i : Size
 
-data Delay (a : Set) (@0 i : Size) : Set where
+data Delay (a : Type) (@0 i : Size) : Type where
   now : a → Delay a i
   later : Thunk (Delay a) i → Delay a i
 
-data HasResult (x : a) : Delay a i → Set where
+data HasResult (x : a) : Delay a i → Type where
   now   : HasResult x (now x)
   later : HasResult x (y .force) → HasResult x (later y)
 
diff --git a/lib/Haskell/Extra/Erase.agda b/lib/Haskell/Extra/Erase.agda
index 1e66c6d1..499a9859 100644
--- a/lib/Haskell/Extra/Erase.agda
+++ b/lib/Haskell/Extra/Erase.agda
@@ -13,7 +13,7 @@ module Haskell.Extra.Erase where
     @0 x y : a
     @0 xs  : List a
 
-  record Erase (@0 a : Set ℓ) : Set ℓ where
+  record Erase (@0 a : Type ℓ) : Type ℓ where
     instance constructor iErased
     field @0 {{get}} : a
   open Erase public
@@ -22,7 +22,7 @@ module Haskell.Extra.Erase where
   pattern Erased x = iErased {{x}}
 
   infixr 4 ⟨_⟩_
-  record Σ0 (@0 a : Set) (b : @0 a → Set) : Set where
+  record Σ0 (@0 a : Type) (b : @0 a → Type) : Type where
     constructor ⟨_⟩_
     field
       @0 proj₁ : a
@@ -33,7 +33,7 @@ module Haskell.Extra.Erase where
   pattern <_> x = record { proj₁ = _ ; proj₂ = x }
 
   -- Resurrection of erased values
-  Rezz : (@0 x : a) → Set
+  Rezz : (@0 x : a) → Type
   Rezz x = ∃ _ (x ≡_)
 
   {-# COMPILE AGDA2HS Rezz inline #-}
@@ -45,7 +45,7 @@ module Haskell.Extra.Erase where
     rezz-id = rezz _
   {-# COMPILE AGDA2HS rezz-id inline #-}
 
-  rezzCong : {@0 a : Set} {@0 x : a} (f : a → b) → Rezz x → Rezz (f x)
+  rezzCong : {@0 a : Type} {@0 x : a} (f : a → b) → Rezz x → Rezz (f x)
   rezzCong f (x ⟨ p ⟩) = f x ⟨ cong f p ⟩
   {-# COMPILE AGDA2HS rezzCong inline #-}
 
@@ -71,7 +71,7 @@ module Haskell.Extra.Erase where
                    ne = subst NonEmpty p itsNonEmpty
   {-# COMPILE AGDA2HS rezzTail inline #-}
 
-  rezzErase : {@0 a : Set} {@0 x : a} → Rezz (Erased x)
+  rezzErase : {@0 a : Type} {@0 x : a} → Rezz (Erased x)
   rezzErase {x = x} = Erased x ⟨ refl ⟩
   {-# COMPILE AGDA2HS rezzErase inline #-}
 
diff --git a/lib/Haskell/Extra/Refinement.agda b/lib/Haskell/Extra/Refinement.agda
index 9ce9302a..920686b2 100644
--- a/lib/Haskell/Extra/Refinement.agda
+++ b/lib/Haskell/Extra/Refinement.agda
@@ -6,7 +6,7 @@ open import Agda.Primitive
 private variable
   ℓ ℓ′ : Level
 
-record ∃ (a : Set ℓ) (@0 P : a → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
+record ∃ (a : Type ℓ) (@0 P : a → Type ℓ′) : Type (ℓ ⊔ ℓ′) where
   constructor _⟨_⟩
   field
     value    : a
@@ -14,12 +14,12 @@ record ∃ (a : Set ℓ) (@0 P : a → Set ℓ′) : Set (ℓ ⊔ ℓ′) where
 open ∃ public
 {-# COMPILE AGDA2HS ∃ unboxed #-}
 
-mapRefine : {@0 P Q : a → Set ℓ} (@0 f : ∀ {x} → P x → Q x) → ∃ a P → ∃ a Q
+mapRefine : {@0 P Q : a → Type ℓ} (@0 f : ∀ {x} → P x → Q x) → ∃ a P → ∃ a Q
 mapRefine f (x ⟨ p ⟩) = x ⟨ f p ⟩
 
 {-# COMPILE AGDA2HS mapRefine transparent #-}
 
-refineMaybe : {@0 P : a → Set ℓ} 
+refineMaybe : {@0 P : a → Type ℓ} 
             → (mx : Maybe a) → @0 (∀ {x} → mx ≡ Just x → P x)
             → Maybe (∃ a P)
 refineMaybe Nothing f = Nothing
diff --git a/lib/Haskell/Extra/Sigma.agda b/lib/Haskell/Extra/Sigma.agda
index db345498..bf460e97 100644
--- a/lib/Haskell/Extra/Sigma.agda
+++ b/lib/Haskell/Extra/Sigma.agda
@@ -1,6 +1,8 @@
 module Haskell.Extra.Sigma where
 
-record Σ (a : Set) (b : @0 a → Set) : Set where
+open import Haskell.Prelude
+
+record Σ (a : Type) (b : @0 a → Type) : Type where
   constructor _,_
   field
     fst : a
@@ -10,7 +12,7 @@ open Σ public
 
 infix 2 Σ-syntax
 
-Σ-syntax : (a : Set) → (@0 a → Set) → Set
+Σ-syntax : (a : Type) → (@0 a → Type) → Type
 Σ-syntax = Σ
 {-# COMPILE AGDA2HS Σ-syntax inline #-}
 
diff --git a/lib/Haskell/Law/Applicative/Def.agda b/lib/Haskell/Law/Applicative/Def.agda
index 9c93b9c0..e3b2854c 100644
--- a/lib/Haskell/Law/Applicative/Def.agda
+++ b/lib/Haskell/Law/Applicative/Def.agda
@@ -9,7 +9,7 @@ open import Haskell.Prim.Tuple
 
 open import Haskell.Law.Functor
 
-record IsLawfulApplicative (F : Set → Set) ⦃ iAppF : Applicative F ⦄ : Set₁ where
+record IsLawfulApplicative (F : Type → Type) ⦃ iAppF : Applicative F ⦄ : Type₁ where
   field
     overlap ⦃ super ⦄ : IsLawfulFunctor F
 
@@ -17,15 +17,15 @@ record IsLawfulApplicative (F : Set → Set) ⦃ iAppF : Applicative F ⦄ : Set
     identity : (v : F a) → (pure id <*> v) ≡ v
 
     -- Composition: pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
-    composition : {a b c : Set} → (u : F (b → c)) (v : F (a → b)) (w : F a)
+    composition : {a b c : Type} → (u : F (b → c)) (v : F (a → b)) (w : F a)
       → (pure _∘_ <*> u <*> v <*> w) ≡ (u <*> (v <*> w))
 
     -- Homomorphism: pure f <*> pure x = pure (f x)
-    homomorphism : {a b : Set} → (f : a → b) (x : a)
+    homomorphism : {a b : Type} → (f : a → b) (x : a)
       → (Applicative._<*>_ iAppF (pure f) (pure x)) ≡ (pure (f x))
 
     -- Interchange: u <*> pure y = pure ($ y) <*> u
-    interchange : {a b : Set} → (u : F (a → b)) (y : a)
+    interchange : {a b : Type} → (u : F (a → b)) (y : a)
       → (u <*> (pure y)) ≡ (pure (_$ y) <*> u)
 
     -- fmap f x = pure f <*> x
diff --git a/lib/Haskell/Law/Applicative/List.agda b/lib/Haskell/Law/Applicative/List.agda
index c7caf4cf..8eb70c75 100644
--- a/lib/Haskell/Law/Applicative/List.agda
+++ b/lib/Haskell/Law/Applicative/List.agda
@@ -13,13 +13,13 @@ open import Haskell.Law.Functor.List
 open import Haskell.Law.List
 
 private
-  identityList : {a : Set} → (v : List a) → (pure id <*> v) ≡ v
+  identityList : {a : Type} → (v : List a) → (pure id <*> v) ≡ v
   identityList [] = refl
   identityList (x ∷ xs)
     rewrite identityList xs
     = refl
 
-  compositionList : {a b c : Set} → (u : List (b → c)) (v : List (a → b)) (w : List a)
+  compositionList : {a b c : Type} → (u : List (b → c)) (v : List (a → b)) (w : List a)
     → ((((pure _∘_) <*> u) <*> v) <*> w) ≡ (u <*> (v <*> w))
   compositionList [] _  _  = refl
   compositionList (u ∷ us) v w
@@ -28,14 +28,14 @@ private
       | compositionList us v w
     = refl 
 
-  interchangeList : {a b : Set} → (u : List (a → b)) → (y : a)
+  interchangeList : {a b : Type} → (u : List (a → b)) → (y : a)
     → (u <*> (pure y)) ≡ (pure (_$ y) <*> u)
   interchangeList [] _ = refl
   interchangeList (x ∷ xs) y
       rewrite interchangeList xs y
       = refl
 
-  functorList : {a b : Set} → (f : a → b) → (x : List a)
+  functorList : {a b : Type} → (f : a → b) → (x : List a)
     → (fmap f x) ≡ ((pure f) <*> x)
   functorList _ [] = refl
   functorList f (x ∷ xs)
diff --git a/lib/Haskell/Law/Def.agda b/lib/Haskell/Law/Def.agda
index 1099dcf6..0a428a17 100644
--- a/lib/Haskell/Law/Def.agda
+++ b/lib/Haskell/Law/Def.agda
@@ -2,5 +2,5 @@ module Haskell.Law.Def where
 
 open import Haskell.Prim
 
-Injective : (a → b) → Set _
+Injective : (a → b) → Type _
 Injective f = ∀ {x y} → f x ≡ f y → x ≡ y
diff --git a/lib/Haskell/Law/Eq/Def.agda b/lib/Haskell/Law/Eq/Def.agda
index 0d519207..2700e541 100644
--- a/lib/Haskell/Law/Eq/Def.agda
+++ b/lib/Haskell/Law/Eq/Def.agda
@@ -12,7 +12,7 @@ open import Haskell.Extra.Refinement
 open import Haskell.Law.Bool
 open import Haskell.Law.Equality
 
-record IsLawfulEq (e : Set) ⦃ iEq : Eq e ⦄ : Set₁ where
+record IsLawfulEq (e : Type) ⦃ iEq : Eq e ⦄ : Type₁ where
   field
     isEquality : ∀ (x y : e) → Reflects (x ≡ y) (x == y)
 
diff --git a/lib/Haskell/Law/Equality.agda b/lib/Haskell/Law/Equality.agda
index 2d307bdc..13d40683 100644
--- a/lib/Haskell/Law/Equality.agda
+++ b/lib/Haskell/Law/Equality.agda
@@ -4,7 +4,7 @@ open import Haskell.Prim
 
 open import Agda.Builtin.TrustMe
 
-_≠_ : {A : Set} → A → A → Set
+_≠_ : {A : Type} → A → A → Type
 _≠_ a b = a ≡ b → ⊥
 
 infix 4 _≠_
@@ -12,25 +12,25 @@ infix 4 _≠_
 --------------------------------------------------
 -- Basic Laws
 
-cong : {A B : Set} → ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
+cong : {A B : Type} → ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
 cong f refl = refl
 
 cong₂ : ∀ (f : a → b → c) {x y u v} → x ≡ y → u ≡ v → f x u ≡ f y v
 cong₂ f refl refl = refl
 
-sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
+sym : ∀ {A : Type} {x y : A} → x ≡ y → y ≡ x
 sym refl = refl
 
-trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans : ∀ {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans refl refl = refl
 
-subst : ∀ {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y
+subst : ∀ {A : Type} (P : A → Type) {x y : A} → x ≡ y → P x → P y
 subst P refl z = z
 
 --------------------------------------------------
 -- Scary Things
 
-trustMe : ∀ {a} {A : Set a} {x y : A} → x ≡ y
+trustMe : ∀ {a} {A : Type a} {x y : A} → x ≡ y
 trustMe = primTrustMe
 
 --------------------------------------------------
@@ -62,6 +62,6 @@ syntax step-≡˘ x y≡z y≡x = x ≡˘⟨ y≡x ⟩ y≡z
 -------------------------------------------------
 -- Utility Functions
 
-subst0 : {@0 a : Set} (@0 p : @0 a → Set) {@0 x y : a} → @0 x ≡ y → p x → p y
+subst0 : {@0 a : Type} (@0 p : @0 a → Type) {@0 x y : a} → @0 x ≡ y → p x → p y
 subst0 p refl z = z
 {-# COMPILE AGDA2HS subst0 transparent #-}
diff --git a/lib/Haskell/Law/Function.agda b/lib/Haskell/Law/Function.agda
index 6bcd1a66..b0c711af 100644
--- a/lib/Haskell/Law/Function.agda
+++ b/lib/Haskell/Law/Function.agda
@@ -10,25 +10,25 @@ This says that two functions produce the same
 result for all input values.
 -}
 infix 4 _≗_
-_≗_ : ∀ {A B : Set} (f g : A → B) → Set
+_≗_ : ∀ {A B : Type} (f g : A → B) → Type
 f ≗ g = ∀ a → f a ≡ g a
 
-Commutative : {a : Set} → (a → a → a) → Set
+Commutative : {a : Type} → (a → a → a) → Type
 Commutative _+_ = ∀ x y → x + y ≡ y + x
 
-Associative : {a : Set} → (a → a → a) → Set
+Associative : {a : Type} → (a → a → a) → Type
 Associative _+_ = ∀ x y z → (x + y) + z ≡ x + (y + z)
 
-Identityˡ : {a : Set} → (a → a → a) → a → Set
+Identityˡ : {a : Type} → (a → a → a) → a → Type
 Identityˡ _+_ 𝟘 = ∀ x → 𝟘 + x ≡ x
 
-Identityʳ : {a : Set} → (a → a → a) → a → Set
+Identityʳ : {a : Type} → (a → a → a) → a → Type
 Identityʳ _+_ 𝟘 = ∀ x → x + 𝟘 ≡ x
 
-Distributiveˡ : {a : Set} → (_+_ : a → a → a) → (_*_ : a → a → a) → Set
+Distributiveˡ : {a : Type} → (_+_ : a → a → a) → (_*_ : a → a → a) → Type
 Distributiveˡ _+_ _*_ = ∀ x y z → x * (y + z) ≡ (x * y) + (x * z)
 
-Distributiveʳ : {a : Set} → (_+_ : a → a → a) → (_*_ : a → a → a) → Set
+Distributiveʳ : {a : Type} → (_+_ : a → a → a) → (_*_ : a → a → a) → Type
 Distributiveʳ _+_ _*_ =  ∀ x y z → (y + z) * x ≡ (y * x) + (z * x)
 
 {-|
@@ -37,8 +37,8 @@ A function φ is homomorphic w.r.t. some function or structure f
 when it preserves this structure in its target domain b
 (where this structure is called g).
 -}
-Homomorphism₁ : ∀ {a b : Set} (f : a → a) (g : b → b)
-  → (φ : a → b) → Set
+Homomorphism₁ : ∀ {a b : Type} (f : a → a) (g : b → b)
+  → (φ : a → b) → Type
 Homomorphism₁ f g φ = φ ∘ f ≗ g ∘ φ
 
 {-|
@@ -47,21 +47,21 @@ A function φ is homomorphic w.r.t. some structure _+ᵃ_
 when it preserves this structure in its target domain b
 (where this structure is called _+ᵇ_).
 -}
-Homomorphism₂ : ∀ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b)
-  → (φ : a → b) → Set
+Homomorphism₂ : ∀ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b)
+  → (φ : a → b) → Type
 Homomorphism₂ _+ᵃ_ _+ᵇ_ φ = ∀ x y → φ (x +ᵃ y) ≡ φ x +ᵇ φ y
 
-record Embedding₂ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) : Set where
+record Embedding₂ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) : Type where
   field
     hom   : Homomorphism₂ _+ᵃ_ _+ᵇ_ φ
     embed : φ⁻¹ ∘ φ ≗ id
 
-record MonoidEmbedding₂ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) (0ᵃ : a) (0ᵇ : b) : Set where
+record MonoidEmbedding₂ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) (0ᵃ : a) (0ᵇ : b) : Type where
   field
     embedding : Embedding₂ _+ᵃ_ _+ᵇ_ φ φ⁻¹
     0-hom     : φ 0ᵃ ≡ 0ᵇ
 
-map-comm : ∀ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a)
+map-comm : ∀ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a)
   → Embedding₂ _+ᵃ_ _+ᵇ_ φ φ⁻¹
   → Commutative _+ᵇ_
   → Commutative _+ᵃ_
@@ -82,7 +82,7 @@ map-comm _+ᵃ_ _+ᵇ_ φ φ⁻¹ proj comm x y =
   where
     open Embedding₂ proj
 
-map-assoc : ∀ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a)
+map-assoc : ∀ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a)
   → Embedding₂ _+ᵃ_ _+ᵇ_ φ φ⁻¹
   → Associative _+ᵇ_
   → Associative _+ᵃ_
@@ -107,7 +107,7 @@ map-assoc _+ᵃ_ _+ᵇ_ φ φ⁻¹ proj assoc x y z =
   where
     open Embedding₂ proj
 
-map-idˡ : ∀ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) (0ᵃ : a) (0ᵇ : b)
+map-idˡ : ∀ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) (0ᵃ : a) (0ᵇ : b)
   → MonoidEmbedding₂ _+ᵃ_ _+ᵇ_ φ φ⁻¹ 0ᵃ 0ᵇ
   → Identityˡ _+ᵇ_ 0ᵇ
   → Identityˡ _+ᵃ_ 0ᵃ
@@ -122,7 +122,7 @@ map-idˡ _+ᵃ_ _+ᵇ_ f g 0ᵃ 0ᵇ membed idˡ x =
     open MonoidEmbedding₂ membed
     open Embedding₂ embedding
 
-map-idʳ : ∀ {a b : Set} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) (0ᵃ : a) (0ᵇ : b)
+map-idʳ : ∀ {a b : Type} (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b) (φ : a → b) (φ⁻¹ : b → a) (0ᵃ : a) (0ᵇ : b)
   → MonoidEmbedding₂ _+ᵃ_ _+ᵇ_ φ φ⁻¹ 0ᵃ 0ᵇ
   → Identityʳ _+ᵇ_ 0ᵇ
   → Identityʳ _+ᵃ_ 0ᵃ
@@ -137,7 +137,7 @@ map-idʳ _+ᵃ_ _+ᵇ_ f g 0ᵃ 0ᵇ membed idʳ x =
     open MonoidEmbedding₂ membed
     open Embedding₂ embedding
 
-module _ {a b : Set}
+module _ {a b : Type}
   (_+ᵃ_ : a → a → a) (_+ᵇ_ : b → b → b)
   (_*ᵃ_ : a → a → a) (_*ᵇ_ : b → b → b)
   (f : a → b) (g : b → a)
diff --git a/lib/Haskell/Law/Functor/Def.agda b/lib/Haskell/Law/Functor/Def.agda
index 6ba05fb8..70cea0f7 100644
--- a/lib/Haskell/Law/Functor/Def.agda
+++ b/lib/Haskell/Law/Functor/Def.agda
@@ -5,7 +5,7 @@ open import Haskell.Prim.Tuple
 
 open import Haskell.Prim.Functor
 
-record IsLawfulFunctor (F : Set → Set) ⦃ iFuncF : Functor F ⦄ : Set₁ where
+record IsLawfulFunctor (F : Type → Type) ⦃ iFuncF : Functor F ⦄ : Type₁ where
   field
     -- Identity: fmap id == id
     identity : (fa : F a) → (fmap id) fa ≡ id fa
diff --git a/lib/Haskell/Law/List.agda b/lib/Haskell/Law/List.agda
index 4bf7efd5..05432bb8 100644
--- a/lib/Haskell/Law/List.agda
+++ b/lib/Haskell/Law/List.agda
@@ -44,7 +44,7 @@ map-concatMap f (x ∷ xs)
   rewrite map-concatMap f xs
   = refl
 
-map-<*>-recomp : {a b c : Set} → (xs : List (a → b)) → (ys : List a) → (u : (b → c))  
+map-<*>-recomp : {a b c : Type} → (xs : List (a → b)) → (ys : List a) → (u : (b → c))  
   → ((map (u ∘_) xs) <*> ys) ≡ map u (xs <*> ys)
 map-<*>-recomp [] _ _  = refl
 map-<*>-recomp (x ∷ xs) ys u 
diff --git a/lib/Haskell/Law/Monad/Def.agda b/lib/Haskell/Law/Monad/Def.agda
index 4f939dbf..a2d8f2e9 100644
--- a/lib/Haskell/Law/Monad/Def.agda
+++ b/lib/Haskell/Law/Monad/Def.agda
@@ -10,28 +10,28 @@ open import Haskell.Prim.Tuple
 
 open import Haskell.Law.Applicative
 
-record IsLawfulMonad (F : Set → Set) ⦃ iMonadF : Monad F ⦄ : Set₁ where
+record IsLawfulMonad (F : Type → Type) ⦃ iMonadF : Monad F ⦄ : Type₁ where
   field
     overlap ⦃ super ⦄ : IsLawfulApplicative F
 
     -- Left identity: return a >>= k = k a
-    leftIdentity : {a : Set} → (a' : a) (k : a → F b) → ((return a') >>= k) ≡ k a'
+    leftIdentity : {a : Type} → (a' : a) (k : a → F b) → ((return a') >>= k) ≡ k a'
 
     -- Right identity: m >>= return = m
-    rightIdentity : {a : Set} → (ma : F a) → (ma >>= return) ≡ ma
+    rightIdentity : {a : Type} → (ma : F a) → (ma >>= return) ≡ ma
 
     -- Associativity: m >>= (\x -> k x >>= h) = (m >>= k) >>= h
-    associativity : {a b c : Set} → (ma : F a) (f : a → F b) (g : b → F c)
+    associativity : {a b c : Type} → (ma : F a) (f : a → F b) (g : b → F c)
       → (ma >>= (λ x → f x >>= g)) ≡ ((ma >>= f) >>= g)
 
     -- pure = return
     pureIsReturn : (a' : a) → pure a' ≡ (Monad.return iMonadF a')
     -- m1 <*> m2 = m1 >>= (\x1 -> m2 >>= (\x2 -> return (x1 x2)))
-    sequence2bind : {a b : Set} → (mab : F (a → b)) (ma : F a)
+    sequence2bind : {a b : Type} → (mab : F (a → b)) (ma : F a)
       → (mab <*> ma) ≡ (mab >>= (λ x1 → (ma >>= (λ x2 → return (x1 x2)))))
 
     -- fmap f xs  =  xs >>= return . f
-    fmap2bind : {a b : Set} → (f : a → b) (ma : F a)
+    fmap2bind : {a b : Type} → (f : a → b) (ma : F a)
       → fmap f ma ≡ (ma >>= (return ∘ f))
     -- (>>) = (*>)
     rSequence2rBind : (ma : F a) → (mb : F b) → (ma *> mb) ≡ (ma >> mb)
diff --git a/lib/Haskell/Law/Monoid/Def.agda b/lib/Haskell/Law/Monoid/Def.agda
index 75383919..880d8e93 100644
--- a/lib/Haskell/Law/Monoid/Def.agda
+++ b/lib/Haskell/Law/Monoid/Def.agda
@@ -8,7 +8,7 @@ open import Haskell.Prim.Monoid
 
 open import Haskell.Law.Semigroup.Def
 
-record IsLawfulMonoid (a : Set) ⦃ iMonoidA : Monoid a ⦄ : Set₁ where
+record IsLawfulMonoid (a : Type) ⦃ iMonoidA : Monoid a ⦄ : Type₁ where
   field
     overlap ⦃ super ⦄ : IsLawfulSemigroup a
 
diff --git a/lib/Haskell/Law/Nat.agda b/lib/Haskell/Law/Nat.agda
index 23853a34..5e4dea03 100644
--- a/lib/Haskell/Law/Nat.agda
+++ b/lib/Haskell/Law/Nat.agda
@@ -13,7 +13,7 @@ suc-injective refl = refl
 The canonical formalization of the
 less-than-or-equal-to relation for natural numbers.
 -}
-data _≤_ : Nat → Nat → Set where
+data _≤_ : Nat → Nat → Type where
   z≤n : ∀ {n}                 → zero  ≤ n
   s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
 
diff --git a/lib/Haskell/Law/Num/Def.agda b/lib/Haskell/Law/Num/Def.agda
index 8d92da0a..e67738c2 100644
--- a/lib/Haskell/Law/Num/Def.agda
+++ b/lib/Haskell/Law/Num/Def.agda
@@ -4,7 +4,7 @@ open import Haskell.Prim
 open import Haskell.Prim.Num
 open import Haskell.Prim.Integer
 
-record IsLawfulNum (a : Set) ⦃ iNum : Num a ⦄ : Set₁ where
+record IsLawfulNum (a : Type) ⦃ iNum : Num a ⦄ : Type₁ where
   field
     +-assoc : ∀ (x y z : a) → (x + y) + z ≡ x + (y + z)
 
@@ -40,7 +40,7 @@ A number homomorphism establishes a homomorphism from one Num type a to another
 In particular, zero and one are mapped to zero and one in the other Num type,
 and addition, multiplication, and negation are homorphic.
 -}
-record NumHomomorphism (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) : Set where
+record NumHomomorphism (a b : Type) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) : Type where
   0ᵃ = Num.fromInteger iNuma (pos 0)
   0ᵇ = Num.fromInteger iNumb (pos 0)
   1ᵃ = Num.fromInteger iNuma (pos 1)
@@ -59,7 +59,7 @@ record NumHomomorphism (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (
 {-|
 A number embedding is an invertible number homomorphism.
 -}
-record NumEmbedding (a b : Set) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) (φ⁻¹ : b → a) : Set where
+record NumEmbedding (a b : Type) ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄ (φ : a → b) (φ⁻¹ : b → a) : Type where
   field
     hom   : NumHomomorphism a b φ
     embed : φ⁻¹ ∘ φ ≗ id
@@ -87,7 +87,7 @@ Given an embedding from one number type a onto another one b,
 we can conclude that b satisfies the laws of Num if a satisfies the
 laws of Num.
 -}
-map-IsLawfulNum : ∀ {a b : Set} ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄
+map-IsLawfulNum : ∀ {a b : Type} ⦃ iNuma : Num a ⦄ ⦃ iNumb : Num b ⦄
   → (a2b : a → b) (b2a : b → a)
   → NumEmbedding a b a2b b2a
   → IsLawfulNum b
diff --git a/lib/Haskell/Law/Ord/Def.agda b/lib/Haskell/Law/Ord/Def.agda
index 4acb6fe4..c092663d 100644
--- a/lib/Haskell/Law/Ord/Def.agda
+++ b/lib/Haskell/Law/Ord/Def.agda
@@ -19,7 +19,7 @@ open import Haskell.Law.Eq
 open import Haskell.Law.Bool
 open import Haskell.Law.Equality
 
-record IsLawfulOrd (a : Set) ⦃ iOrd : Ord a ⦄ : Set₁ where
+record IsLawfulOrd (a : Type) ⦃ iOrd : Ord a ⦄ : Type₁ where
   field
     overlap ⦃ super ⦄ : IsLawfulEq a
 
diff --git a/lib/Haskell/Law/Semigroup/Def.agda b/lib/Haskell/Law/Semigroup/Def.agda
index ea91ead3..d743fcee 100644
--- a/lib/Haskell/Law/Semigroup/Def.agda
+++ b/lib/Haskell/Law/Semigroup/Def.agda
@@ -5,7 +5,7 @@ open import Haskell.Prim.Tuple
 
 open import Haskell.Prim.Monoid
 
-record IsLawfulSemigroup (a : Set) ⦃ iSemigroupA : Semigroup a ⦄ : Set₁ where
+record IsLawfulSemigroup (a : Type) ⦃ iSemigroupA : Semigroup a ⦄ : Type₁ where
   field
     -- Associativity: x <> (y <> z) = (x <> y) <> z
     associativity : (x y z : a) → x <> (y <> z) ≡ (x <> y) <> z
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
index 6b927785..dbe4b34e 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -3,7 +3,8 @@ module Haskell.Prelude where
 
 open import Haskell.Prim
 open Haskell.Prim public using
-  ( Bool; True; False; Char; Integer;
+  ( Type;
+    Bool; True; False; Char; Integer;
     List; []; _∷_; Nat; zero; suc; ⊤; tt;
     TypeError; ⊥; iNumberNat; lengthNat;
     IsTrue; IsFalse; NonEmpty;
@@ -133,7 +134,7 @@ lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
 coerce : @0 a ≡ b → a → b
 coerce refl x = x
 
-IsJust : Maybe a → Set
+IsJust : Maybe a → Type
 IsJust Nothing  = ⊥
 IsJust (Just _) = ⊤
 
diff --git a/lib/Haskell/Prim.agda b/lib/Haskell/Prim.agda
index 94426a8c..84782ab5 100644
--- a/lib/Haskell/Prim.agda
+++ b/lib/Haskell/Prim.agda
@@ -7,7 +7,7 @@
 
 module Haskell.Prim where
 
-open import Agda.Primitive          public
+open import Agda.Primitive          public renaming (Set to Type)
 open import Agda.Builtin.Bool       public renaming (true to True; false to False)
 open import Agda.Builtin.Int        public renaming (Int to Integer)
 open import Agda.Builtin.Nat        public renaming (_==_ to eqNat; _<_ to ltNat; _+_ to addNat; _-_ to monusNat; _*_ to mulNat)
@@ -24,8 +24,8 @@ open import Agda.Builtin.List       public
 
 variable
   @0 ℓ : Level
-  a b c d e : Set
-  f m s t : Set → Set
+  a b c d e : Type
+  f m s t : Type → Type
 
 
 --------------------------------------------------
@@ -57,12 +57,12 @@ case_of_ : (a' : a) → ((a'' : a) → @0 {{ a' ≡ a'' }} → b) → b
 case x of f = f x
 
 infix -2 if_then_else_
-if_then_else_ : {@0 a : Set ℓ} → (flg : Bool) → (@0 {{ flg ≡ True }} → a) → (@0 {{ flg ≡ False }} → a) → a
+if_then_else_ : {@0 a : Type ℓ} → (flg : Bool) → (@0 {{ flg ≡ True }} → a) → (@0 {{ flg ≡ False }} → a) → a
 if False then x else y = y
 if True  then x else y = x
 
 -- for explicit type signatures (e. g. `4 :: Integer` is `the Int 4`)
-the : (@0 a : Set ℓ) -> a -> a
+the : (@0 a : Type ℓ) -> a -> a
 the _ x = x
 
 --------------------------------------------------
@@ -94,9 +94,9 @@ lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs)
 --------------------------------------------------
 -- Proof things
 
-data ⊥ : Set where
+data ⊥ : Type where
 
-magic : {A : Set} → ⊥ → A
+magic : {A : Type} → ⊥ → A
 magic ()
 
 --principle of explosion
@@ -105,26 +105,26 @@ exFalso {False} () b
 exFalso {True} a ()
 
 -- Use to bundle up constraints
-data All {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+data All {a b} {A : Type a} (B : A → Type b) : List A → Type (a ⊔ b) where
   instance
     allNil  : All B []
     allCons : ∀ {x xs} ⦃ i : B x ⦄ ⦃ is : All B xs ⦄ → All B (x ∷ xs)
 
-data Any {a b} {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
+data Any {a b} {A : Type a} (B : A → Type b) : List A → Type (a ⊔ b) where
   instance
     anyHere  : ∀ {x xs} ⦃ i : B x ⦄ → Any B (x ∷ xs)
     anyThere : ∀ {x xs} ⦃ is : Any B xs ⦄ → Any B (x ∷ xs)
 
-data IsTrue : Bool → Set where
+data IsTrue : Bool → Type where
   instance itsTrue : IsTrue True
 
-data IsFalse : Bool → Set where
+data IsFalse : Bool → Type where
   instance itsFalse : IsFalse False
 
-data NonEmpty {a : Set} : List a → Set where
+data NonEmpty {a : Type} : List a → Type where
   instance itsNonEmpty : ∀ {x xs} → NonEmpty (x ∷ xs)
 
-data TypeError (err : AgdaString) : Set where
+data TypeError (err : AgdaString) : Type where
 
-it : ∀ {@0 ℓ} {@0 a : Set ℓ} → ⦃ a ⦄ → a
+it : ∀ {@0 ℓ} {@0 a : Type ℓ} → ⦃ a ⦄ → a
 it ⦃ x ⦄ = x
diff --git a/lib/Haskell/Prim/Applicative.agda b/lib/Haskell/Prim/Applicative.agda
index 20c7aba2..2629f90e 100644
--- a/lib/Haskell/Prim/Applicative.agda
+++ b/lib/Haskell/Prim/Applicative.agda
@@ -15,7 +15,7 @@ open import Haskell.Prim.Tuple
 -- Applicative
 
 -- ** base
-record Applicative (f : Set → Set) : Set₁ where
+record Applicative (f : Type → Type) : Type₁ where
   infixl 4 _<*>_ _<*_ _*>_
   field
     pure  : a → f a
@@ -24,7 +24,7 @@ record Applicative (f : Set → Set) : Set₁ where
     _<*_ : f a → f b → f a
     _*>_ : f a → f b → f b
 -- ** defaults
-record DefaultApplicative (f : Set → Set) : Set₁ where
+record DefaultApplicative (f : Type → Type) : Type₁ where
   constructor mk
   infixl 4 _<*>_ _<*_ _*>_
   field
diff --git a/lib/Haskell/Prim/Bounded.agda b/lib/Haskell/Prim/Bounded.agda
index 402dbfea..bd9ae0d5 100644
--- a/lib/Haskell/Prim/Bounded.agda
+++ b/lib/Haskell/Prim/Bounded.agda
@@ -12,15 +12,15 @@ open import Haskell.Prim.Word
 --------------------------------------------------
 -- Bounded
 
-record BoundedBelow (a : Set) : Set where
+record BoundedBelow (a : Type) : Type where
   field
     minBound : a
 
-record BoundedAbove (a : Set) : Set where
+record BoundedAbove (a : Type) : Type where
   field
     maxBound : a
 
-record Bounded (a : Set) : Set where
+record Bounded (a : Type) : Type where
   field
     overlap ⦃ below ⦄ : BoundedBelow a
     overlap ⦃ above ⦄ : BoundedAbove a
diff --git a/lib/Haskell/Prim/Either.agda b/lib/Haskell/Prim/Either.agda
index 6acd8e6a..ac50e97c 100644
--- a/lib/Haskell/Prim/Either.agda
+++ b/lib/Haskell/Prim/Either.agda
@@ -7,7 +7,7 @@ open import Haskell.Prim.Bool
 --------------------------------------------------
 -- Either
 
-data Either (a b : Set) : Set where
+data Either (a b : Type) : Type where
   Left  : a → Either a b
   Right : b → Either a b
 
diff --git a/lib/Haskell/Prim/Enum.agda b/lib/Haskell/Prim/Enum.agda
index eafa83fc..344d73af 100644
--- a/lib/Haskell/Prim/Enum.agda
+++ b/lib/Haskell/Prim/Enum.agda
@@ -24,37 +24,37 @@ open import Haskell.Prim.Word
 --    minBound and maxBound. Unbounded enums do not support enumFrom
 --    and enumFromThen (since they return infinite lists).
 
-@0 IfBoundedBelow : Maybe (BoundedBelow a) → (⦃ BoundedBelow a ⦄ → Set) → Set
+@0 IfBoundedBelow : Maybe (BoundedBelow a) → (⦃ BoundedBelow a ⦄ → Type) → Type
 IfBoundedBelow Nothing  k = ⊤
 IfBoundedBelow (Just i) k = k ⦃ i ⦄
 
-@0 IfBoundedAbove : Maybe (BoundedAbove a) → (⦃ BoundedAbove a ⦄ → Set) → Set
+@0 IfBoundedAbove : Maybe (BoundedAbove a) → (⦃ BoundedAbove a ⦄ → Type) → Type
 IfBoundedAbove Nothing  k = ⊤
 IfBoundedAbove (Just i) k = k ⦃ i ⦄
 
-record Enum (a : Set) : Set₁ where
+record Enum (a : Type) : Type₁ where
   field
     BoundedBelowEnum : Maybe (BoundedBelow a)
     BoundedAboveEnum : Maybe (BoundedAbove a)
     fromEnum         : a → Int
 
   private
-    @0 IsBoundedBelow : Set
+    @0 IsBoundedBelow : Type
     IsBoundedBelow = maybe ⊥ (λ _ → ⊤) BoundedBelowEnum
 
-    @0 IsBoundedAbove : Set
+    @0 IsBoundedAbove : Type
     IsBoundedAbove = maybe ⊥ (λ _ → ⊤) BoundedAboveEnum
 
-    @0 TrueIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
+    @0 TrueIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Type
     TrueIfLB C = IfBoundedBelow BoundedBelowEnum (IsTrue C)
 
-    @0 TrueIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
+    @0 TrueIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Type
     TrueIfUB C = IfBoundedAbove BoundedAboveEnum (IsTrue C)
 
-    @0 FalseIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Set
+    @0 FalseIfLB : (⦃ BoundedBelow a ⦄ → Bool) → Type
     FalseIfLB C = IfBoundedBelow BoundedBelowEnum (IsFalse C)
 
-    @0 FalseIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Set
+    @0 FalseIfUB : (⦃ BoundedAbove a ⦄ → Bool) → Type
     FalseIfUB C = IfBoundedAbove BoundedAboveEnum (IsFalse C)
 
     minInt : ⦃ BoundedBelow a ⦄ → Int
diff --git a/lib/Haskell/Prim/Eq.agda b/lib/Haskell/Prim/Eq.agda
index a710dbf8..4f844c75 100644
--- a/lib/Haskell/Prim/Eq.agda
+++ b/lib/Haskell/Prim/Eq.agda
@@ -15,7 +15,7 @@ open import Haskell.Prim.Either
 --------------------------------------------------
 -- Eq
 
-record Eq (a : Set) : Set where
+record Eq (a : Type) : Type where
   infix 4 _==_
   field
     _==_ : a → a → Bool
diff --git a/lib/Haskell/Prim/Foldable.agda b/lib/Haskell/Prim/Foldable.agda
index c94cf66b..3de5cc27 100644
--- a/lib/Haskell/Prim/Foldable.agda
+++ b/lib/Haskell/Prim/Foldable.agda
@@ -16,7 +16,7 @@ open import Haskell.Prim.Monoid
 -- Foldable
 
 -- ** base
-record Foldable (t : Set → Set) : Set₁ where
+record Foldable (t : Type → Type) : Type₁ where
   field
     foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
     foldr : (a → b → b) → b → t a → b
@@ -35,7 +35,7 @@ record Foldable (t : Set → Set) : Set₁ where
     product : ⦃ iNum : Num a ⦄ → t a → a
     length : t a → Int
 -- ** defaults
-record DefaultFoldable (t : Set → Set) : Set₁ where
+record DefaultFoldable (t : Type → Type) : Type₁ where
   module M = Foldable {t = t}
   field foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
 
diff --git a/lib/Haskell/Prim/Functor.agda b/lib/Haskell/Prim/Functor.agda
index f14924bc..c0847503 100644
--- a/lib/Haskell/Prim/Functor.agda
+++ b/lib/Haskell/Prim/Functor.agda
@@ -12,13 +12,13 @@ open import Haskell.Prim.Tuple
 -- Functor
 
 -- ** base
-record Functor (f : Set → Set) : Set₁ where
+record Functor (f : Type → Type) : Type₁ where
   infixl 4 _<$_
   field
     fmap : (a → b) → f a → f b
     _<$_ : (@0 {{ b }} → a) → f b → f a
 -- ** defaults
-record DefaultFunctor (f : Set → Set) : Set₁ where
+record DefaultFunctor (f : Type → Type) : Type₁ where
   field fmap : (a → b) → f a → f b
 
   infixl 4 _<$_
diff --git a/lib/Haskell/Prim/IO.agda b/lib/Haskell/Prim/IO.agda
index 5f92f561..b653e3c4 100644
--- a/lib/Haskell/Prim/IO.agda
+++ b/lib/Haskell/Prim/IO.agda
@@ -4,7 +4,7 @@ open import Haskell.Prim
 open import Haskell.Prim.Show
 open import Haskell.Prim.String
 
-postulate IO : ∀{a} → Set a → Set a
+postulate IO : ∀{a} → Type a → Type a
 
 FilePath = String
 
diff --git a/lib/Haskell/Prim/Int.agda b/lib/Haskell/Prim/Int.agda
index 4cc446ef..095940f5 100644
--- a/lib/Haskell/Prim/Int.agda
+++ b/lib/Haskell/Prim/Int.agda
@@ -14,7 +14,7 @@ open import Haskell.Prim.Bool
 --------------------------------------------------
 -- Definition
 
-data Int : Set where
+data Int : Type where
   int64 : Word64 → Int
 
 intToWord : Int → Word64
@@ -101,7 +101,7 @@ showInt a = showInteger (intToInteger a)
 --------------------------------------------------
 -- Constraints
 
-@0 IsNonNegativeInt : Int → Set
+@0 IsNonNegativeInt : Int → Type
 IsNonNegativeInt a@(int64 _) =
   if isNegativeInt a then TypeError (primStringAppend (primStringFromList (showInt a)) " is negative")
                      else ⊤
diff --git a/lib/Haskell/Prim/Integer.agda b/lib/Haskell/Prim/Integer.agda
index a18c86f5..3496b9c9 100644
--- a/lib/Haskell/Prim/Integer.agda
+++ b/lib/Haskell/Prim/Integer.agda
@@ -100,7 +100,7 @@ isNegativeInteger : Integer → Bool
 isNegativeInteger (pos _)    = False
 isNegativeInteger (negsuc _) = True
 
-@0 IsNonNegativeInteger : Integer → Set
+@0 IsNonNegativeInteger : Integer → Type
 IsNonNegativeInteger (pos _)      = ⊤
 IsNonNegativeInteger n@(negsuc _) =
   TypeError (primStringAppend (primShowInteger n) (" is negative"))
diff --git a/lib/Haskell/Prim/List.agda b/lib/Haskell/Prim/List.agda
index 7b02c556..8343eb61 100644
--- a/lib/Haskell/Prim/List.agda
+++ b/lib/Haskell/Prim/List.agda
@@ -15,7 +15,7 @@ map f []       = []
 map f (x ∷ xs) = f x ∷ map f xs
 
 infixr 5 _++_
-_++_ : ∀ {@0 ℓ} {@0 a : Set ℓ} → List a → List a → List a
+_++_ : ∀ {@0 ℓ} {@0 a : Type ℓ} → List a → List a → List a
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ xs ++ ys
 
diff --git a/lib/Haskell/Prim/Maybe.agda b/lib/Haskell/Prim/Maybe.agda
index bf261c3a..2142da9b 100644
--- a/lib/Haskell/Prim/Maybe.agda
+++ b/lib/Haskell/Prim/Maybe.agda
@@ -1,13 +1,14 @@
-
 module Haskell.Prim.Maybe where
 
+open import Haskell.Prim
+
 --------------------------------------------------
 -- Maybe
 
-data Maybe {@0 ℓ} (a : Set ℓ) : Set ℓ where
+data Maybe {@0 ℓ} (a : Type ℓ) : Type ℓ where
   Nothing : Maybe a
   Just    : a -> Maybe a
 
-maybe : ∀ {@0 ℓ₁ ℓ₂} {@0 a : Set ℓ₁} {@0 b : Set ℓ₂} → b → (a → b) → Maybe a → b
+maybe : ∀ {@0 ℓ₁ ℓ₂} {@0 a : Type ℓ₁} {@0 b : Type ℓ₂} → b → (a → b) → Maybe a → b
 maybe n j Nothing  = n
 maybe n j (Just x) = j x
diff --git a/lib/Haskell/Prim/Monad.agda b/lib/Haskell/Prim/Monad.agda
index 70dcd0cc..36204f36 100644
--- a/lib/Haskell/Prim/Monad.agda
+++ b/lib/Haskell/Prim/Monad.agda
@@ -19,14 +19,14 @@ open import Haskell.Prim.Tuple
 module Do where
 
   -- ** base
-  record Monad (m : Set → Set) : Set₁ where
+  record Monad (m : Type → Type) : Type₁ where
     field
       _>>=_ : m a → (a → m b) → m b
       overlap ⦃ super ⦄ : Applicative m
       return : a → m a
       _>>_ : m a → (@0 {{ a }} → m b) → m b
   -- ** defaults
-  record DefaultMonad (m : Set → Set) : Set₁ where
+  record DefaultMonad (m : Type → Type) : Type₁ where
     field
       _>>=_ : m a → (a → m b) → m b
       overlap ⦃ super ⦄ : Applicative m
@@ -112,7 +112,7 @@ instance
 
 instance postulate iMonadIO : Monad IO
 
-record MonadFail (m : Set → Set) : Set₁ where
+record MonadFail (m : Type → Type) : Type₁ where
   field
     fail : String → m a
     overlap ⦃ super ⦄ : Monad m
diff --git a/lib/Haskell/Prim/Monoid.agda b/lib/Haskell/Prim/Monoid.agda
index b5e20631..a011cd11 100644
--- a/lib/Haskell/Prim/Monoid.agda
+++ b/lib/Haskell/Prim/Monoid.agda
@@ -11,7 +11,7 @@ open import Haskell.Prim.Tuple
 --------------------------------------------------
 -- Semigroup
 
-record Semigroup (a : Set) : Set where
+record Semigroup (a : Type) : Type where
   infixr 6 _<>_
   field _<>_ : a → a → a
 open Semigroup ⦃...⦄ public
@@ -48,14 +48,14 @@ instance
 -- Monoid
 
 -- ** base
-record Monoid (a : Set) : Set where
+record Monoid (a : Type) : Type where
   field
     mempty : a
     overlap ⦃ super ⦄ : Semigroup a
     mappend : a → a → a
     mconcat : List a → a
 -- ** defaults
-record DefaultMonoid (a : Set) : Set where
+record DefaultMonoid (a : Type) : Type where
   field
     mempty : a
     overlap ⦃ super ⦄ : Semigroup a
diff --git a/lib/Haskell/Prim/Num.agda b/lib/Haskell/Prim/Num.agda
index c4283254..c7c6bb60 100644
--- a/lib/Haskell/Prim/Num.agda
+++ b/lib/Haskell/Prim/Num.agda
@@ -14,13 +14,13 @@ open import Haskell.Prim.Monoid
 --------------------------------------------------
 -- Num
 
-record Num (a : Set) : Set₁ where
+record Num (a : Type) : Type₁ where
   infixl 6 _+_ _-_
   infixl 7 _*_
   field
-    @0 MinusOK       : a → a → Set
-    @0 NegateOK      : a → Set
-    @0 FromIntegerOK : Integer → Set
+    @0 MinusOK       : a → a → Type
+    @0 NegateOK      : a → Type
+    @0 FromIntegerOK : Integer → Type
     _+_           : a → a → a
     _-_           : (x y : a) → @0 ⦃ MinusOK x y ⦄ → a
     _*_           : a → a → a
diff --git a/lib/Haskell/Prim/Ord.agda b/lib/Haskell/Prim/Ord.agda
index 29e29e4b..beda7476 100644
--- a/lib/Haskell/Prim/Ord.agda
+++ b/lib/Haskell/Prim/Ord.agda
@@ -17,7 +17,7 @@ open import Haskell.Prim.Either
 --------------------------------------------------
 -- Ordering
 
-data Ordering : Set where
+data Ordering : Type where
   LT EQ GT : Ordering
 
 instance
@@ -38,7 +38,7 @@ instance
 --------------------------------------------------
 -- Ord
 
-record Ord (a : Set) : Set where
+record Ord (a : Type) : Type where
   field
     compare : a → a → Ordering
     _<_  : a → a → Bool
@@ -51,7 +51,7 @@ record Ord (a : Set) : Set where
 
   infix 4 _<_ _>_ _<=_ _>=_
 
-record OrdFromCompare (a : Set) : Set where
+record OrdFromCompare (a : Type) : Type where
   field
     compare : a → a → Ordering
     overlap ⦃ super ⦄ : Eq a
@@ -74,7 +74,7 @@ record OrdFromCompare (a : Set) : Set where
   min  : a → a → a
   min x y = if compare x y == GT then y else x
 
-record OrdFromLessThan (a : Set) : Set where
+record OrdFromLessThan (a : Type) : Type where
   field
     _<_ : a → a → Bool
     overlap ⦃ super ⦄ : Eq a
diff --git a/lib/Haskell/Prim/Show.agda b/lib/Haskell/Prim/Show.agda
index 071e6d84..601512b1 100644
--- a/lib/Haskell/Prim/Show.agda
+++ b/lib/Haskell/Prim/Show.agda
@@ -20,7 +20,7 @@ open import Haskell.Prim.Foldable
 --------------------------------------------------
 -- Show
 
-ShowS : Set
+ShowS : Type
 ShowS = String → String
 
 showChar : Char → ShowS
@@ -41,13 +41,13 @@ defaultShowList shows = λ where
            ∘ showString "]"
 
 -- ** base
-record Show (a : Set) : Set where
+record Show (a : Type) : Type where
   field
     showsPrec : Int → a → ShowS
     showList  : List a → ShowS
     show      : a → String
 -- ** export
-record Show₁ (a : Set) : Set where
+record Show₁ (a : Type) : Type where
   field showsPrec : Int → a → ShowS
 
   show : a → String
@@ -55,7 +55,7 @@ record Show₁ (a : Set) : Set where
 
   showList : List a → ShowS
   showList = defaultShowList (showsPrec 0)
-record Show₂ (a : Set) : Set where
+record Show₂ (a : Type) : Type where
   field show : a → String
 
   showsPrec : Int → a → ShowS
diff --git a/lib/Haskell/Prim/Strict.agda b/lib/Haskell/Prim/Strict.agda
index a38cdcc0..5c2353be 100644
--- a/lib/Haskell/Prim/Strict.agda
+++ b/lib/Haskell/Prim/Strict.agda
@@ -3,7 +3,7 @@ module Haskell.Prim.Strict where
 
 open import Haskell.Prim
 
-record Strict (a : Set ℓ) : Set ℓ where
+record Strict (a : Type ℓ) : Type ℓ where
   constructor !_
   field
     force : a
diff --git a/lib/Haskell/Prim/Thunk.agda b/lib/Haskell/Prim/Thunk.agda
index 05372887..688a73fc 100644
--- a/lib/Haskell/Prim/Thunk.agda
+++ b/lib/Haskell/Prim/Thunk.agda
@@ -6,7 +6,7 @@ open import Agda.Builtin.Size public
 
 open import Haskell.Prim
 
-record Thunk {ℓ} (a : @0 Size → Set ℓ) (@0 i : Size) : Set ℓ where
+record Thunk {ℓ} (a : @0 Size → Type ℓ) (@0 i : Size) : Type ℓ where
   constructor delay
   coinductive
   field force : {@0 j : Size< i} → a j
diff --git a/lib/Haskell/Prim/Traversable.agda b/lib/Haskell/Prim/Traversable.agda
index 5ff9e6fd..0c97fbe7 100644
--- a/lib/Haskell/Prim/Traversable.agda
+++ b/lib/Haskell/Prim/Traversable.agda
@@ -16,7 +16,7 @@ open import Haskell.Prim.Tuple
 -- Traversable
 
 -- ** base
-record Traversable (t : Set → Set) : Set₁ where
+record Traversable (t : Type → Type) : Type₁ where
   field
     traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
     overlap ⦃ functor ⦄ : Functor t
@@ -26,7 +26,7 @@ record Traversable (t : Set → Set) : Set₁ where
     mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
     sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
 -- ** defaults
-record DefaultTraversable (t : Set → Set) : Set₁ where
+record DefaultTraversable (t : Type → Type) : Type₁ where
   field
     traverse : ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b)
     overlap ⦃ functor ⦄ : Functor t
diff --git a/lib/Haskell/Prim/Tuple.agda b/lib/Haskell/Prim/Tuple.agda
index b1235cbb..25900c11 100644
--- a/lib/Haskell/Prim/Tuple.agda
+++ b/lib/Haskell/Prim/Tuple.agda
@@ -10,7 +10,7 @@ infix 3 _×_ _×_×_
 
 infix -1 _,_ _,_,_
 
-record _×_ (a b : Set) : Set where
+record _×_ (a b : Type) : Type where
   constructor _,_
   field
     fst : a
@@ -19,7 +19,7 @@ open _×_ public
 
 {-# COMPILE AGDA2HS _×_ tuple #-}
 
-record _×_×_ (a b c : Set) : Set where
+record _×_×_ (a b c : Type) : Type where
   no-eta-equality; pattern
   constructor _,_,_
   field
diff --git a/test/BangPatterns.agda b/test/BangPatterns.agda
index 6ba035c1..fe8cce2b 100644
--- a/test/BangPatterns.agda
+++ b/test/BangPatterns.agda
@@ -19,13 +19,13 @@ foldl'' f (! x0) (x ∷ xs) = foldl'' f (! f x0 x) xs
 
 {-# COMPILE AGDA2HS foldl'' #-}
 
-data LazyMaybe (a : Set ℓ) : Set ℓ where
+data LazyMaybe (a : Type ℓ) : Type ℓ where
   LazyNothing : LazyMaybe a
   LazyJust    : a → LazyMaybe a
 
 {-# COMPILE AGDA2HS LazyMaybe #-}
 
-data StrictMaybe (a : Set ℓ) : Set ℓ where
+data StrictMaybe (a : Type ℓ) : Type ℓ where
   StrictNothing : StrictMaybe a
   StrictJust    : Strict a → StrictMaybe a
 
diff --git a/test/CanonicalInstance.agda b/test/CanonicalInstance.agda
index 1f92e732..e67d92c2 100644
--- a/test/CanonicalInstance.agda
+++ b/test/CanonicalInstance.agda
@@ -4,14 +4,14 @@ module _ where
 
 open import Haskell.Prelude
 
-record ClassA (a : Set) : Set where
+record ClassA (a : Type) : Type where
   field
     myA : a
 
 open ClassA ⦃ ... ⦄ public
 {-# COMPILE AGDA2HS ClassA class #-}
 
-record ClassB (b : Set) : Set where
+record ClassB (b : Type) : Type where
   field
     overlap ⦃ super ⦄ : ClassA b
 {-# COMPILE AGDA2HS ClassB class #-}
diff --git a/test/Coerce.agda b/test/Coerce.agda
index a71c6c2c..05c504b1 100644
--- a/test/Coerce.agda
+++ b/test/Coerce.agda
@@ -1,9 +1,9 @@
 open import Haskell.Prelude
 
-data A : Set where
+data A : Type where
   MkA : Nat → A
 
-data B : Set where
+data B : Type where
   MkB : Nat → B
 
 postulate A≡B : A ≡ B
diff --git a/test/Coinduction.agda b/test/Coinduction.agda
index 28644c84..a490e46b 100644
--- a/test/Coinduction.agda
+++ b/test/Coinduction.agda
@@ -5,7 +5,7 @@ module Coinduction where
 open import Haskell.Prelude
 open import Haskell.Prim.Thunk
 
-data Colist (a : Set) (@0 i : Size) : Set where
+data Colist (a : Type) (@0 i : Size) : Type where
   Nil  : Colist a i
   Cons : a -> Thunk (Colist a) i -> Colist a i
 
diff --git a/test/ConstrainedInstance.agda b/test/ConstrainedInstance.agda
index f7eba90e..60c68850 100644
--- a/test/ConstrainedInstance.agda
+++ b/test/ConstrainedInstance.agda
@@ -1,7 +1,7 @@
 
 open import Haskell.Prelude
 
-data D (a : Set) : Set where
+data D (a : Type) : Type where
   C : a → D a
 {-# COMPILE AGDA2HS D #-}
 
diff --git a/test/Cubical/StreamFusion.agda b/test/Cubical/StreamFusion.agda
index 499ddad2..e8b92648 100644
--- a/test/Cubical/StreamFusion.agda
+++ b/test/Cubical/StreamFusion.agda
@@ -2,7 +2,6 @@ module Cubical.StreamFusion where
 
 open import Haskell.Prelude
 
-open import Agda.Primitive
 open import Agda.Primitive.Cubical
 open import Agda.Builtin.Equality
 open import Agda.Builtin.Size
@@ -10,7 +9,7 @@ open import Agda.Builtin.Size
 variable
   @0 i : Size
 
-record Stream (a : Set) (@0 i : Size) : Set where
+record Stream (a : Type) (@0 i : Size) : Type where
   pattern; inductive; constructor _:>_
   field
     shead : a
diff --git a/test/CustomTuples.agda b/test/CustomTuples.agda
index 364c5b70..7a388885 100644
--- a/test/CustomTuples.agda
+++ b/test/CustomTuples.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-record Σ (a : Set) (b : @0 a → Set) : Set where
+record Σ (a : Type) (b : @0 a → Type) : Type where
   constructor _,_
   field
     fst : a
@@ -13,7 +13,7 @@ test xy = fst xy + snd xy
 
 {-# COMPILE AGDA2HS test #-}
 
-record Stuff (a : Set) : Set where
+record Stuff (a : Type) : Type where
   no-eta-equality; pattern
   constructor stuff
   field
@@ -38,7 +38,7 @@ section = stuff 42
 
 {-# COMPILE AGDA2HS section #-}
 
-record NoStuff : Set where
+record NoStuff : Type where
   no-eta-equality; pattern
   constructor dontlook
 
@@ -50,7 +50,7 @@ bar dontlook = dontlook
 {-# COMPILE AGDA2HS bar #-}
 
 -- This is legal, basically the same as an unboxed record.
-record Legal (a : Set) : Set where
+record Legal (a : Type) : Type where
   constructor mkLegal
   field
     theA : a
diff --git a/test/Datatypes.agda b/test/Datatypes.agda
index 054c1dd8..4e1fa65b 100644
--- a/test/Datatypes.agda
+++ b/test/Datatypes.agda
@@ -1,7 +1,7 @@
 
-open import Agda.Builtin.Bool
+open import Haskell.Prim using (Bool; Type)
 
-data Test : Set where
+data Test : Type where
   CTest : Bool -> @0 {Bool} -> Test
 {-# COMPILE AGDA2HS Test #-}
 
diff --git a/test/Default.agda b/test/Default.agda
index 51df4b70..50809d0a 100644
--- a/test/Default.agda
+++ b/test/Default.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-record HasDefault (a : Set) : Set where
+record HasDefault (a : Type) : Type where
   field
     theDefault : a
 open HasDefault {{...}}
diff --git a/test/DefaultMethods.agda b/test/DefaultMethods.agda
index 141744d8..150ef66a 100644
--- a/test/DefaultMethods.agda
+++ b/test/DefaultMethods.agda
@@ -14,18 +14,18 @@ import Prelude hiding (Show, show, showsPrec, showList, Ord, (<), (>))
 
 -- ** Ord
 
-record Ord (a : Set) : Set where
+record Ord (a : Type) : Type where
   field
     _<_ _>_ : a → a → Bool
 
-record Ord₁ (a : Set) : Set where
+record Ord₁ (a : Type) : Type where
   field
     _<_ : a → a → Bool
 
   _>_ : a → a → Bool
   x > y = y < x
 
-record Ord₂ (a : Set) : Set where
+record Ord₂ (a : Type) : Type where
   field
     _>_ : a → a → Bool
 
@@ -46,7 +46,7 @@ instance
   OrdBool₀ ._>_ = Ord₁._>_ OB
 {-# COMPILE AGDA2HS OrdBool₀ #-}
 
-data Bool1 : Set where
+data Bool1 : Type where
   Mk1 : Bool -> Bool1
 {-# COMPILE AGDA2HS Bool1 #-}
 instance
@@ -58,7 +58,7 @@ instance
       ord₁ .Ord₁._<_ (Mk1 True)  _       = False
 {-# COMPILE AGDA2HS OrdBool₁ #-}
 
-data Bool2 : Set where
+data Bool2 : Type where
   Mk2 : Bool -> Bool2
 {-# COMPILE AGDA2HS Bool2 #-}
 instance
@@ -70,7 +70,7 @@ instance
       (Mk2 True)  <: _       = False
 {-# COMPILE AGDA2HS OrdBool₂ #-}
 
-data Bool3 : Set where
+data Bool3 : Type where
   Mk3 : Bool -> Bool3
 {-# COMPILE AGDA2HS Bool3 #-}
 instance
@@ -82,7 +82,7 @@ instance
       (Mk3 True)  <: _       = False
 {-# COMPILE AGDA2HS OrdBool₃ #-}
 
-data Bool4 : Set where
+data Bool4 : Type where
   Mk4 : Bool -> Bool4
 {-# COMPILE AGDA2HS Bool4 #-}
 lift4 : (Bool → Bool → a) → (Bool4 → Bool4 → a)
@@ -93,7 +93,7 @@ instance
   OrdBool₄ = record {Ord₁ (λ where .Ord₁._<_ → lift4 (λ x y → not x && y))}
 {-# COMPILE AGDA2HS OrdBool₄ #-}
 
-data Bool5 : Set where
+data Bool5 : Type where
   Mk5 : Bool -> Bool5
 {-# COMPILE AGDA2HS Bool5 #-}
 instance
@@ -105,7 +105,7 @@ instance
       (Mk5 True)  >: (Mk5 b) = not b
 {-# COMPILE AGDA2HS OrdBool₅ #-}
 
-data Bool6 : Set where
+data Bool6 : Type where
   Mk6 : Bool -> Bool6
 {-# COMPILE AGDA2HS Bool6 #-}
 instance
@@ -131,13 +131,13 @@ defaultShowList shows (x ∷ xs)
   ∘ showString "]"
 {-# COMPILE AGDA2HS defaultShowList #-}
 
-record Show (a : Set) : Set where
+record Show (a : Type) : Type where
   field
     show : a → String
     showsPrec : Int → a → ShowS
     showList : List a → ShowS
 
-record Show₁ (a : Set) : Set where
+record Show₁ (a : Type) : Type where
   field showsPrec : Int → a → ShowS
 
   show : a → String
@@ -146,7 +146,7 @@ record Show₁ (a : Set) : Set where
   showList : List a → ShowS
   showList = defaultShowList (showsPrec 0)
 
-record Show₂ (a : Set) : Set where
+record Show₂ (a : Type) : Type where
   field show : a → String
 
   showsPrec : Int → a → ShowS
diff --git a/test/Deriving.agda b/test/Deriving.agda
index 4504dd40..c323a1cf 100644
--- a/test/Deriving.agda
+++ b/test/Deriving.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-data Planet : Set where
+data Planet : Type where
   Mercury : Planet
   Venus   : Planet
   Earth   : Planet
@@ -36,7 +36,7 @@ postulate instance iPlanetShow : Show Planet
 
 {-# COMPILE AGDA2HS iPlanetShow derive stock #-}
 
-record Clazz (a : Set) : Set where
+record Clazz (a : Type) : Type where
   field
     foo : a → Int
     bar : a → Bool
@@ -49,7 +49,7 @@ postulate instance iPlanetClazz : Clazz Planet
 
 {-# COMPILE AGDA2HS iPlanetClazz derive anyclass #-}
 
-data Optional (a : Set) : Set where
+data Optional (a : Type) : Type where
   Of    : a → Optional a
   Empty : Optional a
 
@@ -59,7 +59,7 @@ postulate instance iOptionalEq : ⦃ Eq a ⦄ → Eq (Optional a)
 
 {-# COMPILE AGDA2HS iOptionalEq #-}
 
-data Duo (a b : Set) : Set where
+data Duo (a b : Type) : Type where
   MkDuo : (a × b) → Duo a b
 
 {-# COMPILE AGDA2HS Duo newtype #-}
diff --git a/test/ErasedPatternLambda.agda b/test/ErasedPatternLambda.agda
index f7749992..29a4a7b0 100644
--- a/test/ErasedPatternLambda.agda
+++ b/test/ErasedPatternLambda.agda
@@ -2,7 +2,7 @@ open import Haskell.Prelude
 
 Scope = List Bool
 
-data Telescope (@0 α : Scope) : @0 Scope → Set where
+data Telescope (@0 α : Scope) : @0 Scope → Type where
   ExtendTel : ∀ {@0 x β} → Bool → Telescope (x ∷ α) β  → Telescope α (x ∷ β)
 {-# COMPILE AGDA2HS Telescope #-}
 
diff --git a/test/ErasedTypeArguments.agda b/test/ErasedTypeArguments.agda
index f390c9cd..817b40b8 100644
--- a/test/ErasedTypeArguments.agda
+++ b/test/ErasedTypeArguments.agda
@@ -2,14 +2,14 @@
 -- and in lambdas do get erased.
 module ErasedTypeArguments where
 
-open import Agda.Primitive
+open import Agda.Primitive renaming (Set to Type)
 open import Agda.Builtin.Unit
 open import Agda.Builtin.Nat
 
 -- A record type which has both members compiled,
 -- but the argument of the lambda is erased;
 -- so that it won't be dependent-typed after compilation.
-record Σ' {i j} (a : Set i) (b : @0 a -> Set j) : Set (i ⊔ j) where
+record Σ' {i j} (a : Type i) (b : @0 a -> Type j) : Type (i ⊔ j) where
   constructor _:^:_
   field
     proj₁ : a
@@ -26,6 +26,6 @@ test n = n :^: tt
 
 -- Tests a type function that would be accepted anyway,
 -- but the argument is erased.
-data Id {i j} (@0 a : Set i) (f : @0 Set i -> Set j) : Set j where
+data Id {i j} (@0 a : Type i) (f : @0 Type i -> Type j) : Type j where
   MkId : f a -> Id a f
 {-# COMPILE AGDA2HS Id newtype #-}
diff --git a/test/Fail/Copatterns.agda b/test/Fail/Copatterns.agda
index 1db241be..ac8e9910 100644
--- a/test/Fail/Copatterns.agda
+++ b/test/Fail/Copatterns.agda
@@ -4,7 +4,7 @@ module Fail.Copatterns where
 
 open import Haskell.Prelude
 
-record R : Set where
+record R : Type where
   field
     foo : Bool
 open R public
diff --git a/test/Fail/DerivingParseFailure.agda b/test/Fail/DerivingParseFailure.agda
index c31e2084..be7a5b60 100644
--- a/test/Fail/DerivingParseFailure.agda
+++ b/test/Fail/DerivingParseFailure.agda
@@ -1,6 +1,8 @@
 module Fail.DerivingParseFailure where
 
-record Example : Set where
+open import Haskell.Prim using (Type)
+
+record Example : Type where
 {-# COMPILE AGDA2HS Example deriving !& #-}
 -- {-# COMPILE AGDA2HS Example deriving Show via Foo #-}
 -- {-# COMPILE AGDA2HS Example deriving (Show, Eq, Ord) class #-}
diff --git a/test/Fail/ErasedRecordParameter.agda b/test/Fail/ErasedRecordParameter.agda
index 61773175..f0cd7bef 100644
--- a/test/Fail/ErasedRecordParameter.agda
+++ b/test/Fail/ErasedRecordParameter.agda
@@ -1,7 +1,9 @@
 -- c.f. Issue #145, this is the record variant
 module Fail.ErasedRecordParameter where
 
-record Ok (@0 a : Set) : Set where
+open import Haskell.Prim using (Type)
+
+record Ok (@0 a : Type) : Type where
   constructor Thing
   field unThing : a
 open Ok public
diff --git a/test/Fail/ExplicitInstance.agda b/test/Fail/ExplicitInstance.agda
index 2918ca15..921fa750 100644
--- a/test/Fail/ExplicitInstance.agda
+++ b/test/Fail/ExplicitInstance.agda
@@ -3,7 +3,7 @@ module Fail.ExplicitInstance where
 
 open import Haskell.Prelude
 
-record HasDefault (a : Set) : Set where
+record HasDefault (a : Type) : Type where
   field
     theDefault : a
 open HasDefault {{...}}
diff --git a/test/Fail/ExplicitInstance2.agda b/test/Fail/ExplicitInstance2.agda
index 4960cbe7..29de998f 100644
--- a/test/Fail/ExplicitInstance2.agda
+++ b/test/Fail/ExplicitInstance2.agda
@@ -3,7 +3,7 @@ module Fail.ExplicitInstance2 where
 
 open import Haskell.Prelude
 
-record HasDefault (a : Set) : Set where
+record HasDefault (a : Type) : Type where
   field
     theDefault : a
 open HasDefault {{...}}
diff --git a/test/Fail/Issue113a.agda b/test/Fail/Issue113a.agda
index bb33cdef..66e5bb1e 100644
--- a/test/Fail/Issue113a.agda
+++ b/test/Fail/Issue113a.agda
@@ -2,7 +2,9 @@
 
 module Fail.Issue113a where
 
-record Loop : Set where
+open import Haskell.Prim using (Type)
+
+record Loop : Type where
   coinductive
   field force : Loop
 open Loop public
diff --git a/test/Fail/Issue113b.agda b/test/Fail/Issue113b.agda
index 1016b1e0..411ccd34 100644
--- a/test/Fail/Issue113b.agda
+++ b/test/Fail/Issue113b.agda
@@ -2,9 +2,11 @@
 
 module Fail.Issue113b where
 
-postulate A : Set
+open import Haskell.Prim using (Type)
 
-record Loop : Set where
+postulate A : Type
+
+record Loop : Type where
   coinductive
   field force : Loop
 open Loop public
diff --git a/test/Fail/Issue125.agda b/test/Fail/Issue125.agda
index b60bf624..3cbe7af9 100644
--- a/test/Fail/Issue125.agda
+++ b/test/Fail/Issue125.agda
@@ -1,16 +1,18 @@
 module Fail.Issue125 where
 
-data A (a : Set) : Set where
+open import Haskell.Prim using (Type)
+
+data A (a : Type) : Type where
   ACtr : a -> A a
 
 {-# COMPILE AGDA2HS A #-}
 
-data B : Set where
+data B : Type where
   ACtr : B
 
 {-# COMPILE AGDA2HS B #-}
 
-data C : Set where
+data C : Type where
   Ca : C
 
 {-# COMPILE AGDA2HS C #-}
diff --git a/test/Fail/Issue146.agda b/test/Fail/Issue146.agda
index 65c04fec..8edec223 100644
--- a/test/Fail/Issue146.agda
+++ b/test/Fail/Issue146.agda
@@ -2,14 +2,14 @@ module Fail.Issue146 where
 
 open import Haskell.Prelude
 
-record Wrap (a : Set) : Set where
+record Wrap (a : Type) : Type where
   constructor MkWrap
   field wrapped : a
 open Wrap public
 
 {-# COMPILE AGDA2HS Wrap #-}
 
-record Class (a : Set) : Set where
+record Class (a : Type) : Type where
   field
     method : Wrap a → Wrap a
 open Class ⦃...⦄ public
diff --git a/test/Fail/Issue150.agda b/test/Fail/Issue150.agda
index 4bd0713a..19733460 100644
--- a/test/Fail/Issue150.agda
+++ b/test/Fail/Issue150.agda
@@ -2,7 +2,7 @@ module Fail.Issue150 where
 
 open import Haskell.Prelude
 
-record Tup (a b : Set) : Set where
+record Tup (a b : Type) : Type where
   constructor MkTup
   field exl : a ; exr : b
 open Tup public
diff --git a/test/Fail/Issue169-record.agda b/test/Fail/Issue169-record.agda
index 8f8065c5..e04e03bc 100644
--- a/test/Fail/Issue169-record.agda
+++ b/test/Fail/Issue169-record.agda
@@ -6,7 +6,7 @@ module Fail.Issue169-record where
 
 open import Haskell.Prelude
 
-record Identity (a : Set) : Set where
+record Identity (a : Type) : Type where
     field
         runIdentity : a
 open Identity public
diff --git a/test/Fail/Issue185.agda b/test/Fail/Issue185.agda
index 85149d38..4d4d5beb 100644
--- a/test/Fail/Issue185.agda
+++ b/test/Fail/Issue185.agda
@@ -1,8 +1,8 @@
 module Fail.Issue185 where
 
-open import Agda.Builtin.Bool
+open import Haskell.Prim using (Bool; True; Type)
 
-record RecordTest : Set where
+record RecordTest : Type where
   constructor MkRecord
   field
     aBool : Bool
@@ -14,5 +14,5 @@ open RecordTest public
 {-# COMPILE AGDA2HS aBoolAsAFunction #-}
 
 test : Bool
-test = aBoolAsAFunction (MkRecord true)
+test = aBoolAsAFunction (MkRecord True)
 {-# COMPILE AGDA2HS test #-}
diff --git a/test/Fail/Issue223.agda b/test/Fail/Issue223.agda
index dd5e88a4..34a26aac 100644
--- a/test/Fail/Issue223.agda
+++ b/test/Fail/Issue223.agda
@@ -1,8 +1,10 @@
 module Fail.Issue223 where
 
-data Void : Set where
+open import Haskell.Prim using (Type)
+
+data Void : Type where
 {-# COMPILE AGDA2HS Void #-}
 
-test : {a : Set} → Void → a
+test : {a : Type} → Void → a
 test ()
 {-# COMPILE AGDA2HS test #-}
diff --git a/test/Fail/NewTypeRecordTwoFields.agda b/test/Fail/NewTypeRecordTwoFields.agda
index 36a12b2b..cd9459d0 100644
--- a/test/Fail/NewTypeRecordTwoFields.agda
+++ b/test/Fail/NewTypeRecordTwoFields.agda
@@ -2,7 +2,7 @@ module Fail.NewTypeRecordTwoFields where
 
 open import Haskell.Prelude
 
-record Duo (a b : Set) : Set where
+record Duo (a b : Type) : Type where
     constructor MkDuo
     field
         left : a
diff --git a/test/Fail/NewTypeTwoConstructors.agda b/test/Fail/NewTypeTwoConstructors.agda
index 2b143405..191c116f 100644
--- a/test/Fail/NewTypeTwoConstructors.agda
+++ b/test/Fail/NewTypeTwoConstructors.agda
@@ -2,7 +2,7 @@ module Fail.NewTypeTwoConstructors where
 
 open import Haskell.Prelude
 
-data Choice (a b  : Set) : Set where
+data Choice (a b  : Type) : Type where
   A : a → Choice a b
   B : b → Choice a b
 
diff --git a/test/Fail/NewTypeTwoFields.agda b/test/Fail/NewTypeTwoFields.agda
index ddbe3138..94572dd8 100644
--- a/test/Fail/NewTypeTwoFields.agda
+++ b/test/Fail/NewTypeTwoFields.agda
@@ -2,7 +2,7 @@ module Fail.NewTypeTwoFields where
 
 open import Haskell.Prelude
 
-data Duo (a b : Set) : Set where
+data Duo (a b : Type) : Type where
   MkDuo : a → b → Duo a b
 
 {-# COMPILE AGDA2HS Duo newtype #-}
diff --git a/test/Fail/NonCanonicalSuperclass.agda b/test/Fail/NonCanonicalSuperclass.agda
index 0fdf807f..e83e9f52 100644
--- a/test/Fail/NonCanonicalSuperclass.agda
+++ b/test/Fail/NonCanonicalSuperclass.agda
@@ -3,7 +3,7 @@ module Fail.NonCanonicalSuperclass where
 
 open import Haskell.Prelude
 
-record Class (a : Set) : Set where
+record Class (a : Type) : Type where
   field
     foo : a → a
 open Class {{...}} public
@@ -16,7 +16,7 @@ instance
 
 {-# COMPILE AGDA2HS ClassBool #-}
 
-record Subclass (a : Set) : Set where
+record Subclass (a : Type) : Type where
   field
     overlap {{super}} : Class a
     bar : a
diff --git a/test/Fail/NonCopatternInstance.agda b/test/Fail/NonCopatternInstance.agda
index dcde4577..ff3eed61 100644
--- a/test/Fail/NonCopatternInstance.agda
+++ b/test/Fail/NonCopatternInstance.agda
@@ -1,14 +1,16 @@
 
 module Fail.NonCopatternInstance where
 
-record HasId (a : Set) : Set where
+open import Haskell.Prim using (Type)
+
+record HasId (a : Type) : Type where
   field id : a → a
 
 open HasId ⦃ ... ⦄
 
 {-# COMPILE AGDA2HS HasId class #-}
 
-data Unit : Set where
+data Unit : Type where
   MkUnit : Unit
 
 {-# COMPILE AGDA2HS Unit #-}
diff --git a/test/Fail/NonStarDatatypeIndex.agda b/test/Fail/NonStarDatatypeIndex.agda
index 53804e99..16f2ded6 100644
--- a/test/Fail/NonStarDatatypeIndex.agda
+++ b/test/Fail/NonStarDatatypeIndex.agda
@@ -2,6 +2,6 @@ module Fail.NonStarDatatypeIndex where
 
 open import Haskell.Prelude
 
-data T (n : Nat) : Set where
+data T (n : Nat) : Type where
   MkT : T n
 {-# COMPILE AGDA2HS T #-}
diff --git a/test/Fail/NonStarRecordIndex.agda b/test/Fail/NonStarRecordIndex.agda
index bd8c6c1b..6eebe848 100644
--- a/test/Fail/NonStarRecordIndex.agda
+++ b/test/Fail/NonStarRecordIndex.agda
@@ -2,7 +2,7 @@ module Fail.NonStarRecordIndex where
 
 open import Haskell.Prelude
 
-record T (n : Nat) : Set where
+record T (n : Nat) : Type where
   field
     Tb : Bool
 {-# COMPILE AGDA2HS T #-}
diff --git a/test/Fail/QualifiedRecordProjections.agda b/test/Fail/QualifiedRecordProjections.agda
index 709999a1..2ee61180 100644
--- a/test/Fail/QualifiedRecordProjections.agda
+++ b/test/Fail/QualifiedRecordProjections.agda
@@ -1,6 +1,8 @@
 module Fail.QualifiedRecordProjections where
 
-record Test (a : Set) : Set where
+open import Haskell.Prim using (Type)
+
+record Test (a : Type) : Type where
   field
     one : a
 
diff --git a/test/Fail/TypeLambda.agda b/test/Fail/TypeLambda.agda
index de530cc4..7a13550f 100644
--- a/test/Fail/TypeLambda.agda
+++ b/test/Fail/TypeLambda.agda
@@ -3,7 +3,7 @@ module Fail.TypeLambda where
 
 open import Haskell.Prelude
 
-foo : (f : (Set → Set) → Set) (x : f (λ y → Nat)) (y : f List) → Nat
+foo : (f : (Type → Type) → Type) (x : f (λ y → Nat)) (y : f List) → Nat
 foo f x y = 42
 
 {-# COMPILE AGDA2HS foo #-}
diff --git a/test/FunCon.agda b/test/FunCon.agda
index 259ab5a0..4be777b9 100644
--- a/test/FunCon.agda
+++ b/test/FunCon.agda
@@ -1,7 +1,7 @@
 
 open import Haskell.Prelude
 
-data D1 (t : Set → Set) : Set where
+data D1 (t : Type → Type) : Type where
   C1 : t Bool → D1 t
 
 {-# COMPILE AGDA2HS D1 #-}
@@ -11,7 +11,7 @@ f1 = C1 (_== 0)
 
 {-# COMPILE AGDA2HS f1 #-}
 
-data D2 (t : Set → Set → Set) : Set where
+data D2 (t : Type → Type → Type) : Type where
   C2 : t Int Int → D2 t
 
 {-# COMPILE AGDA2HS D2 #-}
diff --git a/test/Haskell/Data/ByteString.agda b/test/Haskell/Data/ByteString.agda
index 5de8842d..3fec94d2 100644
--- a/test/Haskell/Data/ByteString.agda
+++ b/test/Haskell/Data/ByteString.agda
@@ -3,7 +3,7 @@ module Haskell.Data.ByteString where
 open import Haskell.Prelude
 
 postulate
-  ByteString : Set
+  ByteString : Type
 
   instance
     iEqByteString : Eq ByteString
diff --git a/test/HeightMirror.agda b/test/HeightMirror.agda
index 72e84c31..7d7a4374 100644
--- a/test/HeightMirror.agda
+++ b/test/HeightMirror.agda
@@ -2,7 +2,7 @@
 open import Haskell.Prelude hiding (max)
 open import Haskell.Law.Equality hiding (subst)
 
-subst : {p : @0 a → Set} {@0 m n : a} → @0 m ≡ n → p m → p n
+subst : {p : @0 a → Type} {@0 m n : a} → @0 m ≡ n → p m → p n
 subst refl t = t
 
 {-# COMPILE AGDA2HS subst transparent #-}
@@ -12,7 +12,7 @@ max zero    n       = n
 max (suc m) zero    = suc m
 max (suc m) (suc n) = suc (max m n)
 
-data Tree (a : Set) : (@0 height : Nat) → Set where
+data Tree (a : Type) : (@0 height : Nat) → Type where
   Tip : Tree a 0
   Bin : ∀ {@0 l r} (x : a) → Tree a l → Tree a r → Tree a (suc (max l r))
 
diff --git a/test/Importee.agda b/test/Importee.agda
index b64915c7..4bd63301 100644
--- a/test/Importee.agda
+++ b/test/Importee.agda
@@ -8,15 +8,15 @@ _!#_ : Int → Int → Int
 x !# y = x + y
 {-# COMPILE AGDA2HS _!#_ #-}
 
-data Foo : Set where
+data Foo : Type where
   MkFoo : Foo
 {-# COMPILE AGDA2HS Foo #-}
 
 -- ** base
-record Fooable (a : Set) : Set where
+record Fooable (a : Type) : Type where
   field doTheFoo defaultFoo : a
 -- ** defaults
-record DefaultFooable (a : Set) : Set where
+record DefaultFooable (a : Type) : Type where
   field doTheFoo : a
 
   defaultFoo : a
diff --git a/test/Inlining.agda b/test/Inlining.agda
index c5065ee1..602343e9 100644
--- a/test/Inlining.agda
+++ b/test/Inlining.agda
@@ -2,7 +2,7 @@ module Inlining where
 
 open import Haskell.Prelude
 
-Alias : Set
+Alias : Type
 Alias = Bool
 {-# COMPILE AGDA2HS Alias inline #-}
 
@@ -10,7 +10,7 @@ aliased : Alias
 aliased = True
 {-# COMPILE AGDA2HS aliased #-}
 
-record Wrap (a : Set) : Set where
+record Wrap (a : Type) : Type where
   constructor Wrapped
   field
     unwrap : a
diff --git a/test/Issue115.agda b/test/Issue115.agda
index e7e4d08e..03768913 100644
--- a/test/Issue115.agda
+++ b/test/Issue115.agda
@@ -1,10 +1,12 @@
-record Pointed (a : Set) : Set where
+open import Haskell.Prim using (Type)
+
+record Pointed (a : Type) : Type where
   field
     it : a
 open Pointed {{...}} public
 {-# COMPILE AGDA2HS Pointed class #-}
 
-data A : Set where A1 : A
+data A : Type where A1 : A
 {-# COMPILE AGDA2HS A #-}
 
 instance
@@ -12,7 +14,7 @@ instance
   iPointedA .it = A1
 {-# COMPILE AGDA2HS iPointedA #-}
 
-data Delay (a : Set) : Set where
+data Delay (a : Type) : Type where
   Later : Delay a → Delay a
   Now : a → Delay a
 {-# COMPILE AGDA2HS Delay #-}
diff --git a/test/Issue145.agda b/test/Issue145.agda
index feae5372..d4b2b48f 100644
--- a/test/Issue145.agda
+++ b/test/Issue145.agda
@@ -5,7 +5,7 @@ open import Haskell.Prim.Strict
 
 -- ** PASS
 
-module _ {a : Set} where
+module _ {a : Type} where
   it : a → a
   it x = x
   {-# COMPILE AGDA2HS it #-}
@@ -14,13 +14,13 @@ it' : ⦃ Monoid a ⦄ → a → a
 it' x = x
 {-# COMPILE AGDA2HS it' #-}
 
-data Ok' {ℓ} (a : Set ℓ) : Set ℓ where
+data Ok' {ℓ} (a : Type ℓ) : Type ℓ where
   Thing' : Strict a → Ok' a
 {-# COMPILE AGDA2HS Ok' #-}
 
 -- ** FAIL
 
-data Ok {a : Set} : Set where
+data Ok {a : Type} : Type where
   Thing : a → Ok
 {-# COMPILE AGDA2HS Ok #-}
 
diff --git a/test/Issue169.agda b/test/Issue169.agda
index bc005606..3fc35d13 100644
--- a/test/Issue169.agda
+++ b/test/Issue169.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-record Identity (a : Set) : Set where
+record Identity (a : Type) : Type where
     field
         runIdentity : a
 open Identity public
diff --git a/test/Issue200.agda b/test/Issue200.agda
index d4b2a7f3..42ea44d6 100644
--- a/test/Issue200.agda
+++ b/test/Issue200.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-data Void : Set where
+data Void : Type where
 
 test : Maybe Void → Maybe Void
 test = λ
diff --git a/test/Issue210.agda b/test/Issue210.agda
index bd742958..b92972d8 100644
--- a/test/Issue210.agda
+++ b/test/Issue210.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude hiding (f)
 
-record Test (a : Set) : Set₁ where
+record Test (a : Type) : Type₁ where
   field
     f : a -> a
 open Test {{...}} public
diff --git a/test/Issue257.agda b/test/Issue257.agda
index 09dc2588..0293397f 100644
--- a/test/Issue257.agda
+++ b/test/Issue257.agda
@@ -2,6 +2,6 @@ module Issue257 where
 
 open import Haskell.Prelude
 
-record Wrap : Set where
+record Wrap : Type where
   field int : Integer
 {-# COMPILE AGDA2HS Wrap unboxed #-}
diff --git a/test/Issue264.agda b/test/Issue264.agda
index 68ab94ec..9369582d 100644
--- a/test/Issue264.agda
+++ b/test/Issue264.agda
@@ -1,7 +1,8 @@
+open import Haskell.Prim using (Type)
 
-module Issue264 (@0 name : Set) where
+module Issue264 (@0 name : Type) where
 
-data Term : @0 Set → Set where
+data Term : @0 Type → Type where
   Dummy : Term name
 
 {-# COMPILE AGDA2HS Term #-}
diff --git a/test/Issue301.agda b/test/Issue301.agda
index 252555da..16e0e110 100644
--- a/test/Issue301.agda
+++ b/test/Issue301.agda
@@ -3,7 +3,7 @@ open import Haskell.Prelude
 open import Haskell.Prim.Monoid
 open import Haskell.Prim.Foldable
 
-data MyData (a : Set) : Set where
+data MyData (a : Type) : Type where
   Nuttin' : MyData a
 {-# COMPILE AGDA2HS MyData #-}
 
@@ -18,7 +18,7 @@ instance
 
 -- need to create instance for semigroup first
 -- (requires explicitly typed function AFAICT)
-_><_ : {a : Set} -> MyData a -> MyData a -> MyData a
+_><_ : {a : Type} -> MyData a -> MyData a -> MyData a
 _ >< _ = Nuttin'
 {-# COMPILE AGDA2HS _><_ #-}
 
diff --git a/test/Issue305.agda b/test/Issue305.agda
index e9d006af..eaac3f92 100644
--- a/test/Issue305.agda
+++ b/test/Issue305.agda
@@ -1,8 +1,8 @@
 open import Haskell.Prelude
 
-module Issue305 (@0 X : Set) where
+module Issue305 (@0 X : Type) where
 
-record Class (a : Set) : Set where
+record Class (a : Type) : Type where
   field
     foo : a → a
 open Class {{...}} public
@@ -41,7 +41,7 @@ andOneMoreTest : Int → Int
 andOneMoreTest x = foo 5
 {-# COMPILE AGDA2HS andOneMoreTest #-}
 
-record Subclass (a : Set) : Set where
+record Subclass (a : Type) : Type where
   field
     overlap {{super}} : Class a
     bar : a
diff --git a/test/Issue308.agda b/test/Issue308.agda
index ddd05f40..d95957cd 100644
--- a/test/Issue308.agda
+++ b/test/Issue308.agda
@@ -1,19 +1,19 @@
 open import Haskell.Prelude
 
-record Class (a : Set) : Set where
+record Class (a : Type) : Type where
   field
     foo : a → a
 open Class {{...}} public
 {-# COMPILE AGDA2HS Class class #-}
 
-module M1 (@0 X : Set) where
+module M1 (@0 X : Type) where
 
   instance
     ClassInt : Class Int
     ClassInt .foo = _+ 1
   {-# COMPILE AGDA2HS ClassInt #-}
 
-module M2 (@0 X : Set) where
+module M2 (@0 X : Type) where
 
   open M1 X
 
diff --git a/test/Issue309.agda b/test/Issue309.agda
index 9c4e5317..965fe01d 100644
--- a/test/Issue309.agda
+++ b/test/Issue309.agda
@@ -1,7 +1,9 @@
 module Issue309 where
 
-private variable @0 a : Set
+open import Haskell.Prim using (Type)
 
-Ap : (p : @0 a → Set) → @0 a → Set
+private variable @0 a : Type
+
+Ap : (p : @0 a → Type) → @0 a → Type
 Ap p x = p x
 {-# COMPILE AGDA2HS Ap #-}
diff --git a/test/Issue317.agda b/test/Issue317.agda
index 788d8dbd..bcbdef49 100644
--- a/test/Issue317.agda
+++ b/test/Issue317.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-record D : Set where
+record D : Type where
   constructor C
   field unC : Int
 open D public
diff --git a/test/Issue69.agda b/test/Issue69.agda
index 4f14f694..3a065723 100644
--- a/test/Issue69.agda
+++ b/test/Issue69.agda
@@ -2,7 +2,7 @@ open import Haskell.Prelude
 
 mutual
 
-  data Map (k : Set) (a : Set) : Set where
+  data Map (k : Type) (a : Type) : Type where
     Bin : (sz : Nat) → (kx : k) → (x : a)
           → (l : Map k a) → (r : Map k a)
           → {{@0 szVal : sz ≡ (size l) + (size r) + 1}}
@@ -10,7 +10,7 @@ mutual
     Tip : Map k a
   {-# COMPILE AGDA2HS Map #-}
 
-  size : {k a : Set} → Map k a → Nat
+  size : {k a : Type} → Map k a → Nat
   size Tip = 0
   size (Bin sz _ _ _ _) = sz
   {-# COMPILE AGDA2HS size #-}
diff --git a/test/Issue73.agda b/test/Issue73.agda
index d0cb26c8..319c4837 100644
--- a/test/Issue73.agda
+++ b/test/Issue73.agda
@@ -1,6 +1,8 @@
 module Issue73 where
 
-record ImplicitField (a : Set) : Set where
+open import Haskell.Prim using (Type)
+
+record ImplicitField (a : Type) : Type where
     field
         aField : a
         @0 {anImplicitField} : a
diff --git a/test/Issue92.agda b/test/Issue92.agda
index 01140d24..daf3d82d 100644
--- a/test/Issue92.agda
+++ b/test/Issue92.agda
@@ -1,9 +1,9 @@
 open import Haskell.Prelude
 
-postulate Something : Set
+postulate Something : Type
 postulate something : Something
 
-module _ {a : Set} where
+module _ {a : Type} where
   foo : a → a
   foo x = bar {something}
     where
diff --git a/test/Kinds.agda b/test/Kinds.agda
index 053210f7..106839b8 100644
--- a/test/Kinds.agda
+++ b/test/Kinds.agda
@@ -2,14 +2,14 @@ module Kinds where
 
 open import Haskell.Prelude
 
-record ReaderT (r : Set) (m : Set → Set) (a  : Set) : Set where
+record ReaderT (r : Type) (m : Type → Type) (a  : Type) : Type where
   constructor RdrT
   field runReaderT : r → m a
 open ReaderT public
 
 {-# COMPILE AGDA2HS ReaderT #-}
 
-data Kleisli (m : Set → Set) (a b : Set) : Set where
+data Kleisli (m : Type → Type) (a b : Type) : Type where
   K : (a → m b) → Kleisli m a b
 
 {-# COMPILE AGDA2HS Kleisli #-}
diff --git a/test/LawfulOrd.agda b/test/LawfulOrd.agda
index 6027f6ab..ab068ad1 100644
--- a/test/LawfulOrd.agda
+++ b/test/LawfulOrd.agda
@@ -1,7 +1,7 @@
 open import Haskell.Prelude
 open import Haskell.Law
 
-data Ordered (a : Set) : Set where
+data Ordered (a : Type) : Type where
     Gt : ⦃ @0 iOrd : Ord a ⦄ → (a' : a) → (a'' : a) → ⦃ @0 pf : (a' > a'') ≡ True ⦄ → Ordered a
     Lt : ⦃ @0 iOrd : Ord a ⦄ → (a' : a) → (a'' : a) → ⦃ @0 pf : (a' < a'') ≡ True ⦄ → Ordered a
     E :  ⦃ @0 iOrd : Ord a ⦄ → (a' : a) → (a'' : a) → ⦃ @0 pf : a' ≡ a'' ⦄         → Ordered a
diff --git a/test/ModuleParameters.agda b/test/ModuleParameters.agda
index 812689d0..865d22f4 100644
--- a/test/ModuleParameters.agda
+++ b/test/ModuleParameters.agda
@@ -2,10 +2,10 @@
 open import Haskell.Prelude hiding (a)
 
 module ModuleParameters
-  (@0 name : Set)
-  (p : @0 name → Set) where
+  (@0 name : Type)
+  (p : @0 name → Type) where
 
-data Scope : Set where
+data Scope : Type where
   Empty : Scope
   Bind  : (@0 x : name) → p x → Scope → Scope
 {-# COMPILE AGDA2HS Scope #-}
@@ -15,7 +15,7 @@ unbind Empty = Empty
 unbind (Bind _ _ s) = s
 {-# COMPILE AGDA2HS unbind #-}
 
-module _ {a : Set} where
+module _ {a : Type} where
   thing : a → a
   thing x = y
     where y : a
@@ -27,7 +27,7 @@ module _ {a : Set} where
   stuff x (Bind _ _ _) = x
   {-# COMPILE AGDA2HS stuff #-}
 
-  module _ {b : Set} where
+  module _ {b : Type} where
     more : b → a → Scope → Scope
     more _ _ Empty = Empty
     more _ _ (Bind _ _ s) = s
diff --git a/test/NewTypePragma.agda b/test/NewTypePragma.agda
index fb549fcc..97d5be6b 100644
--- a/test/NewTypePragma.agda
+++ b/test/NewTypePragma.agda
@@ -1,3 +1,4 @@
+open import Haskell.Prim using (Type)
 open import Haskell.Prelude using ( Int ; fst ; snd
                                   ; a ; b
                                   ; _×_ ; _,_
@@ -9,7 +10,7 @@ open import Haskell.Prelude using ( Int ; fst ; snd
 -- data newtype
 #-}
 
-data Indexed (a : Set) : Set where
+data Indexed (a : Type) : Type where
     MkIndexed : Int × a → Indexed a
 
 {-# COMPILE AGDA2HS Indexed newtype #-}
@@ -23,7 +24,7 @@ index = MkIndexed
 -- data newtype with deriving
 #-}
 
-data Pair (a b : Set) : Set where
+data Pair (a b : Type) : Type where
     MkPair : a × b → Pair a b
 
 {-# COMPILE AGDA2HS Pair newtype deriving ( Show, Eq ) #-}
@@ -32,7 +33,7 @@ data Pair (a b : Set) : Set where
 -- record newtype
 #-}
 
-record Identity (a : Set) : Set where
+record Identity (a : Type) : Type where
     constructor MkIdentity
     field
         runIdentity : a
@@ -44,7 +45,7 @@ open Identity public
 -- record newtype with erased proof
 #-}
 
-record Equal (a : Set) : Set where
+record Equal (a : Type) : Type where
     constructor MkEqual
     field
         pair : a × a
@@ -57,7 +58,7 @@ open Equal public
 -- record newtype with same name
 #-}
 
-record Duo (a : Set) : Set where
+record Duo (a : Type) : Type where
     field
         duo : a × a
 open Duo public
diff --git a/test/OtherImportee.agda b/test/OtherImportee.agda
index 85f3d86c..3b669c28 100644
--- a/test/OtherImportee.agda
+++ b/test/OtherImportee.agda
@@ -1,6 +1,6 @@
 open import Haskell.Prelude
 
-data OtherFoo : Set where
+data OtherFoo : Type where
   MkFoo : OtherFoo
 
 {-# COMPILE AGDA2HS OtherFoo #-}
diff --git a/test/ProjLike.agda b/test/ProjLike.agda
index 9241eddc..ff678813 100644
--- a/test/ProjLike.agda
+++ b/test/ProjLike.agda
@@ -2,9 +2,9 @@ module ProjLike where
 
 open import Haskell.Prelude
 
-module M (a : Set) where
+module M (a : Type) where
 
-  data Scope : Set where
+  data Scope : Type where
     Empty : Scope
     Bind  : a → Scope → Scope
   
diff --git a/test/ProjectionLike.agda b/test/ProjectionLike.agda
index 9682be21..2d3f2978 100644
--- a/test/ProjectionLike.agda
+++ b/test/ProjectionLike.agda
@@ -3,7 +3,7 @@ open import Haskell.Prelude
 
 module _ (@0 n : Bool) where
 
-record R : Set where
+record R : Type where
   field
     fld : Int
 open R public
diff --git a/test/QualifiedImportee.agda b/test/QualifiedImportee.agda
index 05848f2d..47472825 100644
--- a/test/QualifiedImportee.agda
+++ b/test/QualifiedImportee.agda
@@ -10,16 +10,16 @@ x !# y = x - y
 
 {-# COMPILE AGDA2HS _!#_ #-}
 
-data Foo : Set where
+data Foo : Type where
   MkFoo : Foo
 
 {-# COMPILE AGDA2HS Foo #-}
 
 -- ** base
-record Fooable (a : Set) : Set where
+record Fooable (a : Type) : Type where
   field doTheFoo defaultFoo : a
 -- ** defaults
-record DefaultFooable (a : Set) : Set where
+record DefaultFooable (a : Type) : Type where
   field doTheFoo : a
 
   defaultFoo : a
diff --git a/test/QualifiedImports.agda b/test/QualifiedImports.agda
index 4a936123..fec325a4 100644
--- a/test/QualifiedImports.agda
+++ b/test/QualifiedImports.agda
@@ -36,6 +36,6 @@ qualDefaultBar : Qually.Foo
 qualDefaultBar = Qually.defaultFoo
 {-# COMPILE AGDA2HS qualDefaultBar #-}
 
-Foo : Set
+Foo : Type
 Foo = Importee.Foo
 {-# COMPILE AGDA2HS Foo #-}
diff --git a/test/QualifiedModule.agda b/test/QualifiedModule.agda
index f9d2ef68..7a49e038 100644
--- a/test/QualifiedModule.agda
+++ b/test/QualifiedModule.agda
@@ -1,4 +1,6 @@
 
+open import Haskell.Prim hiding (f)
+
 -- Names of definitions inside a module should not be qualified in the
 -- generated Haskell code!
 
@@ -6,7 +8,7 @@ module _ where
 
 module A where
 
-  data D : Set where
+  data D : Type where
     C : D
   {-# COMPILE AGDA2HS D #-}
 
diff --git a/test/RankNTypes.agda b/test/RankNTypes.agda
index 4cd0987d..855da1a7 100644
--- a/test/RankNTypes.agda
+++ b/test/RankNTypes.agda
@@ -2,21 +2,23 @@
 {-# LANGUAGE Haskell98 #-}
 #-}
 
-data MyBool : Set where
+open import Haskell.Prim using (Type)
+
+data MyBool : Type where
     MyTrue : MyBool
     MyFalse : MyBool
 {-# COMPILE AGDA2HS MyBool #-}
 
-rank2ForallUse : (∀ (a : Set) → a → a) → MyBool
+rank2ForallUse : (∀ (a : Type) → a → a) → MyBool
 rank2ForallUse f = f MyBool MyTrue
 {-# COMPILE AGDA2HS rank2ForallUse #-}
 
-module _  (f : ∀ (a : Set) → a → a) where
+module _  (f : ∀ (a : Type) → a → a) where
     rank2Module : MyBool
     rank2Module = f MyBool MyTrue
     {-# COMPILE AGDA2HS rank2Module #-}
 
 -- ExistentialQuantification: Not supported yet, but also no error message yet
--- data Exist : Set₁ where
---     MkExist : ∀ (a : Set) → a → Exist
+-- data Exist : Type₁ where
+--     MkExist : ∀ (a : Type) → a → Exist
 -- {-# COMPILE AGDA2HS Exist #-}
diff --git a/test/Records.agda b/test/Records.agda
index 5441ce45..2f64760e 100644
--- a/test/Records.agda
+++ b/test/Records.agda
@@ -1,11 +1,12 @@
 module Records where
 
+open import Haskell.Prim using (Type)
 open import Haskell.Prelude using (String; Nat)
 
-variable a b : Set
+variable a b : Type
 
 -- parametrized record type exported as an Haskell record
-record Pair (a b : Set) : Set where
+record Pair (a b : Type) : Type where
   constructor MkPair
   field
     proj₁ : a
@@ -17,13 +18,13 @@ open Pair public
 
 -- no named constructor means we reuse the record name
 
-record Wrap (a : Set) : Set where
+record Wrap (a : Type) : Type where
   field unwrap : a
 open Wrap public
 {-# COMPILE AGDA2HS Wrap #-}
 
 -- record type exported as an Haskell class definition
-record MyMonoid (a : Set) : Set where
+record MyMonoid (a : Type) : Type where
   field
     mempty  : a
     mappend : a → a → a
@@ -40,9 +41,10 @@ swap₂ (record {unwrap = p}) = record {unwrap = record { proj₁ = proj₂ p; p
 {-# COMPILE AGDA2HS swap₂ #-}
 
 -- record with deriving clause
-record User : Set where
+record User : Type where
   field
     name : String
     code : Nat
 open User public
 {-# COMPILE AGDA2HS User deriving (Eq, Show) #-}
+ 
\ No newline at end of file
diff --git a/test/ScopedTypeVariables.agda b/test/ScopedTypeVariables.agda
index b083cc02..960bbad3 100644
--- a/test/ScopedTypeVariables.agda
+++ b/test/ScopedTypeVariables.agda
@@ -3,7 +3,7 @@ open import Haskell.Prelude
 module ScopedTypeVariables (@0 x : Bool) where
 
 -- We can encode explicit `forall` quantification by module parameters in Agda.
-module _ {a : Set} {{_ : Eq a}} where
+module _ {a : Type} {{_ : Eq a}} where
   foo : a → Bool
   foo x = it x == x
     where
@@ -12,7 +12,7 @@ module _ {a : Set} {{_ : Eq a}} where
 {-# COMPILE AGDA2HS foo #-}
 
 -- Type arguments should be compiled in the right order.
-module _ {a b : Set} where
+module _ {a b : Type} where
   bar : a → b → (b → b) → b
   bar x y f = baz y
     where
@@ -20,7 +20,7 @@ module _ {a b : Set} where
       baz z = f (f z)
 {-# COMPILE AGDA2HS bar #-}
 
-data D : Set where
+data D : Type where
   MakeD : (y : Bool) → @0 x ≡ y → D
 {-# COMPILE AGDA2HS D #-}
 
diff --git a/test/Superclass.agda b/test/Superclass.agda
index 61f879ce..ac01ac0b 100644
--- a/test/Superclass.agda
+++ b/test/Superclass.agda
@@ -1,13 +1,13 @@
 {-# OPTIONS --erase-record-parameters #-}
 open import Haskell.Prelude
 
-record Super (a : Set) : Set where
+record Super (a : Type) : Type where
   field
     myFun : a → a
 open Super {{...}}
 {-# COMPILE AGDA2HS Super class #-}
 
-record Sub (a : Set) : Set where
+record Sub (a : Type) : Type where
   field
     overlap {{super}} : Super a
 open Sub {{...}}
@@ -18,13 +18,13 @@ foo = myFun ∘ myFun
 {-# COMPILE AGDA2HS foo #-}
 
 -- Trying if diamonds are fine
-record Sub2 (a : Set) : Set where
+record Sub2 (a : Type) : Type where
   field
     overlap {{super}} : Super a
 open Sub2 {{...}}
 {-# COMPILE AGDA2HS Sub2 class #-}
 
-record Subber (a : Set) : Set where
+record Subber (a : Type) : Type where
   field
     overlap {{super}} : Sub a
     overlap {{super2}} : Sub2 a
@@ -47,7 +47,7 @@ instance
 
 -- Defining a subclass of an existing class from Prelude
 
-record DiscreteOrd (a : Set) : Set where
+record DiscreteOrd (a : Type) : Type where
   field
     overlap {{super}} : Ord a
 open DiscreteOrd {{...}}
diff --git a/test/Test.agda b/test/Test.agda
index df025152..6c361e3b 100644
--- a/test/Test.agda
+++ b/test/Test.agda
@@ -20,7 +20,7 @@ import Data.Monoid
 
 -- ** Datatypes & functions
 
-data Exp (v : Set) : Set where
+data Exp (v : Type) : Type where
   Plus : Exp v → Exp v → Exp v
   Lit : Nat → Exp v
   Var : v → Exp v
@@ -136,7 +136,7 @@ thm (x ∷ xs) ys rewrite thm xs ys | assoc x (sum xs) (sum ys) = refl
 
 -- (custom) Monoid class
 
-record MonoidX (a : Set) : Set where
+record MonoidX (a : Type) : Type where
   field memptyX  : a
         mappendX : a → a → a
 
@@ -177,7 +177,7 @@ sumMon (x ∷ xs) = x <> sumMon xs
 
 -- Using the Monoid class from the Prelude
 
-data NatSum : Set where
+data NatSum : Type where
   MkSum : Nat → NatSum
 
 {-# COMPILE AGDA2HS NatSum #-}
diff --git a/test/TransparentFun.agda b/test/TransparentFun.agda
index 3d7832ae..35f687e1 100644
--- a/test/TransparentFun.agda
+++ b/test/TransparentFun.agda
@@ -1,7 +1,7 @@
 
 open import Haskell.Prelude
 
-data Unit : Set where
+data Unit : Type where
   unit : Unit
 
 myId : @0 Unit → a → a
@@ -14,7 +14,7 @@ testMyId u = myId u 42
 
 {-# COMPILE AGDA2HS testMyId #-}
 
-tyId : @0 Unit → Set → Set
+tyId : @0 Unit → Type → Type
 tyId unit a = a
 
 {-# COMPILE AGDA2HS tyId transparent #-}
@@ -24,7 +24,7 @@ testTyId {unit} n = n
 
 {-# COMPILE AGDA2HS testTyId #-}
 
-data Tree : Set where
+data Tree : Type where
   Tip : Tree
   Bin : Tree → Tree → Tree
 
diff --git a/test/Tree.agda b/test/Tree.agda
index f87d15da..1d83d2b6 100644
--- a/test/Tree.agda
+++ b/test/Tree.agda
@@ -1,11 +1,11 @@
 open import Haskell.Prelude
 
-data _≤_ : Nat → Nat → Set where
+data _≤_ : Nat → Nat → Type where
   instance
     zero-≤ : ∀ {@0 n} → zero ≤ n
     suc-≤ : ∀ {@0 m n} → @0 {{m ≤ n}} → suc m ≤ suc n
 
-data Tree (@0 l u : Nat) : Set where
+data Tree (@0 l u : Nat) : Type where
   Leaf  : @0 {{l ≤ u}} → Tree l u
   Node  : (x : Nat) → Tree l x → Tree x u → Tree l u
 {-# COMPILE AGDA2HS Tree #-}
diff --git a/test/Tuples.agda b/test/Tuples.agda
index 5d5eef04..8b014bd3 100644
--- a/test/Tuples.agda
+++ b/test/Tuples.agda
@@ -8,7 +8,7 @@ swap (a , b) = b , a
 
 {-# COMPILE AGDA2HS swap #-}
 
-data TuplePos : Set where
+data TuplePos : Type where
   Test : TuplePos × Bool → TuplePos
 
 {-# COMPILE AGDA2HS TuplePos #-}
diff --git a/test/TypeBasedUnboxing.agda b/test/TypeBasedUnboxing.agda
index bb7e8e7f..d3191beb 100644
--- a/test/TypeBasedUnboxing.agda
+++ b/test/TypeBasedUnboxing.agda
@@ -6,7 +6,7 @@ open import Haskell.Prelude
 
 data P : Prop where
 
-record R : Set where
+record R : Type where
   field
     @0 anErasedThing : Bool
     aRealThing : Int
diff --git a/test/TypeDirected.agda b/test/TypeDirected.agda
index a4e9a4b2..3eb21d1b 100644
--- a/test/TypeDirected.agda
+++ b/test/TypeDirected.agda
@@ -1,14 +1,14 @@
 {-# OPTIONS --prop #-}
 module TypeDirected where
 
-open import Agda.Builtin.Reflection
+open import Agda.Builtin.Reflection hiding (Type)
 open import Agda.Builtin.Unit
 open import Haskell.Prelude
 
 data MyProp : Prop where
   true : MyProp
 
-myconst : {a : Set} → MyProp → a → {y : a} → a
+myconst : {a : Type} → MyProp → a → {y : a} → a
 myconst p x = x
 
 {-# COMPILE AGDA2HS myconst #-}
diff --git a/test/TypeOperatorExport.agda b/test/TypeOperatorExport.agda
index c3ee0601..9c8178ca 100644
--- a/test/TypeOperatorExport.agda
+++ b/test/TypeOperatorExport.agda
@@ -2,20 +2,18 @@ module TypeOperatorExport where
 
 {-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-}
 
-open import Agda.Primitive
+open import Haskell.Prim
 
-_<_ : Set -> Set -> Set
+_<_ : Type -> Type -> Type
 a < b = a
 {-# COMPILE AGDA2HS _<_ #-}
 
-data _***_ {i j : Level} (a : Set i) (b : Set j) : Set (i ⊔ j) where
+data _***_ {i j : Level} (a : Type i) (b : Type j) : Type (i ⊔ j) where
   _:*:_ : a -> b -> a *** b
 open _***_ public
 {-# COMPILE AGDA2HS _***_ #-}
 
-open import Agda.Builtin.Bool
-
 _&&&_ : Bool -> Bool -> Bool
-false &&& _  = false
+False &&& _  = False
 _     &&& b2 = b2
 {-# COMPILE AGDA2HS _&&&_ #-}
diff --git a/test/TypeOperators.agda b/test/TypeOperators.agda
index 288780ec..4273b780 100644
--- a/test/TypeOperators.agda
+++ b/test/TypeOperators.agda
@@ -2,12 +2,13 @@ module TypeOperators where
 
 {-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-}
 
+open import Haskell.Prim using (Type)
 open import Haskell.Prim.Either
 
 open import Agda.Builtin.Nat
 open import Agda.Builtin.Bool
 
-_:++:_ : Set → Set → Set
+_:++:_ : Type → Type → Type
 _:++:_ = Either
 {-# COMPILE AGDA2HS _:++:_ #-}
 
@@ -15,7 +16,7 @@ mx : Bool :++: Nat
 mx = Left true
 {-# COMPILE AGDA2HS mx #-}
 
-_++++_ : Set → Set → Set
+_++++_ : Type → Type → Type
 _++++_ = Either
 {-# COMPILE AGDA2HS _++++_ #-}
 
@@ -23,7 +24,7 @@ mx' : Bool ++++ Nat
 mx' = Left true
 {-# COMPILE AGDA2HS mx' #-}
 
-data _****_ (a b : Set): Set where
+data _****_ (a b : Type): Type where
   _:****_ : a → b → a **** b
 {-# COMPILE AGDA2HS _****_ #-}
 
diff --git a/test/TypeSynonyms.agda b/test/TypeSynonyms.agda
index be765b12..84a8448d 100644
--- a/test/TypeSynonyms.agda
+++ b/test/TypeSynonyms.agda
@@ -1,5 +1,6 @@
+open import Haskell.Prim using (Type)
 
-data Nat : Set where
+data Nat : Type where
   Zero : Nat
   Suc  : Nat → Nat
 {-# COMPILE AGDA2HS Nat #-}
@@ -11,12 +12,12 @@ myNat : Nat'
 myNat = Suc (Suc Zero)
 {-# COMPILE AGDA2HS myNat #-}
 
-data List (a : Set) : Set where
+data List (a : Type) : Type where
   Nil : List a
   Cons : a → List a → List a
 {-# COMPILE AGDA2HS List #-}
 
-List' : Set → Set
+List' : Type → Type
 List' a = List a
 {-# COMPILE AGDA2HS List' #-}
 
@@ -28,7 +29,7 @@ myListFun Nil = Nil
 myListFun (Cons x xs) = Cons x (myListFun xs)
 {-# COMPILE AGDA2HS myListFun #-}
 
-ListList : Set → Set
+ListList : Type → Type
 ListList a = List (List a)
 {-# COMPILE AGDA2HS ListList #-}
 
diff --git a/test/UnboxPragma.agda b/test/UnboxPragma.agda
index 52f3e50c..7434b88b 100644
--- a/test/UnboxPragma.agda
+++ b/test/UnboxPragma.agda
@@ -1,7 +1,7 @@
 
 open import Haskell.Prelude
 
-record ∃ (A : Set) (@0 P : A → Set) : Set where
+record ∃ (A : Type) (@0 P : A → Type) : Type where
   constructor _[_]
   field
     el : A
@@ -11,7 +11,7 @@ open ∃ public
 {-# COMPILE AGDA2HS ∃ unboxed #-}
 
 postulate
-  IsSorted : List Int → Set
+  IsSorted : List Int → Type
   looksfine : {xs : List Int} → IsSorted xs
 
 sort1 : List Int → ∃ (List Int) IsSorted
@@ -35,7 +35,7 @@ sortAll = map el (map (λ xs → xs [ looksfine {xs} ]) ((1 ∷ 2 ∷ []) ∷ (3
 
 {-# COMPILE AGDA2HS sortAll #-}
 
-record Σ0 (A : Set) (P : @0 A → Set) : Set where
+record Σ0 (A : Type) (P : @0 A → Type) : Type where
   constructor _[_]
   field
     @0 el : A
@@ -44,12 +44,12 @@ open Σ0 public
 
 {-# COMPILE AGDA2HS Σ0 unboxed #-}
 
-Scope : (name : Set) → Set
+Scope : (name : Type) → Type
 Scope name = Σ0 (List name) λ xs → ∃ Int λ n → length xs ≡ n
 
 {-# COMPILE AGDA2HS Scope #-}
 
-emptyScope : {name : Set} → Scope name
+emptyScope : {name : Type} → Scope name
 emptyScope = [] [ 0 [ refl ] ]
 
 {-# COMPILE AGDA2HS emptyScope #-}
diff --git a/test/Vector.agda b/test/Vector.agda
index 25cad781..ebf890b1 100644
--- a/test/Vector.agda
+++ b/test/Vector.agda
@@ -2,32 +2,32 @@
 open import Haskell.Prelude
 
 {- Old style using implicit arguments (no longer supported)
-data Vec (a : Set) : {n : Nat} → Set where
+data Vec (a : Type) : {n : Nat} → Type where
   Nil : Vec a {0}
   Cons : {n : Nat} → a → Vec a {n} → Vec a {suc n}
 {-# COMPILE AGDA2HS Vec #-}
 
-mapV : {a b : Set} {n : Nat} (f : a → b) → Vec a {n} → Vec b {n}
+mapV : {a b : Type} {n : Nat} (f : a → b) → Vec a {n} → Vec b {n}
 mapV f Nil = Nil
 mapV f (Cons x xs) = Cons (f x) (mapV f xs)
 {-# COMPILE AGDA2HS mapV #-}
 
-tailV : {a : Set} {n : Nat} → Vec a {suc n} → Vec a {n}
+tailV : {a : Type} {n : Nat} → Vec a {suc n} → Vec a {n}
 tailV (Cons x xs) = xs
 {-# COMPILE AGDA2HS tailV #-}
 -}
 
 -- New style using erasure instead of implicit arguments
-data Vec (a : Set) : (@0 n : Nat) → Set where
+data Vec (a : Type) : (@0 n : Nat) → Type where
   Nil : Vec a 0
   Cons : {@0 n : Nat} → a → Vec a n → Vec a (suc n)
 {-# COMPILE AGDA2HS Vec #-}
 
-mapV : {a b : Set} {@0 n : Nat} (f : a → b) → Vec a n → Vec b n
+mapV : {a b : Type} {@0 n : Nat} (f : a → b) → Vec a n → Vec b n
 mapV f Nil = Nil
 mapV f (Cons x xs) = Cons (f x) (mapV f xs)
 {-# COMPILE AGDA2HS mapV #-}
 
-tailV : {a : Set} {@0 n : Nat} → Vec a (suc n) → Vec a n
+tailV : {a : Type} {@0 n : Nat} → Vec a (suc n) → Vec a n
 tailV (Cons x xs) = xs
 {-# COMPILE AGDA2HS tailV #-}
diff --git a/test/WitnessedFlows.agda b/test/WitnessedFlows.agda
index bd5e8413..8d4ef541 100644
--- a/test/WitnessedFlows.agda
+++ b/test/WitnessedFlows.agda
@@ -1,7 +1,7 @@
 open import Haskell.Prelude
 open import Haskell.Control.Monad
 
-data Range : Set where
+data Range : Type where
     MkRange : (low high : Int)
             → {{ @0 h : ((low <= high) ≡ True) }}
             → Range
diff --git a/test/golden/DerivingParseFailure.err b/test/golden/DerivingParseFailure.err
index a74ff5db..5e04e5d0 100644
--- a/test/golden/DerivingParseFailure.err
+++ b/test/golden/DerivingParseFailure.err
@@ -1,2 +1,2 @@
-test/Fail/DerivingParseFailure.agda:4,1-44
+test/Fail/DerivingParseFailure.agda:6,1-44
 Parse error: !&
diff --git a/test/golden/ErasedRecordParameter.err b/test/golden/ErasedRecordParameter.err
index fcd7e22e..79d279c2 100644
--- a/test/golden/ErasedRecordParameter.err
+++ b/test/golden/ErasedRecordParameter.err
@@ -1,2 +1,2 @@
-test/Fail/ErasedRecordParameter.agda:4,8-10
+test/Fail/ErasedRecordParameter.agda:6,8-10
 Cannot use erased variable a in Haskell type
diff --git a/test/golden/Issue113a.err b/test/golden/Issue113a.err
index 8fef39b0..1b77fa87 100644
--- a/test/golden/Issue113a.err
+++ b/test/golden/Issue113a.err
@@ -1,2 +1,2 @@
-test/Fail/Issue113a.agda:5,8-12
+test/Fail/Issue113a.agda:7,8-12
 Unboxed record Loop cannot be recursive
diff --git a/test/golden/Issue113b.err b/test/golden/Issue113b.err
index 95bceec2..963af8e0 100644
--- a/test/golden/Issue113b.err
+++ b/test/golden/Issue113b.err
@@ -1,2 +1,2 @@
-test/Fail/Issue113b.agda:7,8-12
+test/Fail/Issue113b.agda:9,8-12
 Unboxed record Loop cannot be recursive
diff --git a/test/golden/Issue223.err b/test/golden/Issue223.err
index 868557d3..ad8d75df 100644
--- a/test/golden/Issue223.err
+++ b/test/golden/Issue223.err
@@ -1,2 +1,2 @@
-test/Fail/Issue223.agda:6,1-5
+test/Fail/Issue223.agda:8,1-5
 Functions defined with absurd patterns exclusively are not supported. Use function `error` from the Haskell.Prelude instead.
diff --git a/test/golden/NonCopatternInstance.err b/test/golden/NonCopatternInstance.err
index 385315f4..c34e6d0d 100644
--- a/test/golden/NonCopatternInstance.err
+++ b/test/golden/NonCopatternInstance.err
@@ -1,3 +1,3 @@
-test/Fail/NonCopatternInstance.agda:17,3-12
+test/Fail/NonCopatternInstance.agda:19,3-12
 Type class instances must be defined using copatterns (or top-level
 records) and cannot be defined using helper functions.
diff --git a/test/golden/QualifiedRecordProjections.err b/test/golden/QualifiedRecordProjections.err
index 4c803b97..786902fa 100644
--- a/test/golden/QualifiedRecordProjections.err
+++ b/test/golden/QualifiedRecordProjections.err
@@ -1,4 +1,4 @@
-test/Fail/QualifiedRecordProjections.agda:5,5-8
+test/Fail/QualifiedRecordProjections.agda:7,5-8
 Record projections (`one` in this case) must be brought into scope
 when compiling to Haskell record types. Add `open Test public`
 after the record declaration to fix this.
diff --git a/tutorials/example-basics/HelloWorld.agda b/tutorials/example-basics/HelloWorld.agda
index 2bf08eb3..769f54a7 100644
--- a/tutorials/example-basics/HelloWorld.agda
+++ b/tutorials/example-basics/HelloWorld.agda
@@ -7,7 +7,7 @@ Entry = Int × List String
 
 
 --defining a datatype
-data Tree (a : Set) : Set where
+data Tree (a : Type) : Type where
     Leaf   : a → Tree a
     Branch : a → Tree a → Tree a → Tree a
 
diff --git a/tutorials/example-proofs/Ascending.agda b/tutorials/example-proofs/Ascending.agda
index dd492294..06a0befc 100644
--- a/tutorials/example-proofs/Ascending.agda
+++ b/tutorials/example-proofs/Ascending.agda
@@ -14,7 +14,7 @@ isAscending (x ∷ y ∷ xs) = if x <= y then isAscending (y ∷ xs) else False
 {-# COMPILE AGDA2HS isAscending #-}
 
 -- data type defining a postulate of ascending order on lists
-data IsAscending₂ {a : Set} ⦃ iOrdA : Ord a ⦄ : List a → Set where
+data IsAscending₂ {a : Type} ⦃ iOrdA : Ord a ⦄ : List a → Type where
     Empty : IsAscending₂ []
     OneElem : (x : a) →  IsAscending₂ (x ∷ [])
     ManyElem : (x y : a) (xs : List a) 
diff --git a/tutorials/example-proofs/Triangle.agda b/tutorials/example-proofs/Triangle.agda
index 6938bccb..6ec25572 100644
--- a/tutorials/example-proofs/Triangle.agda
+++ b/tutorials/example-proofs/Triangle.agda
@@ -10,7 +10,7 @@ countBiggerThan xs b = length (filter (λ x → (x >= b)) xs)
 {-# COMPILE AGDA2HS countBiggerThan #-}
 
 -- Triangle data type deinfition
-data Triangle : Set where
+data Triangle : Type where
     MkTriangle : (alpha beta gamma : Nat)
         → ⦃ @0 h₁ : (((alpha + beta + gamma) == 180) ≡ True ) ⦄
         → @0 ⦃ ((countBiggerThan
diff --git a/tutorials/example-structure/src/agda/Definition.agda b/tutorials/example-structure/src/agda/Definition.agda
index 27ca76ca..1d8eb061 100644
--- a/tutorials/example-structure/src/agda/Definition.agda
+++ b/tutorials/example-structure/src/agda/Definition.agda
@@ -2,7 +2,7 @@ module Definition where
 
 open import Haskell.Prelude
 
-data CountDown : Set where
+data CountDown : Type where
     MkCountdown : (start  : Int)
             → {{ @0 h : ((start > 0) ≡ True) }}
             → CountDown