Rename Set to Type in tests

Author: HeinrichApfelmus

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
 

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 #-}

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

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
 

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 #-}
 

test/Cubical/StreamFusion.agda

@@ -2,15 +2,14 @@ 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
 
 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

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

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 #-}
 

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 {{...}}

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

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 #-}

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 #-}
 

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 #-}

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

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 #-}

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

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 {{...}}

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 {{...}}

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

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

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 #-}