[ refactor ] Avoid importing Prelude in Extra.Dec and Extra.Refinement

Author: jespercockx

lib/base/Haskell/Extra/Dec.agda

@@ -1,11 +1,14 @@
 module Haskell.Extra.Dec where
 
-open import Haskell.Prelude
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
 open import Haskell.Extra.Refinement
+
 open import Agda.Primitive
 
 private variable
-  ℓ : Level
   P : Type
 
 @0 Reflects : Type ℓ → Bool → Type ℓ

lib/base/Haskell/Extra/Refinement.agda

@@ -1,10 +1,7 @@
 module Haskell.Extra.Refinement where
 
-open import Haskell.Prelude
-open import Agda.Primitive
-
-private variable
-  ℓ ℓ′ : Level
+open import Haskell.Prim
+open import Haskell.Prim.Maybe
 
 record ∃ (a : Type ℓ) (@0 P : a → Type ℓ′) : Type (ℓ ⊔ ℓ′) where
   constructor _⟨⟩

lib/base/Haskell/Prim.agda

@@ -23,7 +23,7 @@ open import Agda.Builtin.Strict     public
 open import Agda.Builtin.List       public
 
 variable
-  @0 ℓ : Level
+  @0 ℓ ℓ′ : Level
   a b c d e : Type
   f m s t : Type → Type