diff --git a/lib/base/Haskell/Control/Applicative.agda b/lib/base/Haskell/Control/Applicative.agda
new file mode 100644
index 00000000..2e44047b
--- /dev/null
+++ b/lib/base/Haskell/Control/Applicative.agda
@@ -0,0 +1,31 @@
+module Haskell.Control.Applicative where
+
+open import Haskell.Prim
+open import Haskell.Prim.Maybe
+
+open import Haskell.Prim.Applicative public
+  renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Alternative public
+  renaming (module Instances to AlternativeInstances)
+open import Haskell.Data.Functor public using (_<$>_)
+open import Haskell.Data.Foldable public using (asum)
+
+
+infixl 4 _<**>_
+_<**>_ : ⦃ Applicative f ⦄ → f a → f (a → b) → f b
+_<**>_ = liftA2 (λ a f → f a)
+
+liftA : ⦃ Applicative f ⦄ → (a → b) → f a → f b
+liftA f a = pure f <*> a
+
+liftA3 : ⦃ Applicative f ⦄ → (a → b → c → d) → f a → f b → f c → f d
+liftA3 f a b c = liftA2 f a b <*> c
+
+optional : ⦃ Alternative f ⦄ → f a → f (Maybe a)
+optional v = Just <$> v <|> pure Nothing
+
+-- Omitted for now:
+-- - 'newtype Const a (b :: k) = Const { getConst :: a }'
+-- - 'newtype WrappedMonad (m :: Type -> Type) a = WrapMonad { unwrapMonad :: m a }'
+-- - 'newtype WrappedArrow (a :: Type -> Type -> Type) b c = WrapArrow { unwrapArrow :: a b c }'
+-- - 'newtype ZipList a = ZipList { getZipList :: [a] }'
diff --git a/lib/base/Haskell/Control/Monad.agda b/lib/base/Haskell/Control/Monad.agda
index f42f3813..463271b5 100644
--- a/lib/base/Haskell/Control/Monad.agda
+++ b/lib/base/Haskell/Control/Monad.agda
@@ -2,10 +2,149 @@ module Haskell.Control.Monad where
 
 open import Haskell.Prim
 open import Haskell.Prim.Bool
-open import Haskell.Prim.Monad
-open import Haskell.Prim.String
+open import Haskell.Prim.Int
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Applicative hiding (module Instances)
+open import Haskell.Prim.Alternative hiding (module Instances)
+open import Haskell.Prim.Traversable hiding (module Instances)
+open import Haskell.Prim.Foldable hiding (module Instances)
+open import Haskell.Data.Foldable using (sequenceA₋; foldlM)
+open import Haskell.Data.List using (unzip; zipWith)
 open import Haskell.Extra.Erase
 
-guard : {{ MonadFail m }} → (b : Bool) → m (Erase (b ≡ True))
-guard True = return (Erased refl)
-guard False = fail "Guard was not True"
+open import Haskell.Prim.Functor public
+  renaming (module Instances to FunctorInstances)
+open import Haskell.Prim.Applicative public
+  using () renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Alternative public
+  using () renaming (module Instances to AlternativeInstances)
+open import Haskell.Prim.Monad public
+  renaming (module Instances to MonadInstances)
+open import Haskell.Prim.MonadFail public
+  renaming (module Instances to MonadFailInstances)
+open import Haskell.Prim.MonadPlus public
+  renaming (module Instances to MonadPlusInstances)
+open import Haskell.Prim.Traversable public
+  using (mapM; sequence) renaming (module Instances to TraversableInstances)
+open import Haskell.Prim.Foldable public
+  using () renaming (module Instances to FoldableInstances)
+open import Haskell.Data.Traversable public using (forM)
+open import Haskell.Data.Foldable public using (mapM₋; forM₋; sequence₋; msum)
+open import Haskell.Data.Functor public using (void)
+
+
+private variable a1 a2 a3 a4 a5 r : Type
+
+infixr 1 _=<<_ _>=>_ _<=<_
+_=<<_ : ⦃ Monad m ⦄ → (a → m b) → m a → m b
+_=<<_ = flip _>>=_
+
+_>=>_ : ⦃ Monad m ⦄ → (a → m b) → (b → m c) → a → m c
+f >=> g = λ x → f x >>= g
+
+_<=<_ : ⦃ Monad m ⦄ → (b → m c) → (a → m b) → a → m c
+_<=<_ = flip _>=>_
+
+
+join : ⦃ Monad m ⦄ → m (m a) → m a
+join x = x >>= id
+
+mfilter : ⦃ MonadPlus m ⦄ → (a → Bool) → m a → m a
+mfilter p ma = do
+  a ← ma
+  if p a then return a else mzero
+
+filterM : ⦃ Applicative m ⦄ → (a → m Bool) → List a → m (List a)
+filterM p = foldr (λ x → liftA2 (λ b → if b then (x ∷_) else id) (p x)) (pure [])
+
+mapAndUnzipM : ⦃ Applicative m ⦄ → (a → m (b × c)) → List a → m (List b × List c)
+mapAndUnzipM f xs = fmap unzip (traverse f xs)
+
+zipWithM : ⦃ Applicative m ⦄ → (a → b → m c) → List a → List b → m (List c)
+zipWithM f xs ys = sequenceA (zipWith f xs ys)
+
+zipWithM₋ : ⦃ Applicative m ⦄ → (a → b → m c) → List a → List b → m ⊤
+zipWithM₋ f xs ys = sequenceA₋ (zipWith f xs ys)
+
+foldM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b
+foldM = foldlM
+
+foldM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m ⊤
+foldM₋ f a xs  = foldlM f a xs >> return tt
+
+replicateMNat : ⦃ Applicative m ⦄ → Nat → m a → m (List a)
+replicateMNat zero    _ = pure []
+replicateMNat (suc n) f = liftA2 _∷_ f (replicateMNat n f)
+
+replicateM : ⦃ Applicative m ⦄ → (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → m a → m (List a)
+replicateM cnt f = replicateMNat (intToNat cnt) f
+
+replicateMNat₋ : ⦃ Applicative m ⦄ → Nat → m a → m ⊤
+replicateMNat₋ zero    _ = pure tt
+replicateMNat₋ (suc n) f = f *> replicateMNat₋ n f
+
+replicateM₋ : ⦃ Applicative m ⦄ → (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → m a → m ⊤
+replicateM₋ cnt f = replicateMNat₋ (intToNat cnt) f
+
+
+guard : ⦃ Alternative f ⦄ → (b : Bool) → f (Erase (b ≡ True))
+guard True  = pure (Erased refl)
+guard False = empty
+
+when : ⦃ Applicative f ⦄ → (b : Bool) → ({@0 p : b ≡ True} → f ⊤) → f ⊤
+when True  f = f {refl}
+when False _ = pure tt
+
+unless : ⦃ Applicative f ⦄ → (b : Bool) → ({@0 p : b ≡ False} → f ⊤) → f ⊤
+unless True  _ = pure tt
+unless False f = f {refl}
+
+
+liftM : ⦃ Monad m ⦄ → (a1 → r) → m a1 → m r
+liftM f m1 = do
+  x1 ← m1
+  return (f x1)
+
+liftM2 : ⦃ Monad m ⦄ → (a1 → a2 → r) → m a1 → m a2 → m r
+liftM2 f m1 m2 = do
+  x1 ← m1
+  x2 ← m2
+  return (f x1 x2)
+
+liftM3 : ⦃ Monad m ⦄ → (a1 → a2 → a3 → r) → m a1 → m a2 → m a3 → m r
+liftM3 f m1 m2 m3 = do
+  x1 ← m1
+  x2 ← m2
+  x3 ← m3
+  return (f x1 x2 x3)
+
+liftM4 : ⦃ Monad m ⦄ → (a1 -> a2 -> a3 -> a4 -> r) → m a1 → m a2 → m a3 → m a4 → m r
+liftM4 f m1 m2 m3 m4 = do
+  x1 ← m1
+  x2 ← m2
+  x3 ← m3
+  x4 ← m4
+  return (f x1 x2 x3 x4)
+
+liftM5 : ⦃ Monad m ⦄ → (a1 → a2 → a3 → a4 → a5 → r) → m a1 → m a2 → m a3 → m a4 → m a5 → m r
+liftM5 f m1 m2 m3 m4 m5 = do
+  x1 ← m1
+  x2 ← m2
+  x3 ← m3
+  x4 ← m4
+  x5 ← m5
+  return (f x1 x2 x3 x4 x5)
+
+ap : ⦃ Monad m ⦄ → m (a → b) → m a → m b
+ap m1 m2 = do
+  f ← m1
+  x ← m2
+  return (f x)
+
+infixl 4 _<$!>_
+_<$!>_ : ⦃ Monad m ⦄ → (a → b) → m a → m b
+_<$!>_ = fmap
+
+
+-- Omitted for now:
+-- - 'forever :: Applicative => f -> f a -> f b'
diff --git a/lib/base/Haskell/Data/Foldable.agda b/lib/base/Haskell/Data/Foldable.agda
new file mode 100644
index 00000000..9de1012c
--- /dev/null
+++ b/lib/base/Haskell/Data/Foldable.agda
@@ -0,0 +1,100 @@
+module Haskell.Data.Foldable where
+
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Eq hiding (module Instances)
+open import Haskell.Prim.Ord hiding (module Instances)
+open import Haskell.Prim.Monoid hiding (module Instances)
+open import Haskell.Prim.Applicative hiding (module Instances)
+open import Haskell.Prim.Alternative hiding (module Instances)
+open import Haskell.Prim.Monad hiding (module Instances)
+open import Haskell.Prim.MonadPlus hiding (module Instances)
+
+open import Haskell.Prim.Eq public
+  using () renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord public
+  using () renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Monoid public
+  using () renaming (module Instances to MonoidInstances)
+open import Haskell.Prim.Applicative public
+  using () renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Alternative public
+  using () renaming (module Instances to AlternativeInstances)
+open import Haskell.Prim.Monad public
+  using () renaming (module Instances to MonadInstances)
+open import Haskell.Prim.MonadPlus public
+  using () renaming (module Instances to MonadPlusInstances)
+open import Haskell.Prim.Foldable public
+  renaming (module Instances to FoldableInstances)
+
+
+foldrM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → b → m b) → b → t a → m b
+foldrM f z0 xs = foldl (λ k x z → f x z >>= k) return xs z0
+
+foldlM : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (b → a → m b) → b → t a → m b
+foldlM f z0 xs = foldr (λ x k z → f z x >>= k) return xs z0
+
+traverse₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → (a → f b) → t a → f ⊤
+traverse₋ f = foldr (λ x m → f x *> m) (pure tt)
+
+for₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → t a → (a → f b) → f ⊤
+for₋ = flip traverse₋
+
+mapM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → m b) → t a → m ⊤
+mapM₋ f = foldr (λ x m → f x >> m) (pure tt)
+
+forM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t a → (a → m b) → m ⊤
+forM₋ = flip mapM₋
+
+sequenceA₋ : ⦃ Foldable t ⦄ → ⦃ Applicative f ⦄ → t (f a) → f ⊤
+sequenceA₋ = foldr (λ mx my → mx *> my) (pure tt)
+
+sequence₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t (m a) → m ⊤
+sequence₋ = foldr (λ mx my → mx >> my) (pure tt)
+
+asum : ⦃ Foldable t ⦄ → ⦃ Alternative f ⦄ → t (f a) → f a
+asum = foldr _<|>_ empty
+
+msum : ⦃ Foldable t ⦄ → ⦃ MonadPlus m ⦄ → t (m a) → m a
+msum = asum
+
+concat : ⦃ Foldable t ⦄ → t (List a) → List a
+concat = fold
+
+concatMap : ⦃ Foldable t ⦄ → (a → List b) → t a → List b
+concatMap = foldMap
+
+any : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
+any ⦃ i ⦄ = foldMap ⦃ i ⦄ ⦃ MonoidDisj ⦄
+
+all : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
+all ⦃ i ⦄ = foldMap ⦃ i ⦄ ⦃ MonoidConj ⦄
+
+and : ⦃ Foldable t ⦄ → t Bool → Bool
+and = all id
+
+or : ⦃ Foldable t ⦄ → t Bool → Bool
+or = any id
+
+maximumBy : ⦃ _ : Foldable t ⦄ → (a → a → Ordering) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+maximumBy {a = a} cmp = foldr1 max'
+  where
+    max' : a → a → a
+    max' x y with cmp x y
+    ...         | GT = x
+    ...         | _  = y
+
+minimumBy : ⦃ _ : Foldable t ⦄ → (a → a → Ordering) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+minimumBy {a = a} cmp = foldr1 min'
+  where
+    min' : a → a → a
+    min' x y with cmp x y
+    ...         | GT = y
+    ...         | _  = x
+
+notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool
+notElem x t = not (elem x t)
+
+find : ⦃ Foldable t ⦄ → (a → Bool) → t a → Maybe a
+find ⦃ i ⦄ p = foldMap ⦃ i ⦄ ⦃ MonoidFirst ⦄ (λ x → if p x then Just x else Nothing)
diff --git a/lib/base/Haskell/Data/Functor.agda b/lib/base/Haskell/Data/Functor.agda
new file mode 100644
index 00000000..9f7ae4e3
--- /dev/null
+++ b/lib/base/Haskell/Data/Functor.agda
@@ -0,0 +1,26 @@
+module Haskell.Data.Functor where
+
+open import Haskell.Prim
+open import Haskell.Prim.Tuple
+
+open import Haskell.Prim.Functor public
+  renaming (module Instances to FunctorInstances)
+
+
+infixl 4 _$>_
+_$>_ : ⦃ Functor f ⦄ → f a → (@0 ⦃ a ⦄ → b) → f b
+_$>_ = flip _<$_
+
+infixl 4 _<$>_
+_<$>_ : ⦃ Functor f ⦄ → (a → b) → f a → f b
+_<$>_ = fmap
+
+infixl 1 _<&>_
+_<&>_ : ⦃ Functor f ⦄ → f a → (a → b) → f b
+m <&> f = fmap f m
+
+unzip : ⦃ Functor f ⦄ → f (a × b) -> (f a × f b)
+unzip xs = fst <$> xs , snd <$> xs
+
+void : ⦃ Functor f ⦄ → f a → f ⊤
+void = tt <$_
diff --git a/lib/base/Haskell/Data/List.agda b/lib/base/Haskell/Data/List.agda
index 00cbff80..84f86991 100644
--- a/lib/base/Haskell/Data/List.agda
+++ b/lib/base/Haskell/Data/List.agda
@@ -1,90 +1,316 @@
 module Haskell.Data.List where
 
-open import Haskell.Prelude
+open import Haskell.Prim
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Int
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Eq hiding (module Instances)
+open import Haskell.Prim.Ord hiding (module Instances)
+open import Haskell.Prim.Num hiding (module Instances)
 
-open import Haskell.Data.Ord using (comparing)
+open import Haskell.Prim.List public
+open import Haskell.Prim.Eq public
+  using () renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord public
+  using () renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Num public
+  using () renaming (module Instances to NumInstances)
+open import Haskell.Prim.Foldable public
+  using (null; length; foldl; foldl'; foldl1; foldr; foldr1; sum; product; maximum; minimum; elem)
+  renaming (module Instances to FoldableInstances)
+open import Haskell.Data.Foldable public
+  using (concat; concatMap; and; or; any; all; maximumBy; minimumBy; notElem; find)
+open import Haskell.Data.Traversable public using (mapAccumL; mapAccumR)
+open import Haskell.Data.String public using (lines; words; unlines; unwords)
 
-open import Haskell.Law.Eq
-open import Haskell.Law.Equality
 
-{-----------------------------------------------------------------------------
-    Operations
-------------------------------------------------------------------------------}
+variable i : Type
+
+uncons : List a → Maybe (a × List a)
+uncons []       = Nothing
+uncons (x ∷ xs) = Just (x , xs)
+
+unsnoc : List a → Maybe (List a × a)
+unsnoc = foldr (λ x → Just ∘ maybe ([] , x) (λ (a , b) → x ∷ a , b)) Nothing
+
+singleton : a → List a
+singleton = _∷ []
+
+compareLength : List a → Int → Ordering
+compareLength xs n =
+  if n < 0 then GT
+  else foldr (λ _ f m → if m > 0 then f (m - 1) else GT) (λ m → if m > 0 then LT else EQ) xs n
+
+foldl1' : (a → a → a) → (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
+foldl1' f (x ∷ xs) = foldl f x xs
+
+scanl : (b → a → b) → b → List a → List b
+scanl f z []       = z ∷ []
+scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs
+
+scanl' : (b → a → b) → b → List a → List b
+scanl' = scanl
+
+scanl1 : (a → a → a) → List a → List a
+scanl1 f []       = []
+scanl1 f (x ∷ xs) = scanl f x xs
+
+scanr : (a → b → b) → b → List a → List b
+scanr f z [] = z ∷ []
+scanr f z (x ∷ xs) = case scanr f z xs of λ where
+  []         → [] -- impossible
+  qs@(q ∷ _) → f x q ∷ qs
+
+scanr1 : (a → a → a) → List a → List a
+scanr1 f []       = []
+scanr1 f (x ∷ xs) = case scanr1 f xs of λ where
+  []         → x ∷ []
+  qs@(q ∷ _) → f x q ∷ qs
+
+replicateNat : Nat → a → List a
+replicateNat zero    _ = []
+replicateNat (suc n) x = x ∷ replicateNat n x
+
+replicate : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → a → List a
+replicate n = replicateNat (intToNat n)
+
+takeNat : Nat → List a → List a
+takeNat n       [] = []
+takeNat zero    xs = []
+takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs
+
+take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
+take n xs = takeNat (intToNat n) xs
+
+dropNat : Nat → List a → List a
+dropNat n       [] = []
+dropNat zero    xs = xs
+dropNat (suc n) (_ ∷ xs) = dropNat n xs
+
+drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
+drop n xs = dropNat (intToNat n) xs
+
+splitAtNat : (n : Nat) → List a → List a × List a
+splitAtNat _       []       = [] , []
+splitAtNat 0       xs       = [] , xs
+splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs)
+
+splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a
+splitAt n xs = splitAtNat (intToNat n) xs
+
+takeWhile : (a → Bool) → List a → List a
+takeWhile p [] = []
+takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else []
+
+dropWhile : (a → Bool) → List a → List a
+dropWhile p [] = []
+dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs
+
+dropWhileEnd : (a → Bool) → List a → List a
+dropWhileEnd p = foldr (λ x xs → if p x && null xs then [] else x ∷ xs) []
+
+span : (a → Bool) → List a → List a × List a
+span p [] = [] , []
+span p (x ∷ xs) = if p x then first (x ∷_) (span p xs)
+                         else ([] , x ∷ xs)
+
+break : (a → Bool) → List a → List a × List a
+break p = span (not ∘ p)
+
+stripPrefix : ⦃ Eq a ⦄ → List a → List a → Maybe (List a)
+stripPrefix []       ys       = Just ys
+stripPrefix _        []       = Nothing
+stripPrefix (x ∷ xs) (y ∷ ys) = if x == y then stripPrefix xs ys else Nothing
+
+reverse : List a → List a
+reverse = foldl (flip _∷_) []
+
+inits : List a → List (List a)
+inits = map reverse ∘ scanl (flip _∷_) []
+
+tails : List a → List (List a)
+tails []           = singleton []
+tails xs@(_ ∷ xs') = xs ∷ tails xs'
+
+isPrefixOf : ⦃ Eq a ⦄ → List a → List a → Bool
+isPrefixOf []       _        = True
+isPrefixOf _        []       = False
+isPrefixOf (x ∷ xs) (y ∷ ys) = x == y && isPrefixOf xs ys
+
+isSuffixOf : ⦃ Eq a ⦄ → List a → List a → Bool
+isSuffixOf xs ys = isPrefixOf (reverse xs) (reverse ys)
+
+isInfixOf : ⦃ Eq a ⦄ → List a → List a → Bool
+isInfixOf xs ys = any (isPrefixOf xs) (tails ys)
+
+isSubsequenceOf : ⦃ Eq a ⦄ → List a → List a → Bool
+isSubsequenceOf []           _        = True
+isSubsequenceOf _            []       = False
+isSubsequenceOf xs@(x ∷ xs') (y ∷ ys) = if x == y then isSubsequenceOf xs' ys
+                                        else isSubsequenceOf xs ys
+
+lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
+lookup _ []              = Nothing
+lookup k ((x , y) ∷ xys) = if k == x then Just y else lookup k xys
+
+filter : (a → Bool) → List a → List a
+filter p []       = []
+filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs
 
 partition : (a → Bool) → List a → (List a × List a)
 partition p xs = (filter p xs , filter (not ∘ p) xs)
 
--- | Delete all occurrences of an item.
--- Not part of 'Data.List'.
-deleteAll : ⦃ _ : Eq a ⦄ → @0 ⦃ IsLawfulEq a ⦄ → a → List a → List a
-deleteAll x = filter (not ∘ (x ==_))
-
--- | These semantics of 'nub' assume that the 'Eq' instance
--- is lawful.
--- These semantics are inefficient, but good for proofs.
-nub : ⦃ _ : Eq a ⦄ → @0 ⦃ IsLawfulEq a ⦄ → List a → List a
-nub [] = []
-nub (x ∷ xs) = x ∷ deleteAll x (nub xs)
-
-postulate
-  sortBy : (a → a → Ordering) → List a → List a
-
-sort : ⦃ Ord a ⦄ → List a → List a
-sort = sortBy compare
-
-sortOn : ⦃ Ord b ⦄ → (a → b) → List a → List a
-sortOn f =
-    map snd
-    ∘ sortBy (comparing fst)
-    ∘ map (λ x → let y = f x in seq y (y , x))
-
-{-----------------------------------------------------------------------------
-    Properties
-------------------------------------------------------------------------------}
-
--- | A deleted item is no longer an element.
---
-prop-elem-deleteAll
-  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
-      (x y : a) (zs : List a)
-  → elem x (deleteAll y zs)
-    ≡ (if x == y then False else elem x zs)
---
-prop-elem-deleteAll x y []
-  with x == y
-... | False = refl
-... | True  = refl
-prop-elem-deleteAll x y (z ∷ zs)
-  with recurse ← prop-elem-deleteAll x y zs
-  with y == z in eqyz
-... | True
-    with x == z in eqxz
-...   | True
-      rewrite equality' _ _ (trans (equality x z eqxz) (sym (equality y z eqyz)))
-      = recurse
-...   | False
-      = recurse
-prop-elem-deleteAll x y (z ∷ zs)
-    | False
-    with x == z in eqxz
-...   | True
-      rewrite equality x z eqxz | eqSymmetry y z | eqyz
-      = refl
-...   | False
-      = recurse
-
--- | An item is an element of the 'nub' iff it is
--- an element of the original list.
---
-prop-elem-nub
-  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
-      (x : a) (ys : List a)
-  → elem x (nub ys)
-    ≡ elem x ys
---
-prop-elem-nub x [] = refl
-prop-elem-nub x (y ∷ ys)
-  rewrite prop-elem-deleteAll x y (nub ys)
-  with x == y
-... | True = refl
-... | False = prop-elem-nub x ys
+infixl 9 _!?_
+_!?_ : List a → Int → Maybe a
+[]       !? _ = Nothing
+(x ∷ xs) !? n = case compare n 0 of λ where
+  LT → Nothing
+  EQ → Just x
+  GT → xs !? (n - 1)
+
+infixl 9 _!!ᴺ_
+_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a
+(x ∷ xs) !!ᴺ zero  = x
+(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n
+
+infixl 9 _!!_
+_!!_ : (xs : List a) (n : Int)
+     → ⦃ @0 _ : IsNonNegativeInt n ⦄
+     → ⦃ @0 _  : IsTrue (intToNat n < lengthNat xs) ⦄ → a
+xs !! n = xs !!ᴺ intToNat n
+
+findIndices : (a → Bool) → List a → List Int
+findIndices p xs = let go x r k = if p x then k ∷ r (k + 1) else r (k + 1)
+                   in foldr go (const []) xs 0
+
+findIndex : (a → Bool) → List a → Maybe Int
+findIndex p xs = case findIndices p xs of λ where
+  []      → Nothing
+  (x ∷ _) → Just x
+
+elemIndices : ⦃ Eq a ⦄ → a → List a → List Int
+elemIndices x = findIndices (x ==_)
+
+elemIndex : ⦃ Eq a ⦄ → a → List a → Maybe Int
+elemIndex x = findIndex (x ==_)
+
+zipWith : (a → b → c) → List a → List b → List c
+zipWith f []       _        = []
+zipWith f _        []       = []
+zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
+
+zipWith3 : (a → b → c → d) → List a → List b → List c → List d
+zipWith3 f []       _        _        = []
+zipWith3 f _        []       _        = []
+zipWith3 f _        _        []       = []
+zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs
+
+zip : List a → List b → List (a × b)
+zip = zipWith _,_
+
+zip3 : List a → List b → List c → List (a × b × c)
+zip3 = zipWith3 _,_,_
+
+unzip : List (a × b) → List a × List b
+unzip []              = [] , []
+unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys
+
+unzip3 : List (a × b × c) → List a × List b × List c
+unzip3 []                   = [] , [] , []
+unzip3 ((x , y , z) ∷ xyzs) = case unzip3 xyzs of λ where
+  (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs
+
+intersperse : a → List a → List a
+intersperse _   []       = []
+intersperse sep (x ∷ xs) = x ∷ prependToAll sep xs
+  where
+    prependToAll : a → List a → List a
+    prependToAll _   []       = []
+    prependToAll sep (x ∷ xs) = sep ∷ x ∷ prependToAll sep xs
+
+intercalate : List a → List (List a) → List a
+intercalate xs xss = concat (intersperse xs xss)
+
+subsequences : List a → List (List a)
+subsequences xs = [] ∷ nonEmptySubsequences xs
+  where
+    nonEmptySubsequences : List a → List (List a)
+    nonEmptySubsequences []       = []
+    nonEmptySubsequences (x ∷ xs) = let f ys r = ys ∷ (x ∷ ys) ∷ r
+                                    in singleton x ∷ foldr f [] (nonEmptySubsequences xs)
+
+nubBy : (a → a → Bool) → List a → List a
+nubBy eq [] = []
+nubBy eq (x ∷ xs) = x ∷ filter (not ∘ eq x) (nubBy eq xs)
+
+nub : ⦃ Eq a ⦄ → List a → List a
+nub = nubBy _==_
+
+deleteBy : (a → a → Bool) → a → List a → List a
+deleteBy _  _ []       = []
+deleteBy eq x (x' ∷ xs) = if eq x x' then xs else x' ∷ deleteBy eq x xs
+
+delete : ⦃ Eq a ⦄ → a → List a → List a
+delete = deleteBy _==_
+
+deleteFirstsBy : (a → a → Bool) → List a → List a → List a
+deleteFirstsBy eq = foldl (flip (deleteBy eq))
+
+infix 5 _\\_
+_\\_ : ⦃ Eq a ⦄ → List a → List a → List a
+_\\_ = deleteFirstsBy _==_
+
+unionBy : (a → a → Bool) → List a → List a → List a
+unionBy eq xs ys = xs ++ deleteFirstsBy eq (nubBy eq ys) xs
+
+union : ⦃ Eq a ⦄ → List a → List a → List a
+union = unionBy _==_
+
+intersectBy : (a → a → Bool) → List a → List a → List a
+intersectBy eq xs ys = filter (λ x → any (eq x) ys) xs
+
+intersect : ⦃ Eq a ⦄ → List a → List a → List a
+intersect = intersectBy _==_
+
+insertBy : (a → a → Ordering) → a → List a → List a
+insertBy _   x []           = singleton x
+insertBy cmp x ys@(y ∷ ys') = case cmp x y of λ where
+  GT → y ∷ insertBy cmp x ys'
+  _  → x ∷ ys
+
+insert : ⦃ Ord a ⦄ → a → List a → List a
+insert = insertBy compare
+
+
+-- Omitted for now:
+-- [obviously non-terminating]
+-- - 'iterate :: (a -> a) -> a -> [a]'
+-- - 'iterate' :: (a -> a) -> a -> [a]'
+-- - 'repeat :: a -> [a]'
+-- - 'cycle :: [a] -> [a]'
+-- - 'unfoldr :: (b -> Maybe (a, b)) -> b -> [a]
+
+-- [hard to prove termination]
+-- - 'groupBy :: (a -> a -> Bool) -> [a] -> [[a]]'
+-- - 'group :: Eq a => [a] -> [[a]]'
+-- - 'transpose :: [[a]] -> [[a]]'
+-- - 'permutations :: [a] -> [[a]]'
+-- - 'sortBy :: (a -> a -> Ordering) -> [a] -> [a]'
+-- - 'sort :: Ord a => [a] -> [a]'
+-- - 'sortOn :: Ord b => (a -> b) -> [a] -> [a]
+
+-- [type signature includes currently not supported (?) `NonEmpty` type]
+-- - 'inits1 :: [a] -> [NonEmpty a]'
+-- - 'tails1 :: [a] -> [NonEmpty a]'
+
+-- - 'zipWith4', 'zipWith5', 'zipWith6', 'zipWith7'
+-- - 'zip4', 'zip5', 'zip6', 'zip7'
+-- - 'unzip4', 'unzip5', 'unzip6', 'unzip7'
+
+-- - 'genericLength :: Num i => [a] -> i'
+-- - 'genericTake :: Integral i => i -> [a] -> [a]'
+-- - 'genericDrop :: Integral i => i -> [a] -> [a]'
+-- - 'genericSplitAt :: Integral i => i -> [a] -> ([a], [a])'
+-- - 'genericIndex :: Integral i => [a] -> i -> a'
+-- - 'genericReplicate :: Integral i => i -> a -> [a]'
diff --git a/lib/base/Haskell/Data/String.agda b/lib/base/Haskell/Data/String.agda
new file mode 100644
index 00000000..d807e704
--- /dev/null
+++ b/lib/base/Haskell/Data/String.agda
@@ -0,0 +1,44 @@
+module Haskell.Data.String where
+
+open import Haskell.Prim
+open import Haskell.Prim.List
+open import Haskell.Prim.Foldable hiding (module Instances)
+open import Haskell.Data.Foldable
+
+open import Haskell.Prim.String public
+open import Haskell.Prim.Foldable public
+  using () renaming (module Instances to FoldableInstances)
+
+
+module Helpers where
+  cons : Char → List String → List String
+  cons c []       = (c ∷ []) ∷ []
+  cons c (s ∷ ss) = (c ∷ s) ∷ ss
+
+  mutual
+    space : String → List String
+    space []      = []
+    space (c ∷ s) = if primIsSpace c then space s else cons c (word s)
+
+    word  : String → List String
+    word []      = []
+    word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s)
+
+open Helpers
+
+lines : String → List String
+lines []         = []
+lines ('\n' ∷ s) = [] ∷ lines s
+lines (c    ∷ s) = cons c (lines s)
+
+words : String → List String
+words [] = []
+words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s
+
+unlines : List String → String
+unlines = concatMap (_++ "\n")
+
+unwords : List String → String
+unwords [] = ""
+unwords (w ∷ []) = w
+unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws
diff --git a/lib/base/Haskell/Data/Traversable.agda b/lib/base/Haskell/Data/Traversable.agda
new file mode 100644
index 00000000..569f8623
--- /dev/null
+++ b/lib/base/Haskell/Data/Traversable.agda
@@ -0,0 +1,110 @@
+module Haskell.Data.Traversable where
+
+open import Haskell.Prim hiding (s)
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Functor hiding (module Instances)
+open import Haskell.Prim.Applicative hiding (module Instances)
+open import Haskell.Prim.Monad hiding (module Instances)
+
+open import Haskell.Prim.Functor public
+  using () renaming (module Instances to FunctorInstances)
+open import Haskell.Prim.Applicative public
+  using () renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.Monad public
+  using () renaming (module Instances to MonadInstances)
+open import Haskell.Prim.Traversable public
+  renaming (module Instances to TraversableInstances)
+
+
+private variable s : Type
+
+for : ⦃ Traversable t ⦄ → ⦃ Applicative f ⦄ → t a → (a → f b) → f (t b)
+for = flip traverse
+
+forM :  ⦃ Traversable t ⦄ → ⦃ Monad m ⦄ → t a → (a → m b) → m (t b)
+forM = flip mapM
+
+module Helpers where
+  record State (s a : Type) : Type where
+    constructor mkState
+    pattern
+    field run : s → s × a
+
+  record StateT (s : Type) (m : Type → Type) (a : Type) : Type where
+    constructor mkStateT
+    pattern
+    field run : s → m (s × a)
+
+  instance
+    open DefaultFunctor
+    open ApplicativeFrom<*>
+
+    iDefaultFunctorState : DefaultFunctor (State s)
+    iDefaultFunctorState .fmap f (mkState k) = mkState $ λ s → let s' , v = k s in s' , f v
+
+    iFunctorState : Functor (State s)
+    iFunctorState = record { DefaultFunctor iDefaultFunctorState }
+
+    iDefaultApplicativeStateL : ApplicativeFrom<*> (State s)
+    iDefaultApplicativeStateL .pure x = mkState (λ s → s , x)
+    iDefaultApplicativeStateL ._<*>_ (mkState kf) (mkState kx) = mkState $ λ s →
+      let s' , f = kf s
+          s'' , x = kx s'
+      in s'' , f x
+
+    iApplicativeStateL : Applicative (State s)
+    iApplicativeStateL = record { ApplicativeFrom<*> iDefaultApplicativeStateL }
+
+    iDefaultApplicativeStateR : ApplicativeFrom<*> (State s)
+    iDefaultApplicativeStateR .pure x = mkState (λ s → s , x)
+    iDefaultApplicativeStateR ._<*>_ (mkState kf) (mkState kx) = mkState $ λ s →
+      let s' , x = kx s
+          s'' , f = kf s'
+      in s'' , f x
+
+    iApplicativeStateR : Applicative (State s)
+    iApplicativeStateR = record { ApplicativeFrom<*> iDefaultApplicativeStateR }
+
+    iDefaultFunctorStateT : ⦃ Monad m ⦄ → DefaultFunctor (StateT s m)
+    iDefaultFunctorStateT .fmap f (mkStateT kx) = mkStateT $ λ s → do
+      s' , x ← kx s
+      return (s' , f x)
+
+    iFunctorStateT : ⦃ Monad m ⦄ → Functor (StateT s m)
+    iFunctorStateT = record { DefaultFunctor iDefaultFunctorStateT }
+
+    iDefaultApplicativeStateT : ⦃ Monad m ⦄ → ApplicativeFrom<*> (StateT s m)
+    iDefaultApplicativeStateT .pure x = mkStateT (λ s → return (s , x))
+    iDefaultApplicativeStateT ._<*>_ (mkStateT kf) (mkStateT kx) = mkStateT $ λ s → do
+      s' , f ← kf s
+      s'' , x ← kx s'
+      return (s'' , f x)
+
+    iApplicativeStateT : ⦃ Monad m ⦄ → Applicative (StateT s m)
+    iApplicativeStateT = record { ApplicativeFrom<*> iDefaultApplicativeStateT}
+
+    iDefaultMonadStateT : ⦃ Monad m ⦄ → DefaultMonad (StateT s m)
+    iDefaultMonadStateT .DefaultMonad._>>=_ m k = mkStateT $ λ s → do
+      s' , x ← StateT.run m s
+      StateT.run (k x) s'
+
+    iMonadStateT : ⦃ Monad m ⦄ → Monad (StateT s m)
+    iMonadStateT = record { DefaultMonad iDefaultMonadStateT }
+
+open Helpers
+
+mapAccumL : ⦃ Traversable t ⦄ → (s → a → s × b) → s → t a → s × t b
+mapAccumL ⦃ iTraversable ⦄ f s t = State.run (traverse ⦃ iTraversable ⦄ ⦃ iApplicativeStateL ⦄ (mkState ∘ flip f) t) s
+
+mapAccumR : ⦃ Traversable t ⦄ → (s → a → s × b) → s → t a → s × t b
+mapAccumR ⦃ iTraversable ⦄ f s t = State.run (traverse ⦃ iTraversable ⦄ ⦃ iApplicativeStateR ⦄ (mkState ∘ flip f) t) s
+
+mapAccumM : ⦃ Monad m ⦄ → ⦃ Traversable t ⦄ → (s → a → m (s × b)) → s → t a → m (s × t b)
+mapAccumM f s t = StateT.run (mapM (mkStateT ∘ flip f) t) s
+
+forAccumM : ⦃ Monad m ⦄ → ⦃ Traversable t ⦄ → s → t a → (s → a → m (s × b)) → m (s × t b)
+forAccumM s t f = mapAccumM f s t
+
+-- Omitted for now:
+-- - 'fmapDefault :: Traversable t => (a -> b) -> t a -> t b'
+-- - 'foldMapDefault :: (Traversable t, Monoid m) => (a -> m) -> t a -> m'
diff --git a/lib/base/Haskell/Extra/Refinement.agda b/lib/base/Haskell/Extra/Refinement.agda
index d8621f6a..4d0a4b7a 100644
--- a/lib/base/Haskell/Extra/Refinement.agda
+++ b/lib/base/Haskell/Extra/Refinement.agda
@@ -1,10 +1,12 @@
 module Haskell.Extra.Refinement where
 
-open import Haskell.Prelude
+open import Haskell.Prim
+open import Haskell.Prim.Maybe
 open import Agda.Primitive
 
+
 private variable
-  ℓ ℓ′ : Level
+  ℓ′ : Level
 
 record ∃ (a : Type ℓ) (@0 P : a → Type ℓ′) : Type (ℓ ⊔ ℓ′) where
   constructor _⟨⟩
diff --git a/lib/base/Haskell/Law/List.agda b/lib/base/Haskell/Law/List.agda
index 377b91be..7a613cbc 100644
--- a/lib/base/Haskell/Law/List.agda
+++ b/lib/base/Haskell/Law/List.agda
@@ -2,9 +2,11 @@ module Haskell.Law.List where
 
 open import Haskell.Law.Equality
 open import Haskell.Prim renaming (addNat to _+ₙ_)
-open import Haskell.Prim.Foldable
 open import Haskell.Prim.List
 open import Haskell.Prim.Applicative
+open import Haskell.Prim.Foldable
+open import Haskell.Data.Foldable
+
 
 []≠∷ : ∀ x (xs : List a) → [] ≠ x ∷ xs
 []≠∷ x xs ()
diff --git a/lib/base/Haskell/Law/Monoid/Def.agda b/lib/base/Haskell/Law/Monoid/Def.agda
index 880d8e93..bf88e06e 100644
--- a/lib/base/Haskell/Law/Monoid/Def.agda
+++ b/lib/base/Haskell/Law/Monoid/Def.agda
@@ -4,7 +4,10 @@ open import Haskell.Prim
 open import Haskell.Prim.Tuple
 
 open import Haskell.Prim.Foldable
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
 open import Haskell.Prim.Monoid
+  renaming (module Instances to MonoidInstances)
 
 open import Haskell.Law.Semigroup.Def
 
diff --git a/lib/base/Haskell/Law/Semigroup/Def.agda b/lib/base/Haskell/Law/Semigroup/Def.agda
index d743fcee..34c54fdf 100644
--- a/lib/base/Haskell/Law/Semigroup/Def.agda
+++ b/lib/base/Haskell/Law/Semigroup/Def.agda
@@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.Def where
 open import Haskell.Prim
 open import Haskell.Prim.Tuple
 
-open import Haskell.Prim.Monoid
+open import Haskell.Prim.Semigroup
 
 record IsLawfulSemigroup (a : Type) ⦃ iSemigroupA : Semigroup a ⦄ : Type₁ where
   field
diff --git a/lib/base/Haskell/Law/Semigroup/Either.agda b/lib/base/Haskell/Law/Semigroup/Either.agda
index 084f3926..7540e274 100644
--- a/lib/base/Haskell/Law/Semigroup/Either.agda
+++ b/lib/base/Haskell/Law/Semigroup/Either.agda
@@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.Either where
 open import Haskell.Prim
 open import Haskell.Prim.Either
 
-open import Haskell.Prim.Monoid
+open import Haskell.Prim.Semigroup
 
 open import Haskell.Law.Equality
 open import Haskell.Law.Semigroup.Def
diff --git a/lib/base/Haskell/Law/Semigroup/List.agda b/lib/base/Haskell/Law/Semigroup/List.agda
index b5518bdb..53dcb1f2 100644
--- a/lib/base/Haskell/Law/Semigroup/List.agda
+++ b/lib/base/Haskell/Law/Semigroup/List.agda
@@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.List where
 open import Haskell.Prim
 open import Haskell.Prim.List
 
-open import Haskell.Prim.Monoid
+open import Haskell.Prim.Semigroup
 
 open import Haskell.Law.Equality
 open import Haskell.Law.List
diff --git a/lib/base/Haskell/Law/Semigroup/Maybe.agda b/lib/base/Haskell/Law/Semigroup/Maybe.agda
index 7387d3a4..0757c634 100644
--- a/lib/base/Haskell/Law/Semigroup/Maybe.agda
+++ b/lib/base/Haskell/Law/Semigroup/Maybe.agda
@@ -3,7 +3,7 @@ module Haskell.Law.Semigroup.Maybe where
 open import Haskell.Prim
 open import Haskell.Prim.Maybe
 
-open import Haskell.Prim.Monoid
+open import Haskell.Prim.Semigroup
 
 open import Haskell.Law.Equality
 open import Haskell.Law.Semigroup.Def
diff --git a/lib/base/Haskell/Prelude.agda b/lib/base/Haskell/Prelude.agda
index dbe4b34e..c071a92e 100644
--- a/lib/base/Haskell/Prelude.agda
+++ b/lib/base/Haskell/Prelude.agda
@@ -1,49 +1,316 @@
 {-# OPTIONS --no-auto-inline #-}
+
 module Haskell.Prelude where
 
-open import Haskell.Prim
-open Haskell.Prim public using
-  ( Type;
-    Bool; True; False; Char; Integer;
-    List; []; _∷_; Nat; zero; suc; ⊤; tt;
-    TypeError; ⊥; iNumberNat; lengthNat;
-    IsTrue; IsFalse; NonEmpty;
-    All; allNil; allCons;
-    Any; anyHere; anyThere;
-    id; _∘_; _$_; flip; const;
-    if_then_else_; case_of_;
-    Number; fromNat; Negative; fromNeg;
-    IsString; fromString;
-    _≡_; refl;
-    a; b; c; d; e; f; m; s; t )
-
-open import Haskell.Prim.Absurd      public
-open import Haskell.Prim.Applicative public
-open import Haskell.Prim.Bool        public
-open import Haskell.Prim.Bounded     public
-open import Haskell.Prim.Char        public
-open import Haskell.Prim.Double      public
-open import Haskell.Prim.Either      public
-open import Haskell.Prim.Enum        public
-open import Haskell.Prim.Eq          public
-open import Haskell.Prim.Foldable    public
-open import Haskell.Prim.Functor     public
-open import Haskell.Prim.Int         public
-open import Haskell.Prim.Integer     public
-open import Haskell.Prim.IO          public
-open import Haskell.Prim.List        public
-open import Haskell.Prim.Maybe       public
-open import Haskell.Prim.Monad       public
-open import Haskell.Prim.Monoid      public
-open import Haskell.Prim.Num         public
-open import Haskell.Prim.Ord         public
-open import Haskell.Prim.Show        public
-open import Haskell.Prim.String      public
-open import Haskell.Prim.Traversable public
-open import Haskell.Prim.Tuple       public hiding (first; second; _***_)
-open import Haskell.Prim.Word        public
-
--- Problematic features
+open import Haskell.Prim                public
+  using (Type;
+         Bool; True; False; Char; Integer;
+         List; []; _∷_; Nat; zero; suc; ⊤; tt;
+         TypeError; ⊥; iNumberNat;
+         IsTrue; IsFalse; NonEmpty;
+         All; allNil; allCons;
+         Any; anyHere; anyThere;
+         id; _∘_; _$_; flip; const;
+         if_then_else_; case_of_;
+         Number; fromNat; Negative; fromNeg;
+         IsString; fromString;
+         _≡_; refl;
+         a; b; c; d; e; f; m; s; t)
+open import Haskell.Prim.Absurd         public
+open import Haskell.Prim.Bool           public
+open import Haskell.Prim.Bounded        public
+  renaming (module Instances to BoundedInstances)
+open import Haskell.Prim.Char           public
+open import Haskell.Prim.Double         public
+open import Haskell.Prim.Either         public
+open import Haskell.Prim.Enum           public
+  renaming (module Instances to EnumInstances)
+open import Haskell.Prim.Int            public
+open import Haskell.Prim.Integer        public
+open import Haskell.Prim.IO             public
+  hiding (returnIO; bindIO; failIO; mplusIO)
+open import Haskell.Prim.Maybe          public
+open import Haskell.Prim.Tuple          public hiding (first; second; _***_)
+open import Haskell.Prim.Word           public
+open import Haskell.Prim.Eq             public
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord            public
+  renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Num            public
+  renaming (module Instances to NumInstances)
+open import Haskell.Prim.Show           public
+  renaming (module Instances to ShowInstances)
+open import Haskell.Prim.Semigroup      public
+  renaming (module Instances to SemigroupInstances)
+open import Haskell.Prim.Monoid         public
+  renaming (module Instances to MonoidInstances)
+
+-- Explicitly reexport definitions from Haskell.Data.Functor (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Data.Functor
+
+module Functor = Haskell.Data.Functor.Functor
+module DefaultFunctor = Haskell.Data.Functor.DefaultFunctor
+module FunctorInstances = Haskell.Data.Functor.FunctorInstances
+
+open Functor ⦃ ... ⦄ public
+
+Functor : (f : Type → Type) → Type₁
+Functor = Haskell.Data.Functor.Functor
+
+DefaultFunctor : (f : Type → Type) → Type₁
+DefaultFunctor = Haskell.Data.Functor.DefaultFunctor
+
+infixl 4 _<$>_
+_<$>_ : ⦃ Haskell.Data.Functor.Functor f ⦄ → (a → b) → f a → f b
+_<$>_ = Haskell.Data.Functor._<$>_
+
+-- Explicitly reexport definitions from Haskell.Control.Applicative (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Control.Applicative
+
+module Applicative = Haskell.Control.Applicative.Applicative
+module ApplicativeFrom<*> = Haskell.Control.Applicative.ApplicativeFrom<*>
+module ApplicativeFromLiftA2 = Haskell.Control.Applicative.ApplicativeFromLiftA2
+module ApplicativeInstances = Haskell.Control.Applicative.ApplicativeInstances
+
+open Applicative ⦃ ... ⦄ public
+
+Applicative : (f : Type → Type) → Type₁
+Applicative = Haskell.Control.Applicative.Applicative
+
+ApplicativeFrom<*> : (f : Type → Type) → Type₁
+ApplicativeFrom<*> = Haskell.Control.Applicative.ApplicativeFrom<*>
+
+ApplicativeFromLiftA2 : (f : Type → Type) → Type₁
+ApplicativeFromLiftA2 = Haskell.Control.Applicative.ApplicativeFromLiftA2
+
+-- Explicitly reexport definitions from Haskell.Control.Monad (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Control.Monad
+
+module Monad = Haskell.Control.Monad.Monad
+module DefaultMonad = Haskell.Control.Monad.DefaultMonad
+module MonadInstances = Haskell.Control.Monad.MonadInstances
+module Dont = Haskell.Control.Monad.Dont
+
+module MonadFail = Haskell.Control.Monad.MonadFail
+module MonadFailInstances = Haskell.Control.Monad.MonadFailInstances
+
+open Monad ⦃ ... ⦄ public
+open MonadFail ⦃ ... ⦄ public
+
+Monad : (m : Type → Type) → Type₁
+Monad = Haskell.Control.Monad.Monad
+
+DefaultMonad : (m : Type → Type) → Type₁
+DefaultMonad = Haskell.Control.Monad.DefaultMonad
+
+MonadFail : (m : Type → Type) → Type₁
+MonadFail = Haskell.Control.Monad.MonadFail
+
+infixr 1 _=<<_
+_=<<_ : ⦃ Monad m ⦄ → (a → m b) → m a → m b
+_=<<_ = Haskell.Control.Monad._=<<_
+
+-- Explicitly reexport definitions from Haskell.Data.Foldable (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Data.Foldable
+
+module Foldable = Haskell.Data.Foldable.Foldable
+  hiding (fold; foldMap'; foldr'; toList; null; length)
+module DefaultFoldable = Haskell.Data.Foldable.DefaultFoldable
+module FoldableInstances = Haskell.Data.Foldable.FoldableInstances
+
+open Foldable ⦃ ... ⦄ public
+
+Foldable : (t : Type → Type) → Type₁
+Foldable = Haskell.Data.Foldable.Foldable
+
+DefaultFoldable : (t : Type → Type) → Type₁
+DefaultFoldable = Haskell.Data.Foldable.DefaultFoldable
+
+mapM₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → (a → m b) → t a → m ⊤
+mapM₋ = Haskell.Data.Foldable.mapM₋
+
+sequence₋ : ⦃ Foldable t ⦄ → ⦃ Monad m ⦄ → t (m a) → m ⊤
+sequence₋ = Haskell.Data.Foldable.sequence₋
+
+-- Explicitly reexport definitions from Haskell.Data.Traversable (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Data.Traversable
+
+module Traversable = Haskell.Data.Traversable.Traversable
+module DefaultTraversable = Haskell.Data.Traversable.DefaultTraversable
+module TraversableInstances = Haskell.Data.Traversable.TraversableInstances
+
+open Traversable ⦃ ... ⦄ public
+
+Traversable : (t : Type → Type) → Type₁
+Traversable = Haskell.Data.Traversable.Traversable
+
+-- Explicitly reexport definitions from Haskell.Data.String (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Data.String
+
+String : Type
+String = Haskell.Data.String.String
+
+instance iIsStringString : IsString String
+iIsStringString = Haskell.Data.String.iIsStringString
+
+lines : String → List String
+lines = Haskell.Data.String.lines
+
+words : String → List String
+words = Haskell.Data.String.words
+
+unlines : List String → String
+unlines = Haskell.Data.String.unlines
+
+unwords : List String → String
+unwords = Haskell.Data.String.unwords
+
+-- Explicitly reexport definitions from Haskell.Data.List (update these
+-- to use Agda's builtin reexport mechanism as soon as issue #126 is fixed):
+import Haskell.Data.List
+
+infixr 5 _++_
+_++_ : List a → List a → List a
+_++_ = Haskell.Data.List._++_
+
+map : (a → b) → List a → List b
+map = Haskell.Data.List.map
+
+reverse : List a → List a
+reverse = Haskell.Data.List.reverse
+
+lengthNat : List a → Nat
+lengthNat = Haskell.Data.List.lengthNat
+
+length : ⦃ Foldable t ⦄ → t a → Int
+length = Haskell.Data.List.length
+
+head : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
+head = Haskell.Data.List.head
+
+last : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
+last = Haskell.Data.List.last
+
+tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
+tail = Haskell.Data.List.tail
+
+init : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
+init = Haskell.Data.List.init
+
+infixl 9 _!!ᴺ_
+_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a
+_!!ᴺ_ = Haskell.Data.List._!!ᴺ_
+
+infixl 9 _!!_
+_!!_ : (xs : List a) (n : Int)
+     → ⦃ @0 _ : IsNonNegativeInt n ⦄
+     → ⦃ @0 _  : IsTrue (intToNat n < lengthNat xs) ⦄ → a
+_!!_ = Haskell.Data.List._!!_
+
+splitAtNat : (n : Nat) → List a → List a × List a
+splitAtNat = Haskell.Data.List.splitAtNat
+
+splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a
+splitAt = Haskell.Data.List.splitAt
+
+lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
+lookup = Haskell.Data.List.lookup
+
+null : ⦃ Foldable t ⦄ → t a → Bool
+null = Haskell.Data.List.null
+
+scanl : (b → a → b) → b → List a → List b
+scanl = Haskell.Data.List.scanl
+
+scanl1 : (a → a → a) → List a → List a
+scanl1 = Haskell.Data.List.scanl1
+
+scanr : (a → b → b) → b → List a → List b
+scanr = Haskell.Data.List.scanr
+
+scanr1 : (a → a → a) → List a → List a
+scanr1 = Haskell.Data.List.scanr1
+
+replicateNat : Nat → a → List a
+replicateNat = Haskell.Data.List.replicateNat
+
+replicate : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → a → List a
+replicate = Haskell.Data.List.replicate
+
+takeNat : Nat → List a → List a
+takeNat = Haskell.Data.List.takeNat
+
+take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
+take = Haskell.Data.List.take
+
+dropNat : Nat → List a → List a
+dropNat = Haskell.Data.List.dropNat
+
+drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
+drop = Haskell.Data.List.drop
+
+takeWhile : (a → Bool) → List a → List a
+takeWhile = Haskell.Data.List.takeWhile
+
+dropWhile : (a → Bool) → List a → List a
+dropWhile = Haskell.Data.List.dropWhile
+
+filter : (a → Bool) → List a → List a
+filter = Haskell.Data.List.filter
+
+span : (a → Bool) → List a → List a × List a
+span = Haskell.Data.List.span
+
+break : (a → Bool) → List a → List a × List a
+break = Haskell.Data.List.break
+
+zip : List a → List b → List (a × b)
+zip = Haskell.Data.List.zip
+
+zip3 : List a → List b → List c → List (a × b × c)
+zip3 = Haskell.Data.List.zip3
+
+zipWith : (a → b → c) → List a → List b → List c
+zipWith = Haskell.Data.List.zipWith
+
+zipWith3 : (a → b → c → d) → List a → List b → List c → List d
+zipWith3 = Haskell.Data.List.zipWith3
+
+unzip : List (a × b) → List a × List b
+unzip = Haskell.Data.List.unzip
+
+unzip3 : List (a × b × c) → List a × List b × List c
+unzip3 = Haskell.Data.List.unzip3
+
+and : ⦃ Foldable t ⦄ → t Bool → Bool
+and = Haskell.Data.List.and
+
+or : ⦃ Foldable t ⦄ → t Bool → Bool
+or = Haskell.Data.List.or
+
+any : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
+any = Haskell.Data.List.any
+
+all : ⦃ Foldable t ⦄ → (a → Bool) → t a → Bool
+all = Haskell.Data.List.all
+
+concat : ⦃ Foldable t ⦄ → t (List a) → List a
+concat = Haskell.Data.List.concat
+
+concatMap : ⦃ Foldable t ⦄ → (a → List b) → t a → List b
+concatMap = Haskell.Data.List.concatMap
+
+notElem : ⦃ Foldable t ⦄ → ⦃ Eq a ⦄ → a → t a → Bool
+notElem = Haskell.Data.List.notElem
+
+
+-- Problematic features:
 --  - [Partial]:  Could pass implicit/instance arguments to prove totality.
 --  - [Float]:    Or Float (Agda floats are Doubles)
 --  - [Infinite]: Define colists and map to Haskell lists?
@@ -51,6 +318,7 @@ open import Haskell.Prim.Word        public
 -- Missing from the Haskell Prelude:
 --
 --     Float        [Float]
+--
 --     Rational
 --
 --     Real(toRational),
@@ -61,31 +329,23 @@ open import Haskell.Prim.Word        public
 --     RealFrac(properFraction, truncate, round, ceiling, floor),
 --     RealFloat(floatRadix, floatDigits, floatRange, decodeFloat,
 --               encodeFloat, exponent, significand, scaleFloat, isNaN,
---               isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2),
+--               isInfinite, isDenormalized, isIEEE, isNegativeZero, atan2)
 --
 --     subtract, even, odd, gcd, lcm, (^), (^^),
---     fromIntegral, realToFrac,
---
---     foldr1, foldl1, maximum, minimum      [Partial]
+--     fromIntegral, realToFrac
 --
 --     until [Partial]
 --
 --     iterate, repeat, cycle          [Infinite]
 --
 --     ReadS, Read(readsPrec, readList),
---     reads, readParen, read, lex,
+--     reads, readParen, read, lex
 --
---     IO, putChar, putStr, putStrLn, print,
---     getChar, getLine, getContents, interact,
---     FilePath, readFile, writeFile, appendFile, readIO, readLn,
---     IOError, ioError, userError,
-
+--     readIO, readLn,
+--     IOError, ioError, userError
 
---------------------------------------------------
--- Functions
 
 infixr 0 _$!_
-
 _$!_ : (a → b) → a → b
 _$!_ = _$_
 
@@ -104,32 +364,6 @@ error {i = ()} err
 errorWithoutStackTrace : {@0 @(tactic absurd) i : ⊥} → String → a
 errorWithoutStackTrace {i = ()} err
 
--------------------------------------------------
--- More List functions
---   These uses Eq, Ord, or Foldable, so can't go in Prim.List without
---   turning those dependencies around.
-
-reverse : List a → List a
-reverse = foldl (flip _∷_) []
-
-infixl 9 _!!_ _!!ᴺ_
-
-_!!ᴺ_ : (xs : List a) (n : Nat) → @0 ⦃ IsTrue (n < lengthNat xs) ⦄ → a
-(x ∷ xs) !!ᴺ zero  = x
-(x ∷ xs) !!ᴺ suc n = xs !!ᴺ n
-
-_!!_ : (xs : List a) (n : Int)
-     → ⦃ @0 nn : IsNonNegativeInt n ⦄
-     → ⦃ @0 _  : IsTrue (intToNat n {{nn}} < lengthNat xs) ⦄ → a
-xs !! n = xs !!ᴺ intToNat n
-
-lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
-lookup x []              = Nothing
-lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
-
-
--------------------------------------------------
--- Unsafe functions
 
 coerce : @0 a ≡ b → a → b
 coerce refl x = x
@@ -137,4 +371,3 @@ coerce refl x = x
 IsJust : Maybe a → Type
 IsJust Nothing  = ⊥
 IsJust (Just _) = ⊤
-
diff --git a/lib/base/Haskell/Prim.agda b/lib/base/Haskell/Prim.agda
index 43b52006..295af905 100644
--- a/lib/base/Haskell/Prim.agda
+++ b/lib/base/Haskell/Prim.agda
@@ -22,6 +22,7 @@ open import Agda.Builtin.Word       public renaming (primWord64ToNat to w2n; pri
 open import Agda.Builtin.Strict     public
 open import Agda.Builtin.List       public
 
+
 variable
   @0 ℓ : Level
   a b c d e : Type
@@ -65,6 +66,7 @@ if True  then x else y = x
 the : (@0 a : Type ℓ) -> a -> a
 the _ x = x
 
+
 --------------------------------------------------
 -- Agda strings
 
@@ -83,14 +85,6 @@ instance
   iNumberNat .fromNat n = n
 
 
---------------------------------------------------
--- Lists
-
-lengthNat : List a → Nat
-lengthNat []       = 0
-lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs)
-
-
 --------------------------------------------------
 -- Proof things
 
@@ -99,7 +93,7 @@ data ⊥ : Type where
 magic : {A : Type} → ⊥ → A
 magic ()
 
---principle of explosion
+-- Principle of explosion
 exFalso : {x : Bool} → (x ≡ True) → (x ≡ False) → ⊥
 exFalso {False} () b
 exFalso {True} a ()
diff --git a/lib/base/Haskell/Prim/Absurd.agda b/lib/base/Haskell/Prim/Absurd.agda
index 349955dc..1fd4003d 100644
--- a/lib/base/Haskell/Prim/Absurd.agda
+++ b/lib/base/Haskell/Prim/Absurd.agda
@@ -1,12 +1,12 @@
-
 module Haskell.Prim.Absurd where
 
 open import Haskell.Prim
+open import Haskell.Prim.List using (lengthNat)
 
 open import Agda.Builtin.Reflection renaming (bindTC to _>>=_; absurd to absurdP)
 
-private
 
+private
   pattern vArg x = arg (arg-info visible (modality relevant quantity-ω)) x
 
   refute : Nat → Term
diff --git a/lib/base/Haskell/Prim/Alternative.agda b/lib/base/Haskell/Prim/Alternative.agda
new file mode 100644
index 00000000..74f740d5
--- /dev/null
+++ b/lib/base/Haskell/Prim/Alternative.agda
@@ -0,0 +1,42 @@
+module Haskell.Prim.Alternative where
+
+open import Haskell.Prim
+open import Haskell.Prim.Applicative
+  renaming (module Instances to ApplicativeInstances)
+open import Haskell.Prim.IO
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.String
+
+
+--------------------------------------------------------------------------------
+-- Alternative
+
+-- ** base
+record Alternative (f : Type → Type) : Type₁ where
+  infixl 3 _<|>_
+  field
+    empty : f a
+    _<|>_ : f a → f a → f a
+    overlap ⦃ super ⦄ : Applicative f
+
+-- ** export
+open Alternative ⦃...⦄ public
+{-# COMPILE AGDA2HS Alternative existing-class #-}
+
+-- ** instances
+module Instances where
+  instance
+    iAlternativeList : Alternative List
+    iAlternativeList .empty = []
+    iAlternativeList ._<|>_ = _++_
+
+    iAlternativeMaybe : Alternative Maybe
+    iAlternativeMaybe .empty = Nothing
+    iAlternativeMaybe ._<|>_ (Just x) _ = Just x
+    iAlternativeMaybe ._<|>_ Nothing  y = y
+
+    iAlternativeIO : Alternative IO
+    iAlternativeIO .empty = failIO "mzero"
+    iAlternativeIO ._<|>_ = mplusIO
+open Instances public
diff --git a/lib/base/Haskell/Prim/Applicative.agda b/lib/base/Haskell/Prim/Applicative.agda
index 2629f90e..9e4efccb 100644
--- a/lib/base/Haskell/Prim/Applicative.agda
+++ b/lib/base/Haskell/Prim/Applicative.agda
@@ -1,30 +1,54 @@
 module Haskell.Prim.Applicative where
 
 open import Haskell.Prim
-open import Haskell.Prim.Either
-open import Haskell.Prim.Foldable
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
+open import Haskell.Prim.Monoid
+  renaming (module Instances to MonoidInstances)
 open import Haskell.Prim.Functor
+  renaming (module Instances to FunctorInstances)
+open import Haskell.Prim.Foldable
+  renaming (module Instances to FoldableInstances)
+open import Haskell.Prim.Either
 open import Haskell.Prim.IO
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
-open import Haskell.Prim.Monoid
 open import Haskell.Prim.Tuple
 
 
---------------------------------------------------
+--------------------------------------------------------------------------------
 -- Applicative
 
 -- ** base
 record Applicative (f : Type → Type) : Type₁ where
   infixl 4 _<*>_ _<*_ _*>_
   field
-    pure  : a → f a
-    _<*>_ : f (a → b) → f a → f b
+    pure   : a → f a
+    _<*>_  : f (a → b) → f a → f b
+    liftA2 : (a → b → c) → f a → f b → f c
     overlap ⦃ super ⦄ : Functor f
     _<*_ : f a → f b → f a
     _*>_ : f a → f b → f b
+
 -- ** defaults
-record DefaultApplicative (f : Type → Type) : Type₁ where
+record ApplicativeFromLiftA2 (f : Type → Type) : Type₁ where
+  constructor mk
+  infixl 4 _<*>_ _<*_ _*>_
+  field
+    pure  : a → f a
+    liftA2 : (a → b → c) → f a → f b → f c
+    overlap ⦃ super ⦄ : Functor f
+
+  _<*>_  : f (a → b) → f a → f b
+  _<*>_ = liftA2 id
+
+  _<*_ : f a → f b → f a
+  _<*_ = liftA2 const
+
+  _*>_ : f a → f b → f b
+  x *> y = (id <$ x) <*> y
+
+record ApplicativeFrom<*> (f : Type → Type) : Type₁ where
   constructor mk
   infixl 4 _<*>_ _<*_ _*>_
   field
@@ -32,61 +56,73 @@ record DefaultApplicative (f : Type → Type) : Type₁ where
     _<*>_ : f (a → b) → f a → f b
     overlap ⦃ super ⦄ : Functor f
 
+  liftA2 : (a → b → c) → f a → f b → f c
+  liftA2 f x y = fmap f x <*> y
+
   _<*_ : f a → f b → f a
-  x <* y = const <$> x <*> y
+  x <* y = fmap const x <*> y
 
   _*>_ : f a → f b → f b
-  x *> y = const id <$> x <*> y
+  x *> y = fmap (const id) x <*> y
+
 -- ** export
 open Applicative ⦃...⦄ public
 {-# COMPILE AGDA2HS Applicative existing-class #-}
+
 -- ** instances
-instance
-  open DefaultApplicative
+module Instances where
+  instance
+    open ApplicativeFrom<*>
+
+    iDefaultApplicativeList : ApplicativeFrom<*> List
+    iDefaultApplicativeList .pure x = x ∷ []
+    iDefaultApplicativeList ._<*>_ fs xs = foldMap (λ f → map f xs) fs
 
-  iDefaultApplicativeList : DefaultApplicative List
-  iDefaultApplicativeList .pure x = x ∷ []
-  iDefaultApplicativeList ._<*>_ fs xs = concatMap (λ f → map f xs) fs
+    iApplicativeList : Applicative List
+    iApplicativeList = record {ApplicativeFrom<*> iDefaultApplicativeList}
 
-  iApplicativeList : Applicative List
-  iApplicativeList = record {DefaultApplicative iDefaultApplicativeList}
+    iDefaultApplicativeMaybe : ApplicativeFrom<*> Maybe
+    iDefaultApplicativeMaybe .pure = Just
+    iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x)
+    iDefaultApplicativeMaybe ._<*>_ _        _        = Nothing
 
-  iDefaultApplicativeMaybe : DefaultApplicative Maybe
-  iDefaultApplicativeMaybe .pure = Just
-  iDefaultApplicativeMaybe ._<*>_ (Just f) (Just x) = Just (f x)
-  iDefaultApplicativeMaybe ._<*>_ _        _        = Nothing
+    iApplicativeMaybe : Applicative Maybe
+    iApplicativeMaybe = record {ApplicativeFrom<*> iDefaultApplicativeMaybe}
 
-  iApplicativeMaybe : Applicative Maybe
-  iApplicativeMaybe = record {DefaultApplicative iDefaultApplicativeMaybe}
+    iDefaultApplicativeEither : ApplicativeFrom<*> (Either a)
+    iDefaultApplicativeEither .pure = Right
+    iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x)
+    iDefaultApplicativeEither ._<*>_ (Left e)  _         = Left e
+    iDefaultApplicativeEither ._<*>_ _         (Left e)  = Left e
 
-  iDefaultApplicativeEither : DefaultApplicative (Either a)
-  iDefaultApplicativeEither .pure = Right
-  iDefaultApplicativeEither ._<*>_ (Right f) (Right x) = Right (f x)
-  iDefaultApplicativeEither ._<*>_ (Left e)  _         = Left e
-  iDefaultApplicativeEither ._<*>_ _         (Left e)  = Left e
+    iApplicativeEither : Applicative (Either a)
+    iApplicativeEither = record{ApplicativeFrom<*> iDefaultApplicativeEither}
 
-  iApplicativeEither : Applicative (Either a)
-  iApplicativeEither = record{DefaultApplicative iDefaultApplicativeEither}
+    iDefaultApplicativeFun : ApplicativeFrom<*> (λ b → a → b)
+    iDefaultApplicativeFun .pure        = const
+    iDefaultApplicativeFun ._<*>_ f g x = f x (g x)
 
-  iDefaultApplicativeFun : DefaultApplicative (λ b → a → b)
-  iDefaultApplicativeFun .pure        = const
-  iDefaultApplicativeFun ._<*>_ f g x = f x (g x)
+    iApplicativeFun : Applicative (λ b → a → b)
+    iApplicativeFun = record{ApplicativeFrom<*> iDefaultApplicativeFun}
 
-  iApplicativeFun : Applicative (λ b → a → b)
-  iApplicativeFun = record{DefaultApplicative iDefaultApplicativeFun}
+    iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → ApplicativeFrom<*> (a ×_)
+    iDefaultApplicativeTuple₂ .pure x                = mempty , x
+    iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x
 
-  iDefaultApplicativeTuple₂ : ⦃ Monoid a ⦄ → DefaultApplicative (a ×_)
-  iDefaultApplicativeTuple₂ .pure x                = mempty , x
-  iDefaultApplicativeTuple₂ ._<*>_ (a , f) (b , x) = a <> b , f x
+    iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
+    iApplicativeTuple₂ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₂}
 
-  iApplicativeTuple₂ : ⦃ Monoid a ⦄ → Applicative (a ×_)
-  iApplicativeTuple₂ = record{DefaultApplicative iDefaultApplicativeTuple₂}
+    iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ApplicativeFrom<*> (a × b ×_)
+    iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x
+    iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x
 
-  iDefaultApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultApplicative (a × b ×_)
-  iDefaultApplicativeTuple₃ .pure x = mempty , mempty , x
-  iDefaultApplicativeTuple₃ ._<*>_ (a , u , f) (b , v , x) = a <> b , u <> v , f x
+    iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
+    iApplicativeTuple₃ = record{ApplicativeFrom<*> iDefaultApplicativeTuple₃}
 
-  iApplicativeTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Applicative (a × b ×_)
-  iApplicativeTuple₃ = record{DefaultApplicative iDefaultApplicativeTuple₃}
+    iDefaultApplicativeIO : ApplicativeFrom<*> IO
+    iDefaultApplicativeIO .pure = returnIO
+    iDefaultApplicativeIO ._<*>_ m1 m2 = bindIO m1 (λ f → bindIO m2 (λ x → returnIO (f x)))
 
-instance postulate iApplicativeIO : Applicative IO
+    iApplicativeIO : Applicative IO
+    iApplicativeIO = record{ApplicativeFrom<*> iDefaultApplicativeIO}
+open Instances public
diff --git a/lib/base/Haskell/Prim/Bounded.agda b/lib/base/Haskell/Prim/Bounded.agda
index bd9ae0d5..515526a4 100644
--- a/lib/base/Haskell/Prim/Bounded.agda
+++ b/lib/base/Haskell/Prim/Bounded.agda
@@ -3,13 +3,16 @@ module Haskell.Prim.Bounded where
 
 open import Haskell.Prim
 open import Haskell.Prim.Eq
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord
+  renaming (module Instances to OrdInstances)
 open import Haskell.Prim.Int
 open import Haskell.Prim.Maybe
-open import Haskell.Prim.Ord
 open import Haskell.Prim.Tuple
 open import Haskell.Prim.Word
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Bounded
 
 record BoundedBelow (a : Type) : Type where
@@ -30,59 +33,61 @@ record Bounded (a : Type) : Type where
 open BoundedBelow ⦃...⦄ public
 open BoundedAbove ⦃...⦄ public
 
-instance
-  iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a
-  iBounded .Bounded.below = it
-  iBounded .Bounded.above = it
-
-instance
-  iBoundedBelowNat : BoundedBelow Nat
-  iBoundedBelowNat .minBound = 0
-
-  iBoundedBelowWord : BoundedBelow Word
-  iBoundedBelowWord .minBound = 0
-  iBoundedAboveWord : BoundedAbove Word
-  iBoundedAboveWord .maxBound = 18446744073709551615
-
-  iBoundedBelowInt : BoundedBelow Int
-  iBoundedBelowInt .minBound = -9223372036854775808
-  iBoundedAboveInt : BoundedAbove Int
-  iBoundedAboveInt .maxBound = 9223372036854775807
-
-  iBoundedBelowBool : BoundedBelow Bool
-  iBoundedBelowBool .minBound = False
-  iBoundedAboveBool : BoundedAbove Bool
-  iBoundedAboveBool .maxBound = True
-
-  iBoundedBelowChar : BoundedBelow Char
-  iBoundedBelowChar .minBound = '\0'
-  iBoundedAboveChar : BoundedAbove Char
-  iBoundedAboveChar .maxBound = '\1114111'
-
-  iBoundedBelowUnit : BoundedBelow ⊤
-  iBoundedBelowUnit .minBound = tt
-
-  iBoundedAboveUnit : BoundedAbove ⊤
-  iBoundedAboveUnit .maxBound = tt
-
-  iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄
-                      → BoundedBelow (a × b)
-  iBoundedBelowTuple₂ .minBound = minBound , minBound
-  iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄
-                      → BoundedAbove (a × b)
-  iBoundedAboveTuple₂ .maxBound = maxBound , maxBound
-
-  iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄
-                      → BoundedBelow (a × b × c)
-  iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound
-  iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄
-                      → BoundedAbove (a × b × c)
-  iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound
-
-  iBoundedBelowOrdering : BoundedBelow Ordering
-  iBoundedBelowOrdering .minBound = LT
-  iBoundedAboveOrdering : BoundedAbove Ordering
-  iBoundedAboveOrdering .maxBound = GT
+module Instances where
+  instance
+    iBounded : ⦃ BoundedBelow a ⦄ → ⦃ BoundedAbove a ⦄ → Bounded a
+    iBounded .Bounded.below = it
+    iBounded .Bounded.above = it
+
+  instance
+    iBoundedBelowNat : BoundedBelow Nat
+    iBoundedBelowNat .minBound = 0
+
+    iBoundedBelowWord : BoundedBelow Word
+    iBoundedBelowWord .minBound = 0
+    iBoundedAboveWord : BoundedAbove Word
+    iBoundedAboveWord .maxBound = 18446744073709551615
+
+    iBoundedBelowInt : BoundedBelow Int
+    iBoundedBelowInt .minBound = -9223372036854775808
+    iBoundedAboveInt : BoundedAbove Int
+    iBoundedAboveInt .maxBound = 9223372036854775807
+
+    iBoundedBelowBool : BoundedBelow Bool
+    iBoundedBelowBool .minBound = False
+    iBoundedAboveBool : BoundedAbove Bool
+    iBoundedAboveBool .maxBound = True
+
+    iBoundedBelowChar : BoundedBelow Char
+    iBoundedBelowChar .minBound = '\0'
+    iBoundedAboveChar : BoundedAbove Char
+    iBoundedAboveChar .maxBound = '\1114111'
+
+    iBoundedBelowUnit : BoundedBelow ⊤
+    iBoundedBelowUnit .minBound = tt
+
+    iBoundedAboveUnit : BoundedAbove ⊤
+    iBoundedAboveUnit .maxBound = tt
+
+    iBoundedBelowTuple₂ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄
+                        → BoundedBelow (a × b)
+    iBoundedBelowTuple₂ .minBound = minBound , minBound
+    iBoundedAboveTuple₂ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄
+                        → BoundedAbove (a × b)
+    iBoundedAboveTuple₂ .maxBound = maxBound , maxBound
+
+    iBoundedBelowTuple₃ : ⦃ BoundedBelow a ⦄ → ⦃ BoundedBelow b ⦄ → ⦃ BoundedBelow c ⦄
+                        → BoundedBelow (a × b × c)
+    iBoundedBelowTuple₃ .minBound = minBound , minBound , minBound
+    iBoundedAboveTuple₃ : ⦃ BoundedAbove a ⦄ → ⦃ BoundedAbove b ⦄ → ⦃ BoundedAbove c ⦄
+                        → BoundedAbove (a × b × c)
+    iBoundedAboveTuple₃ .maxBound = maxBound , maxBound , maxBound
+
+    iBoundedBelowOrdering : BoundedBelow Ordering
+    iBoundedBelowOrdering .minBound = LT
+    iBoundedAboveOrdering : BoundedAbove Ordering
+    iBoundedAboveOrdering .maxBound = GT
+open Instances public
 
 -- Sanity checks
 
diff --git a/lib/base/Haskell/Prim/Enum.agda b/lib/base/Haskell/Prim/Enum.agda
index 344d73af..a4ae3e62 100644
--- a/lib/base/Haskell/Prim/Enum.agda
+++ b/lib/base/Haskell/Prim/Enum.agda
@@ -2,22 +2,27 @@
 module Haskell.Prim.Enum where
 
 open import Haskell.Prim
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Bounded
-open import Haskell.Prim.Either
 open import Haskell.Prim.Eq
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord
+  renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Num
+  renaming (module Instances to NumInstances)
+open import Haskell.Prim.Bounded
+  renaming (module Instances to BoundedInstances)
 open import Haskell.Prim.Functor
+  renaming (module Instances to FunctorInstances)
+open import Haskell.Prim.Bool
+open import Haskell.Prim.Either
 open import Haskell.Prim.Int
 open import Haskell.Prim.Integer
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
-open import Haskell.Prim.Num
-open import Haskell.Prim.Ord
 open import Haskell.Prim.Tuple
 open import Haskell.Prim.Word
 
 
---------------------------------------------------
+--------------------------------------------------------------------------------
 -- Enum
 --    Assumptions: unbounded enums have no constraints on their
 --    operations and bounded enums should work on all values between
@@ -82,182 +87,184 @@ open Enum ⦃...⦄ public
 
 {-# COMPILE AGDA2HS Enum existing-class #-}
 
-private
-  divNat : Nat → Nat → Nat
-  divNat a 0       = 0
-  divNat a (suc b) = div-helper 0 b a b
-
-  diff : Integer → Integer → Maybe Nat
-  diff a b =
-    case a - b of λ where
-      (pos n)    → Just n
-      (negsuc _) → Nothing
-
-  unsafeIntegerToNat : Integer → Nat
-  unsafeIntegerToNat (pos n) = n
-  unsafeIntegerToNat (negsuc _) = 0
-
-  integerFromCount : Integer → Integer → Nat → List Integer
-  integerFromCount a step 0       = []
-  integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n
-
-  integerFromTo : Integer → Integer → List Integer
-  integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a)
-
-  integerFromThenTo : (a a₁ : Integer) → @0 ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer
-  integerFromThenTo a a₁ b =
-    case compare a a₁ of λ where
-      LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a)
-      EQ → [] -- impossible
-      GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b)
-
-instance
-  iEnumInteger : Enum Integer
-  iEnumInteger .BoundedBelowEnum  = Nothing
-  iEnumInteger .BoundedAboveEnum  = Nothing
-  iEnumInteger .fromEnum          = integerToInt
-  iEnumInteger .toEnum          n = intToInteger n
-  iEnumInteger .succ              = _+ 1
-  iEnumInteger .pred              = _- 1
-  iEnumInteger .enumFromTo        = integerFromTo
-  iEnumInteger .enumFromThenTo    = integerFromThenTo
-
-private
-  fromTo : (from : a → Integer) (to : Integer → a)
-         → a → a → List a
-  fromTo from to a b = map to (enumFromTo (from a) (from b))
-
-  fromThenTo : (from : a → Integer) (to : Integer → a)
-             → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
-  fromThenTo from to a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))
-
-
-instance
-  iEnumNat : Enum Nat
-  iEnumNat .BoundedBelowEnum = Just it
-  iEnumNat .BoundedAboveEnum = Nothing
-  iEnumNat .fromEnum = integerToInt ∘ pos
-  iEnumNat .toEnum n = unsafeIntegerToNat (intToInteger n)
-  iEnumNat .succ n = suc n
-  iEnumNat .pred (suc n) = n
-  iEnumNat .enumFromTo = fromTo pos unsafeIntegerToNat
-  iEnumNat .enumFromThenTo = fromThenTo pos unsafeIntegerToNat
-
-  iEnumInt : Enum Int
-  iEnumInt .BoundedBelowEnum      = Just it
-  iEnumInt .BoundedAboveEnum      = Just it
-  iEnumInt .fromEnum              = integerToInt ∘ intToInteger
-  iEnumInt .toEnum         n      = integerToInt (intToInteger n)
-  iEnumInt .succ           x      = integerToInt (intToInteger x + 1)
-  iEnumInt .pred           x      = integerToInt (intToInteger x - 1)
-  iEnumInt .enumFromTo     a b    = fromTo intToInteger integerToInt a b
-  iEnumInt .enumFromThenTo a a₁ b = fromThenTo intToInteger integerToInt a a₁ b
-  iEnumInt .enumFrom       a      = fromTo intToInteger integerToInt a maxBound
-  iEnumInt .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo intToInteger integerToInt a a₁ maxBound
-              else fromThenTo intToInteger integerToInt a a₁ minBound
-
-  iEnumWord : Enum Word
-  iEnumWord .BoundedBelowEnum      = Just it
-  iEnumWord .BoundedAboveEnum      = Just it
-  iEnumWord .fromEnum              = integerToInt ∘ wordToInteger
-  iEnumWord .toEnum         n      = integerToWord (intToInteger n)
-  iEnumWord .succ           x      = integerToWord (wordToInteger x + 1)
-  iEnumWord .pred           x      = integerToWord (wordToInteger x - 1)
-  iEnumWord .enumFromTo     a b    = fromTo wordToInteger integerToWord a b
-  iEnumWord .enumFromThenTo a a₁ b = fromThenTo wordToInteger integerToWord a a₁ b
-  iEnumWord .enumFrom       a      = fromTo wordToInteger integerToWord a maxBound
-  iEnumWord .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo wordToInteger integerToWord a a₁ maxBound
-              else fromThenTo wordToInteger integerToWord a a₁ minBound
-
-private
-  fromBool : Bool → Integer
-  fromBool = if_then 1 else 0
-
-  toBool : Integer → Bool
-  toBool = _/= 0
-
-instance
-  iEnumBool : Enum Bool
-  iEnumBool .BoundedBelowEnum      = Just it
-  iEnumBool .BoundedAboveEnum      = Just it
-  iEnumBool .fromEnum              = integerToInt ∘ fromBool
-  iEnumBool .toEnum         n      = toBool (intToInteger n)
-  iEnumBool .succ           x      = toBool (fromBool x + 1)
-  iEnumBool .pred           x      = toBool (fromBool x - 1)
-  iEnumBool .enumFromTo     a b    = fromTo fromBool toBool a b
-  iEnumBool .enumFromThenTo a a₁ b = fromThenTo fromBool toBool a a₁ b
-  iEnumBool .enumFrom       a      = fromTo fromBool toBool a maxBound
-  iEnumBool .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo fromBool toBool a a₁ maxBound
-              else fromThenTo fromBool toBool a a₁ minBound
-
-private
-  fromOrdering : Ordering → Integer
-  fromOrdering = λ where LT → 0; EQ → 1; GT → 2
-
-  toOrdering : Integer → Ordering
-  toOrdering = λ where (pos 0) → LT; (pos 1) → EQ; _ → GT
-
-instance
-  iEnumOrdering : Enum Ordering
-  iEnumOrdering .BoundedBelowEnum      = Just it
-  iEnumOrdering .BoundedAboveEnum      = Just it
-  iEnumOrdering .fromEnum              = integerToInt ∘ fromOrdering
-  iEnumOrdering .toEnum         n      = toOrdering (intToInteger n)
-  iEnumOrdering .succ           x      = toOrdering (fromOrdering x + 1)
-  iEnumOrdering .pred           x      = toOrdering (fromOrdering x - 1)
-  iEnumOrdering .enumFromTo     a b    = fromTo fromOrdering toOrdering a b
-  iEnumOrdering .enumFromThenTo a a₁ b = fromThenTo fromOrdering toOrdering a a₁ b
-  iEnumOrdering .enumFrom       a      = fromTo fromOrdering toOrdering a maxBound
-  iEnumOrdering .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo fromOrdering toOrdering a a₁ maxBound
-              else fromThenTo fromOrdering toOrdering a a₁ minBound
-
-private
-  fromUnit : ⊤ → Integer
-  fromUnit _ = 0
-
-  toUnit : Integer → ⊤
-  toUnit _ = tt
-
-instance
-  iEnumUnit : Enum ⊤
-  iEnumUnit .BoundedBelowEnum      = Just it
-  iEnumUnit .BoundedAboveEnum      = Just it
-  iEnumUnit .fromEnum              = integerToInt ∘ fromUnit
-  iEnumUnit .toEnum         n      = toUnit (intToInteger n)
-  iEnumUnit .succ           x      = toUnit (fromUnit x + 1)
-  iEnumUnit .pred           x      = toUnit (fromUnit x - 1)
-  iEnumUnit .enumFromTo     a b    = fromTo fromUnit toUnit a b
-  iEnumUnit .enumFromThenTo a a₁ b = fromThenTo fromUnit toUnit a a₁ b
-  iEnumUnit .enumFrom       a      = fromTo fromUnit toUnit a maxBound
-  iEnumUnit .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo fromUnit toUnit a a₁ maxBound
-              else fromThenTo fromUnit toUnit a a₁ minBound
-
-private
-  fromChar : Char → Integer
-  fromChar = pos ∘ c2n
-
-  toChar : Integer → Char
-  toChar = λ where (pos n) → primNatToChar n; _ → '_'
-
-instance
-  iEnumChar : Enum Char
-  iEnumChar .BoundedBelowEnum      = Just it
-  iEnumChar .BoundedAboveEnum      = Just it
-  iEnumChar .fromEnum              = integerToInt ∘ fromChar
-  iEnumChar .toEnum         n      = toChar (intToInteger n)
-  iEnumChar .succ           x      = toChar (fromChar x + 1)
-  iEnumChar .pred           x      = toChar (fromChar x - 1)
-  iEnumChar .enumFromTo     a b    = fromTo fromChar toChar a b
-  iEnumChar .enumFromThenTo a a₁ b = fromThenTo fromChar toChar a a₁ b
-  iEnumChar .enumFrom       a      = fromTo fromChar toChar a maxBound
-  iEnumChar .enumFromThen   a a₁   =
-    if a < a₁ then fromThenTo fromChar toChar a a₁ maxBound
-              else fromThenTo fromChar toChar a a₁ minBound
-
-  -- Missing:
-  --  Enum Double  (can't go via Integer)
+module Instances where
+  private
+    divNat : Nat → Nat → Nat
+    divNat a 0       = 0
+    divNat a (suc b) = div-helper 0 b a b
+
+    diff : Integer → Integer → Maybe Nat
+    diff a b =
+      case a - b of λ where
+        (pos n)    → Just n
+        (negsuc _) → Nothing
+
+    unsafeIntegerToNat : Integer → Nat
+    unsafeIntegerToNat (pos n) = n
+    unsafeIntegerToNat (negsuc _) = 0
+
+    integerFromCount : Integer → Integer → Nat → List Integer
+    integerFromCount a step 0       = []
+    integerFromCount a step (suc n) = a ∷ integerFromCount (a + step) step n
+
+    integerFromTo : Integer → Integer → List Integer
+    integerFromTo a b = maybe [] (integerFromCount a 1 ∘ suc) (diff b a)
+
+    integerFromThenTo : (a a₁ : Integer) → @0 ⦃ IsFalse (integerToInt a == integerToInt a₁) ⦄ → Integer → List Integer
+    integerFromThenTo a a₁ b =
+      case compare a a₁ of λ where
+        LT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a₁ - a))))) (diff b a)
+        EQ → [] -- impossible
+        GT → maybe [] (λ d → integerFromCount a (a₁ - a) (suc (divNat d (unsafeIntegerToNat (a - a₁))))) (diff a b)
+
+  instance
+    iEnumInteger : Enum Integer
+    iEnumInteger .BoundedBelowEnum  = Nothing
+    iEnumInteger .BoundedAboveEnum  = Nothing
+    iEnumInteger .fromEnum          = integerToInt
+    iEnumInteger .toEnum          n = intToInteger n
+    iEnumInteger .succ              = _+ 1
+    iEnumInteger .pred              = _- 1
+    iEnumInteger .enumFromTo        = integerFromTo
+    iEnumInteger .enumFromThenTo    = integerFromThenTo
+
+  private
+    fromTo : (from : a → Integer) (to : Integer → a)
+          → a → a → List a
+    fromTo from to a b = map to (enumFromTo (from a) (from b))
+
+    fromThenTo : (from : a → Integer) (to : Integer → a)
+              → (x x₁ : a) → @0 ⦃ IsFalse (fromEnum (from x) == fromEnum (from x₁)) ⦄ → a → List a
+    fromThenTo from to a a₁ b = map to (enumFromThenTo (from a) (from a₁) (from b))
+
+
+  instance
+    iEnumNat : Enum Nat
+    iEnumNat .BoundedBelowEnum = Just it
+    iEnumNat .BoundedAboveEnum = Nothing
+    iEnumNat .fromEnum = integerToInt ∘ pos
+    iEnumNat .toEnum n = unsafeIntegerToNat (intToInteger n)
+    iEnumNat .succ n = suc n
+    iEnumNat .pred (suc n) = n
+    iEnumNat .enumFromTo = fromTo pos unsafeIntegerToNat
+    iEnumNat .enumFromThenTo = fromThenTo pos unsafeIntegerToNat
+
+    iEnumInt : Enum Int
+    iEnumInt .BoundedBelowEnum      = Just it
+    iEnumInt .BoundedAboveEnum      = Just it
+    iEnumInt .fromEnum              = integerToInt ∘ intToInteger
+    iEnumInt .toEnum         n      = integerToInt (intToInteger n)
+    iEnumInt .succ           x      = integerToInt (intToInteger x + 1)
+    iEnumInt .pred           x      = integerToInt (intToInteger x - 1)
+    iEnumInt .enumFromTo     a b    = fromTo intToInteger integerToInt a b
+    iEnumInt .enumFromThenTo a a₁ b = fromThenTo intToInteger integerToInt a a₁ b
+    iEnumInt .enumFrom       a      = fromTo intToInteger integerToInt a maxBound
+    iEnumInt .enumFromThen   a a₁   =
+      if a < a₁ then fromThenTo intToInteger integerToInt a a₁ maxBound
+                else fromThenTo intToInteger integerToInt a a₁ minBound
+
+    iEnumWord : Enum Word
+    iEnumWord .BoundedBelowEnum      = Just it
+    iEnumWord .BoundedAboveEnum      = Just it
+    iEnumWord .fromEnum              = integerToInt ∘ wordToInteger
+    iEnumWord .toEnum         n      = integerToWord (intToInteger n)
+    iEnumWord .succ           x      = integerToWord (wordToInteger x + 1)
+    iEnumWord .pred           x      = integerToWord (wordToInteger x - 1)
+    iEnumWord .enumFromTo     a b    = fromTo wordToInteger integerToWord a b
+    iEnumWord .enumFromThenTo a a₁ b = fromThenTo wordToInteger integerToWord a a₁ b
+    iEnumWord .enumFrom       a      = fromTo wordToInteger integerToWord a maxBound
+    iEnumWord .enumFromThen   a a₁   =
+      if a < a₁ then fromThenTo wordToInteger integerToWord a a₁ maxBound
+                else fromThenTo wordToInteger integerToWord a a₁ minBound
+
+  private
+    fromBool : Bool → Integer
+    fromBool = if_then 1 else 0
+
+    toBool : Integer → Bool
+    toBool = _/= 0
+
+  instance
+    iEnumBool : Enum Bool
+    iEnumBool .BoundedBelowEnum      = Just it
+    iEnumBool .BoundedAboveEnum      = Just it
+    iEnumBool .fromEnum              = integerToInt ∘ fromBool
+    iEnumBool .toEnum         n      = toBool (intToInteger n)
+    iEnumBool .succ           x      = toBool (fromBool x + 1)
+    iEnumBool .pred           x      = toBool (fromBool x - 1)
+    iEnumBool .enumFromTo     a b    = fromTo fromBool toBool a b
+    iEnumBool .enumFromThenTo a a₁ b = fromThenTo fromBool toBool a a₁ b
+    iEnumBool .enumFrom       a      = fromTo fromBool toBool a maxBound
+    iEnumBool .enumFromThen   a a₁   =
+      if a < a₁ then fromThenTo fromBool toBool a a₁ maxBound
+                else fromThenTo fromBool toBool a a₁ minBound
+
+  private
+    fromOrdering : Ordering → Integer
+    fromOrdering = λ where LT → 0; EQ → 1; GT → 2
+
+    toOrdering : Integer → Ordering
+    toOrdering = λ where (pos 0) → LT; (pos 1) → EQ; _ → GT
+
+  instance
+    iEnumOrdering : Enum Ordering
+    iEnumOrdering .BoundedBelowEnum      = Just it
+    iEnumOrdering .BoundedAboveEnum      = Just it
+    iEnumOrdering .fromEnum              = integerToInt ∘ fromOrdering
+    iEnumOrdering .toEnum         n      = toOrdering (intToInteger n)
+    iEnumOrdering .succ           x      = toOrdering (fromOrdering x + 1)
+    iEnumOrdering .pred           x      = toOrdering (fromOrdering x - 1)
+    iEnumOrdering .enumFromTo     a b    = fromTo fromOrdering toOrdering a b
+    iEnumOrdering .enumFromThenTo a a₁ b = fromThenTo fromOrdering toOrdering a a₁ b
+    iEnumOrdering .enumFrom       a      = fromTo fromOrdering toOrdering a maxBound
+    iEnumOrdering .enumFromThen   a a₁   =
+      if a < a₁ then fromThenTo fromOrdering toOrdering a a₁ maxBound
+                else fromThenTo fromOrdering toOrdering a a₁ minBound
+
+  private
+    fromUnit : ⊤ → Integer
+    fromUnit _ = 0
+
+    toUnit : Integer → ⊤
+    toUnit _ = tt
+
+  instance
+    iEnumUnit : Enum ⊤
+    iEnumUnit .BoundedBelowEnum      = Just it
+    iEnumUnit .BoundedAboveEnum      = Just it
+    iEnumUnit .fromEnum              = integerToInt ∘ fromUnit
+    iEnumUnit .toEnum         n      = toUnit (intToInteger n)
+    iEnumUnit .succ           x      = toUnit (fromUnit x + 1)
+    iEnumUnit .pred           x      = toUnit (fromUnit x - 1)
+    iEnumUnit .enumFromTo     a b    = fromTo fromUnit toUnit a b
+    iEnumUnit .enumFromThenTo a a₁ b = fromThenTo fromUnit toUnit a a₁ b
+    iEnumUnit .enumFrom       a      = fromTo fromUnit toUnit a maxBound
+    iEnumUnit .enumFromThen   a a₁   =
+      if a < a₁ then fromThenTo fromUnit toUnit a a₁ maxBound
+                else fromThenTo fromUnit toUnit a a₁ minBound
+
+  private
+    fromChar : Char → Integer
+    fromChar = pos ∘ c2n
+
+    toChar : Integer → Char
+    toChar = λ where (pos n) → primNatToChar n; _ → '_'
+
+  instance
+    iEnumChar : Enum Char
+    iEnumChar .BoundedBelowEnum      = Just it
+    iEnumChar .BoundedAboveEnum      = Just it
+    iEnumChar .fromEnum              = integerToInt ∘ fromChar
+    iEnumChar .toEnum         n      = toChar (intToInteger n)
+    iEnumChar .succ           x      = toChar (fromChar x + 1)
+    iEnumChar .pred           x      = toChar (fromChar x - 1)
+    iEnumChar .enumFromTo     a b    = fromTo fromChar toChar a b
+    iEnumChar .enumFromThenTo a a₁ b = fromThenTo fromChar toChar a a₁ b
+    iEnumChar .enumFrom       a      = fromTo fromChar toChar a maxBound
+    iEnumChar .enumFromThen   a a₁   =
+      if a < a₁ then fromThenTo fromChar toChar a a₁ maxBound
+                else fromThenTo fromChar toChar a a₁ minBound
+
+    -- Missing:
+    --  Enum Double  (can't go via Integer)
+open Instances public
diff --git a/lib/base/Haskell/Prim/Eq.agda b/lib/base/Haskell/Prim/Eq.agda
index 4f844c75..54e61d50 100644
--- a/lib/base/Haskell/Prim/Eq.agda
+++ b/lib/base/Haskell/Prim/Eq.agda
@@ -12,7 +12,8 @@ open import Haskell.Prim.Tuple
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Either
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Eq
 
 record Eq (a : Type) : Type where
@@ -29,54 +30,56 @@ x /= y = not (x == y)
 
 infix 4 _/=_
 
-instance
-  iEqNat : Eq Nat
-  iEqNat ._==_ = eqNat
+module Instances where
+  instance
+    iEqNat : Eq Nat
+    iEqNat ._==_ = eqNat
 
-  iEqInteger : Eq Integer
-  iEqInteger ._==_ = eqInteger
+    iEqInteger : Eq Integer
+    iEqInteger ._==_ = eqInteger
 
-  iEqInt : Eq Int
-  iEqInt ._==_ = eqInt
+    iEqInt : Eq Int
+    iEqInt ._==_ = eqInt
 
-  iEqWord : Eq Word
-  iEqWord ._==_ = eqWord
+    iEqWord : Eq Word
+    iEqWord ._==_ = eqWord
 
-  iEqDouble : Eq Double
-  iEqDouble ._==_ = primFloatEquality
+    iEqDouble : Eq Double
+    iEqDouble ._==_ = primFloatEquality
 
-  iEqBool : Eq Bool
-  iEqBool ._==_ False False = True
-  iEqBool ._==_ True  True  = True
-  iEqBool ._==_ _     _     = False
+    iEqBool : Eq Bool
+    iEqBool ._==_ False False = True
+    iEqBool ._==_ True  True  = True
+    iEqBool ._==_ _     _     = False
 
-  iEqChar : Eq Char
-  iEqChar ._==_ = eqChar
+    iEqChar : Eq Char
+    iEqChar ._==_ = eqChar
 
-  iEqUnit : Eq ⊤
-  iEqUnit ._==_ _ _ = True
+    iEqUnit : Eq ⊤
+    iEqUnit ._==_ _ _ = True
 
-  iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
-  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂
+    iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
+    iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂
 
-  iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
-  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂
+    iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
+    iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂
 
-  iEqList : ⦃ Eq a ⦄ → Eq (List a)
-  iEqList {a} ._==_ = eqList
-    where
-      eqList : List a → List a → Bool
-      eqList [] [] = True
-      eqList (x ∷ xs) (y ∷ ys) = x == y && eqList xs ys
-      eqList _ _ = False
+    iEqList : ⦃ Eq a ⦄ → Eq (List a)
+    iEqList {a} ._==_ = eqList
+      where
+        eqList : List a → List a → Bool
+        eqList [] [] = True
+        eqList (x ∷ xs) (y ∷ ys) = x == y && eqList xs ys
+        eqList _ _ = False
 
 
-  iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a)
-  iEqMaybe ._==_ Nothing  Nothing  = True
-  iEqMaybe ._==_ (Just x) (Just y) = x == y
-  iEqMaybe ._==_ _        _        = False
+    iEqMaybe : ⦃ Eq a ⦄ → Eq (Maybe a)
+    iEqMaybe ._==_ Nothing  Nothing  = True
+    iEqMaybe ._==_ (Just x) (Just y) = x == y
+    iEqMaybe ._==_ _        _        = False
 
-  iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b)
-  iEqEither ._==_ (Left  x) (Left  y) = x == y
-  iEqEither ._==_ (Right x) (Right y) = x == y
-  iEqEither ._==_ _        _          = False
+    iEqEither : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (Either a b)
+    iEqEither ._==_ (Left  x) (Left  y) = x == y
+    iEqEither ._==_ (Right x) (Right y) = x == y
+    iEqEither ._==_ _        _          = False
+open Instances public
diff --git a/lib/base/Haskell/Prim/Foldable.agda b/lib/base/Haskell/Prim/Foldable.agda
index 3de5cc27..b91f9474 100644
--- a/lib/base/Haskell/Prim/Foldable.agda
+++ b/lib/base/Haskell/Prim/Foldable.agda
@@ -1,122 +1,151 @@
-
 module Haskell.Prim.Foldable where
 
 open import Haskell.Prim
-open import Haskell.Prim.Num hiding (abs)
+open import Haskell.Prim.Num
+  hiding (abs) renaming (module Instances to NumInstances)
 open import Haskell.Prim.Eq
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord
+  renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
+open import Haskell.Prim.Monoid
+  renaming (module Instances to MonoidInstances)
 open import Haskell.Prim.List
 open import Haskell.Prim.Int
 open import Haskell.Prim.Bool
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Either
 open import Haskell.Prim.Tuple
-open import Haskell.Prim.Monoid
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Foldable
 
 -- ** base
 record Foldable (t : Type → Type) : Type₁ where
   field
-    foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
-    foldr : (a → b → b) → b → t a → b
-    foldl : (b → a → b) → b → t a → b
-    any : (a → Bool) → t a → Bool
-    all : (a → Bool) → t a → Bool
-    and : t Bool → Bool
-    null : t a → Bool
-    or : t Bool → Bool
-    concat : t (List a) → List a
-    concatMap : (a → List b) → t a → List b
-    elem : ⦃ Eq a ⦄ → a → t a → Bool
-    notElem : ⦃ Eq a ⦄ → a → t a → Bool
-    toList : t a → List a
-    sum : ⦃ iNum : Num a ⦄ → t a → a
-    product : ⦃ iNum : Num a ⦄ → t a → a
-    length : t a → Int
+    fold     : ⦃ Monoid b ⦄ → t b → b
+    foldMap  : ⦃ Monoid b ⦄ → (a → b) → t a → b
+    foldMap' : ⦃ Monoid b ⦄ → (a → b) → t a → b
+    foldr    : (a → b → b) → b → t a → b
+    foldr'   : (a → b → b) → b → t a → b
+    foldl    : (b → a → b) → b → t a → b
+    foldl'   : (b → a → b) → b → t a → b
+    toList   : t a → List a
+    foldr1   : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+    foldl1   : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+    null     : t a → Bool
+    length   : t a → Int
+    elem     : ⦃ Eq a ⦄ → a → t a → Bool
+    maximum  : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+    minimum  : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+    sum      : ⦃ Num a ⦄ → t a → a
+    product  : ⦃ Num a ⦄ → t a → a
+
 -- ** defaults
 record DefaultFoldable (t : Type → Type) : Type₁ where
-  module M = Foldable {t = t}
   field foldMap : ⦃ Monoid b ⦄ → (a → b) → t a → b
 
+  fold : ⦃ Monoid b ⦄ → t b → b
+  fold = foldMap id
+
   foldr : (a → b → b) → b → t a → b
   foldr f z t = foldMap ⦃ MonoidEndo ⦄ f t z
 
+  foldr' : (a → b → b) → b → t a → b
+  foldr' = foldr
+
   foldl : (b → a → b) → b → t a → b
   foldl f z t = foldMap ⦃ MonoidEndoᵒᵖ ⦄ (flip f) t z
 
-  any : (a → Bool) → t a → Bool
-  any = foldMap ⦃ MonoidDisj ⦄
+  foldl' : (b → a → b) → b → t a → b
+  foldl' = foldl
 
-  all : (a → Bool) → t a → Bool
-  all = foldMap ⦃ MonoidConj ⦄
+  foldMap' : ⦃ Monoid b ⦄ → (a → b) → t a → b
+  foldMap' f = foldl' (λ acc a → acc <> f a) mempty
 
-  and : t Bool → Bool
-  and = all id
+  toList : t a → List a
+  toList = foldr _∷_ []
 
-  or : t Bool → Bool
-  or = any id
+  foldr1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+  foldr1 f s = let l = toList s
+                   xs , x = init l , last l
+               in foldrList f x xs
+    where
+      foldrList : (a → b → b) → b → List a → b
+      foldrList f z = λ where
+        []       → z
+        (x ∷ xs) → f x (foldrList f z xs)
+
+  foldl1 : (a → a → a) → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+  foldl1 f s with toList s
+  ...           | x ∷ xs = foldlList f x xs
+    where
+      foldlList : (b → a → b) → b → List a → b
+      foldlList f z = λ where
+        []       → z
+        (x ∷ xs) → foldlList f (f z x) xs
 
   null : t a → Bool
-  null = all (const False)
-
-  concat : t (List a) → List a
-  concat = foldMap id
+  null = foldMap ⦃ MonoidConj ⦄ (const False)
 
-  concatMap : (a → List b) → t a → List b
-  concatMap = foldMap
+  length : t a → Int
+  length = foldMap ⦃ MonoidSum ⦄ (const 1)
 
   elem : ⦃ Eq a ⦄ → a → t a → Bool
   elem x = foldMap ⦃ MonoidDisj ⦄ (x ==_)
 
-  notElem : ⦃ Eq a ⦄ → a → t a → Bool
-  notElem x t = not (elem x t)
+  maximum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+  maximum = foldr1 max
 
-  toList : t a → List a
-  toList = foldr _∷_ []
+  minimum : ⦃ Ord a ⦄ → (s : t a) → @0 ⦃ NonEmpty (toList s) ⦄ → a
+  minimum = foldr1 min
 
-  sum : ⦃ iNum : Num a ⦄ → t a → a
-  sum = foldMap ⦃ MonoidSum ⦄ id
+  sum : ⦃ Num a ⦄ → t a → a
+  sum = fold ⦃ MonoidSum ⦄
 
-  product : ⦃ iNum : Num a ⦄ → t a → a
-  product = foldMap ⦃ MonoidProduct ⦄ id
+  product : ⦃ Num a ⦄ → t a → a
+  product = fold ⦃ MonoidProduct ⦄
 
-  length : t a → Int
-  length = foldMap ⦃ MonoidSum ⦄ (const 1)
 -- ** export
 open Foldable ⦃...⦄ public
 {-# COMPILE AGDA2HS Foldable existing-class #-}
 
 -- ** instances
-instance
-  iDefaultFoldableList : DefaultFoldable List
-  iDefaultFoldableList .DefaultFoldable.foldMap = foldMapList
-    where
-      foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b
-      foldMapList f []       = mempty
-      foldMapList f (x ∷ xs) = f x <> foldMapList f xs
-
-  iFoldableList : Foldable List
-  iFoldableList = record {DefaultFoldable iDefaultFoldableList}
-
-  iDefaultFoldableMaybe : DefaultFoldable Maybe
-  iDefaultFoldableMaybe .DefaultFoldable.foldMap = λ where
-    _ Nothing  → mempty
-    f (Just x) → f x
-
-  iFoldableMaybe : Foldable Maybe
-  iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe}
-
-  iDefaultFoldableEither : DefaultFoldable (Either a)
-  iDefaultFoldableEither .DefaultFoldable.foldMap = λ where
-    _ (Left _)  → mempty
-    f (Right x) → f x
-
-  iFoldableEither : Foldable (Either a)
-  iFoldableEither = record {DefaultFoldable iDefaultFoldableEither}
-
-  iDefaultFoldablePair : DefaultFoldable (a ×_)
-  iDefaultFoldablePair .DefaultFoldable.foldMap = λ f (_ , x) → f x
-
-  iFoldablePair : Foldable (a ×_)
-  iFoldablePair = record {DefaultFoldable iDefaultFoldablePair}
+module Instances where
+  instance
+    open DefaultFoldable
+
+    iDefaultFoldableList : DefaultFoldable List
+    iDefaultFoldableList .foldMap = foldMapList
+      where
+        foldMapList : ⦃ Monoid b ⦄ → (a → b) → List a → b
+        foldMapList f []       = mempty
+        foldMapList f (x ∷ xs) = f x <> foldMapList f xs
+
+    iFoldableList : Foldable List
+    iFoldableList = record {DefaultFoldable iDefaultFoldableList}
+
+    iDefaultFoldableMaybe : DefaultFoldable Maybe
+    iDefaultFoldableMaybe .foldMap = λ where
+      _ Nothing  → mempty
+      f (Just x) → f x
+
+    iFoldableMaybe : Foldable Maybe
+    iFoldableMaybe = record {DefaultFoldable iDefaultFoldableMaybe}
+
+    iDefaultFoldableEither : DefaultFoldable (Either a)
+    iDefaultFoldableEither .foldMap = λ where
+      _ (Left _)  → mempty
+      f (Right x) → f x
+
+    iFoldableEither : Foldable (Either a)
+    iFoldableEither = record {DefaultFoldable iDefaultFoldableEither}
+
+    iDefaultFoldablePair : DefaultFoldable (a ×_)
+    iDefaultFoldablePair .foldMap = λ f (_ , x) → f x
+
+    iFoldablePair : Foldable (a ×_)
+    iFoldablePair = record {DefaultFoldable iDefaultFoldablePair}
+open Instances public
diff --git a/lib/base/Haskell/Prim/Functor.agda b/lib/base/Haskell/Prim/Functor.agda
index c0847503..4df971d2 100644
--- a/lib/base/Haskell/Prim/Functor.agda
+++ b/lib/base/Haskell/Prim/Functor.agda
@@ -8,7 +8,8 @@ open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Tuple
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Functor
 
 -- ** base
@@ -17,12 +18,12 @@ record Functor (f : Type → Type) : Type₁ where
   field
     fmap : (a → b) → f a → f b
     _<$_ : (@0 {{ b }} → a) → f b → f a
+
 -- ** defaults
 record DefaultFunctor (f : Type → Type) : Type₁ where
   field fmap : (a → b) → f a → f b
 
   infixl 4 _<$_
-
   _<$_ : (@0 {{ b }} → a) → f b → f a
   x <$ m = fmap (λ b → x {{b}}) m
 
@@ -30,60 +31,54 @@ record DefaultFunctor (f : Type → Type) : Type₁ where
 open Functor ⦃...⦄ public
 {-# COMPILE AGDA2HS Functor existing-class #-}
 
-_<$>_ : {{Functor f}} → (a → b) → f a → f b
-_<$>_ = fmap
-
-_<&>_ : {{Functor f}} → f a → (a → b) → f b
-m <&> f = fmap f m
-
-_$>_ : {{Functor f}} → f a → (@0 {{ a }} → b) → f b
-m $> x = x <$ m
-
-void : {{Functor f}} → f a → f ⊤
-void = tt <$_
+-- ** instances
+module Instances where
+  instance
+    open DefaultFunctor
 
-infixl 1 _<&>_
-infixl 4 _<$>_ _$>_
+    iDefaultFunctorList : DefaultFunctor List
+    iDefaultFunctorList .fmap = map
 
-instance
-  iDefaultFunctorList : DefaultFunctor List
-  iDefaultFunctorList .DefaultFunctor.fmap = map
+    iFunctorList : Functor List
+    iFunctorList = record{DefaultFunctor iDefaultFunctorList}
 
-  iFunctorList : Functor List
-  iFunctorList = record{DefaultFunctor iDefaultFunctorList}
+    iDefaultFunctorMaybe : DefaultFunctor Maybe
+    iDefaultFunctorMaybe .fmap = λ where
+      f Nothing  → Nothing
+      f (Just x) → Just (f x)
 
-  iDefaultFunctorMaybe : DefaultFunctor Maybe
-  iDefaultFunctorMaybe .DefaultFunctor.fmap = λ where
-    f Nothing  → Nothing
-    f (Just x) → Just (f x)
+    iFunctorMaybe : Functor Maybe
+    iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe}
 
-  iFunctorMaybe : Functor Maybe
-  iFunctorMaybe = record{DefaultFunctor iDefaultFunctorMaybe}
+    iDefaultFunctorEither : DefaultFunctor (Either a)
+    iDefaultFunctorEither .fmap = λ where
+      f (Left  x) → Left x
+      f (Right y) → Right (f y)
 
-  iDefaultFunctorEither : DefaultFunctor (Either a)
-  iDefaultFunctorEither .DefaultFunctor.fmap = λ where
-    f (Left  x) → Left x
-    f (Right y) → Right (f y)
+    iFunctorEither : Functor (Either a)
+    iFunctorEither = record{DefaultFunctor iDefaultFunctorEither}
 
-  iFunctorEither : Functor (Either a)
-  iFunctorEither = record{DefaultFunctor iDefaultFunctorEither}
+    iDefaultFunctorFun : DefaultFunctor (λ b → a → b)
+    iDefaultFunctorFun .fmap = _∘_
 
-  iDefaultFunctorFun : DefaultFunctor (λ b → a → b)
-  iDefaultFunctorFun .DefaultFunctor.fmap = _∘_
+    iFunctorFun : Functor (λ b → a → b)
+    iFunctorFun = record{DefaultFunctor iDefaultFunctorFun}
 
-  iFunctorFun : Functor (λ b → a → b)
-  iFunctorFun = record{DefaultFunctor iDefaultFunctorFun}
+    iDefaultFunctorTuple₂ : DefaultFunctor (a ×_)
+    iDefaultFunctorTuple₂ .fmap = λ f (x , y) → x , f y
 
-  iDefaultFunctorTuple₂ : DefaultFunctor (a ×_)
-  iDefaultFunctorTuple₂ .DefaultFunctor.fmap = λ f (x , y) → x , f y
+    iFunctorTuple₂ : Functor (a ×_)
+    iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂}
 
-  iFunctorTuple₂ : Functor (a ×_)
-  iFunctorTuple₂ = record{DefaultFunctor iDefaultFunctorTuple₂}
+    iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_)
+    iDefaultFunctorTuple₃ .fmap = λ where f (x , y , z) → x , y , f z
 
-  iDefaultFunctorTuple₃ : DefaultFunctor (a × b ×_)
-  iDefaultFunctorTuple₃ .DefaultFunctor.fmap = λ where f (x , y , z) → x , y , f z
+    iFunctorTuple₃ : Functor (a × b ×_)
+    iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃}
 
-  iFunctorTuple₃ : Functor (a × b ×_)
-  iFunctorTuple₃ = record{DefaultFunctor iDefaultFunctorTuple₃}
+    iDefaultFunctorIO : DefaultFunctor IO
+    iDefaultFunctorIO .fmap = λ f x → bindIO x (returnIO ∘ f)
 
-instance postulate iFunctorIO : Functor IO
+    iFunctorIO : Functor IO
+    iFunctorIO = record{DefaultFunctor iDefaultFunctorIO}
+open Instances public
diff --git a/lib/base/Haskell/Prim/IO.agda b/lib/base/Haskell/Prim/IO.agda
index b653e3c4..31b88ccc 100644
--- a/lib/base/Haskell/Prim/IO.agda
+++ b/lib/base/Haskell/Prim/IO.agda
@@ -4,6 +4,7 @@ open import Haskell.Prim
 open import Haskell.Prim.Show
 open import Haskell.Prim.String
 
+
 postulate IO : ∀{a} → Type a → Type a
 
 FilePath = String
@@ -25,3 +26,9 @@ postulate
   readFile       : FilePath → IO String
   writeFile      : FilePath → String → IO ⊤
   appendFile     : FilePath → String → IO ⊤
+
+  -- For instance definitions
+  returnIO       : a → IO a
+  bindIO         : IO a → (a → IO b) → IO b
+  failIO         : String → IO a
+  mplusIO        : IO a → IO a → IO a
diff --git a/lib/base/Haskell/Prim/List.agda b/lib/base/Haskell/Prim/List.agda
index 8343eb61..87d2cc5b 100644
--- a/lib/base/Haskell/Prim/List.agda
+++ b/lib/base/Haskell/Prim/List.agda
@@ -2,127 +2,33 @@
 module Haskell.Prim.List where
 
 open import Haskell.Prim
-open import Haskell.Prim.Bool
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Int
-
 
 --------------------------------------------------
 -- List
 
-map : (a → b) → List a → List b
-map f []       = []
-map f (x ∷ xs) = f x ∷ map f xs
-
 infixr 5 _++_
 _++_ : ∀ {@0 ℓ} {@0 a : Type ℓ} → List a → List a → List a
 []       ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ xs ++ ys
 
-filter : (a → Bool) → List a → List a
-filter p []       = []
-filter p (x ∷ xs) = if p x then x ∷ filter p xs else filter p xs
-
-scanl : (b → a → b) → b → List a → List b
-scanl f z []       = z ∷ []
-scanl f z (x ∷ xs) = z ∷ scanl f (f z x) xs
-
-scanr : (a → b → b) → b → List a → List b
-scanr f z [] = z ∷ []
-scanr f z (x ∷ xs) =
-  case scanr f z xs of λ where
-    []         → [] -- impossible
-    qs@(q ∷ _) → f x q ∷ qs
-
-scanl1 : (a → a → a) → List a → List a
-scanl1 f []       = []
-scanl1 f (x ∷ xs) = scanl f x xs
-
-scanr1 : (a → a → a) → List a → List a
-scanr1 f []       = []
-scanr1 f (x ∷ []) = x ∷ []
-scanr1 f (x ∷ xs) =
-  case scanr1 f xs of λ where
-    []         → [] -- impossible
-    qs@(q ∷ _) → f x q ∷ qs
-
-takeWhile : (a → Bool) → List a → List a
-takeWhile p [] = []
-takeWhile p (x ∷ xs) = if p x then x ∷ takeWhile p xs else []
-
-dropWhile : (a → Bool) → List a → List a
-dropWhile p [] = []
-dropWhile p (x ∷ xs) = if p x then dropWhile p xs else x ∷ xs
-
-span : (a → Bool) → List a → List a × List a
-span p [] = [] , []
-span p (x ∷ xs) = if p x then first (x ∷_) (span p xs)
-                         else ([] , x ∷ xs)
-
-break : (a → Bool) → List a → List a × List a
-break p = span (not ∘ p)
-
-zipWith : (a → b → c) → List a → List b → List c
-zipWith f []       _        = []
-zipWith f _        []       = []
-zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
-
-zip : List a → List b → List (a × b)
-zip = zipWith _,_
-
-zipWith3 : (a → b → c → d) → List a → List b → List c → List d
-zipWith3 f []       _        _        = []
-zipWith3 f _        []       _        = []
-zipWith3 f _        _        []       = []
-zipWith3 f (x ∷ xs) (y ∷ ys) (z ∷ zs) = f x y z ∷ zipWith3 f xs ys zs
-
-zip3 : List a → List b → List c → List (a × b × c)
-zip3 = zipWith3 _,_,_
-
-unzip : List (a × b) → List a × List b
-unzip []              = [] , []
-unzip ((x , y) ∷ xys) = (x ∷_) *** (y ∷_) $ unzip xys
-
-unzip3 : List (a × b × c) → List a × List b × List c
-unzip3 []                   = [] , [] , []
-unzip3 ((x , y , z) ∷ xyzs) =
-  case unzip3 xyzs of λ where
-    (xs , ys , zs) → x ∷ xs , y ∷ ys , z ∷ zs
-
-takeNat : Nat → List a → List a
-takeNat n       [] = []
-takeNat zero    xs = []
-takeNat (suc n) (x ∷ xs) = x ∷ takeNat n xs
-
-take : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
-take n xs = takeNat (intToNat n) xs
-
-dropNat : Nat → List a → List a
-dropNat n       [] = []
-dropNat zero    xs = xs
-dropNat (suc n) (_ ∷ xs) = dropNat n xs
-
-drop : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a
-drop n xs = dropNat (intToNat n) xs
-
-splitAtNat : (n : Nat) → List a → List a × List a
-splitAtNat _       []       = [] , []
-splitAtNat 0       xs       = [] , xs
-splitAtNat (suc n) (x ∷ xs) = first (x ∷_) (splitAtNat n xs)
-
-splitAt : (n : Int) → @0 ⦃ IsNonNegativeInt n ⦄ → List a → List a × List a
-splitAt n xs = splitAtNat (intToNat n) xs
-
 head : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
 head (x ∷ _) = x
 
-tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
-tail (_ ∷ xs) = xs
-
 last : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → a
 last (x ∷ [])         = x
 last (_ ∷ xs@(_ ∷ _)) = last xs
 
+tail : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
+tail (_ ∷ xs) = xs
+
 init : (xs : List a) → @0 ⦃ NonEmpty xs ⦄ → List a
 init (x ∷ [])         = []
 init (x ∷ xs@(_ ∷ _)) = x ∷ init xs
+
+map : (a → b) → List a → List b
+map f []       = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+lengthNat : List a → Nat
+lengthNat []       = 0
+lengthNat (_ ∷ xs) = addNat 1 (lengthNat xs)
diff --git a/lib/base/Haskell/Prim/Monad.agda b/lib/base/Haskell/Prim/Monad.agda
index bff504d7..88357014 100644
--- a/lib/base/Haskell/Prim/Monad.agda
+++ b/lib/base/Haskell/Prim/Monad.agda
@@ -1,19 +1,24 @@
-
 module Haskell.Prim.Monad where
 
 open import Haskell.Prim
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
+open import Haskell.Prim.Monoid
+  renaming (module Instances to MonoidInstances)
+open import Haskell.Prim.Functor
+  renaming (module Instances to FunctorInstances)
 open import Haskell.Prim.Applicative
-open import Haskell.Prim.Either
+  renaming (module Instances to ApplicativeInstances)
 open import Haskell.Prim.Foldable
-open import Haskell.Prim.Functor
+  renaming (module Instances to FoldableInstances)
+open import Haskell.Prim.Either
 open import Haskell.Prim.IO
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
-open import Haskell.Prim.Monoid
-open import Haskell.Prim.String
 open import Haskell.Prim.Tuple
 
--------------------------------------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Monad
 
 module Do where
@@ -25,6 +30,7 @@ module Do where
       overlap ⦃ super ⦄ : Applicative m
       return : a → m a
       _>>_ : m a → (@0 {{ a }} → m b) → m b
+
   -- ** defaults
   record DefaultMonad (m : Type → Type) : Type₁ where
     field
@@ -54,84 +60,52 @@ module Dont where
 
 open Do public
 
-_=<<_ : {{Monad m}} → (a → m b) → m a → m b
-_=<<_ = flip _>>=_
-
-mapM₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → (a → m b) → t a → m ⊤
-mapM₋ f = foldr (λ x k → f x >> k) (pure tt)
-
-sequence₋ : ⦃ Monad m ⦄ → ⦃ Foldable t ⦄ → t (m a) → m ⊤
-sequence₋ = foldr (λ mx my → mx >> my) (pure tt)
-
 -- ** instances
-instance
-  iDefaultMonadList : DefaultMonad List
-  iDefaultMonadList .DefaultMonad._>>=_ = flip concatMap
-
-  iMonadList : Monad List
-  iMonadList = record {DefaultMonad iDefaultMonadList}
-
-  iDefaultMonadMaybe : DefaultMonad Maybe
-  iDefaultMonadMaybe .DefaultMonad._>>=_ = flip (maybe Nothing)
-
-  iMonadMaybe : Monad Maybe
-  iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe}
-
-  iDefaultMonadEither : DefaultMonad (Either a)
-  iDefaultMonadEither .DefaultMonad._>>=_ = flip (either Left)
-
-  iMonadEither : Monad (Either a)
-  iMonadEither = record {DefaultMonad iDefaultMonadEither}
-
-  iDefaultMonadFun : DefaultMonad (λ b → a → b)
-  iDefaultMonadFun .DefaultMonad._>>=_ = λ f k r → k (f r) r
+module Instances where
+  instance
+    open DefaultMonad
 
-  iMonadFun : Monad (λ b → a → b)
-  iMonadFun = record {DefaultMonad iDefaultMonadFun}
+    iDefaultMonadList : DefaultMonad List
+    iDefaultMonadList ._>>=_ = flip foldMap
 
-  iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_)
-  iDefaultMonadTuple₂ .DefaultMonad._>>=_ = λ (a , x) k → first (a <>_) (k x)
+    iMonadList : Monad List
+    iMonadList = record {DefaultMonad iDefaultMonadList}
 
-  iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_)
-  iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂}
+    iDefaultMonadMaybe : DefaultMonad Maybe
+    iDefaultMonadMaybe ._>>=_ = flip (maybe Nothing)
 
-  iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_)
-  iDefaultMonadTuple₃ .DefaultMonad._>>=_ = λ where
-    (a , b , x) k → case k x of λ where
-      (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y
+    iMonadMaybe : Monad Maybe
+    iMonadMaybe = record {DefaultMonad iDefaultMonadMaybe}
 
-  iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
-  iMonadTuple₃ = record {DefaultMonad iDefaultMonadTuple₃}
+    iDefaultMonadEither : DefaultMonad (Either a)
+    iDefaultMonadEither ._>>=_ = flip (either Left)
 
--- For 'Monad IO', we only postulate the '_>>=_' operation,
--- and construct the instance via 'DefaultMonad' as usual.
--- This is necessary to ensure that the existing 'Applicative IO'
--- instance is picked for the 'super' instance field.
-postulate
-  bindIO : IO a → (a → IO b) → IO b
+    iMonadEither : Monad (Either a)
+    iMonadEither = record {DefaultMonad iDefaultMonadEither}
 
-instance
-  iDefaultMonadIO : DefaultMonad IO
-  iDefaultMonadIO .DefaultMonad._>>=_ = bindIO
+    iDefaultMonadFun : DefaultMonad (λ b → a → b)
+    iDefaultMonadFun ._>>=_ = λ f k r → k (f r) r
 
-  iMonadIO : Monad IO
-  iMonadIO = record {DefaultMonad iDefaultMonadIO}
+    iMonadFun : Monad (λ b → a → b)
+    iMonadFun = record {DefaultMonad iDefaultMonadFun}
 
--------------------------------------------------------------------------------
--- MonadFail class
+    iDefaultMonadTuple₂ : ⦃ Monoid a ⦄ → DefaultMonad (a ×_)
+    iDefaultMonadTuple₂ ._>>=_ = λ (a , x) k → first (a <>_) (k x)
 
-record MonadFail (m : Type → Type) : Type₁ where
-  field
-    fail : String → m a
-    overlap ⦃ super ⦄ : Monad m
+    iMonadTuple₂ : ⦃ Monoid a ⦄ → Monad (a ×_)
+    iMonadTuple₂ = record {DefaultMonad iDefaultMonadTuple₂}
 
-open MonadFail ⦃...⦄ public
+    iDefaultMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonad (a × b ×_)
+    iDefaultMonadTuple₃ ._>>=_ = λ where
+      (a , b , x) k → case k x of λ where
+        (a₁ , b₁ , y) → a <> a₁ , b <> b₁ , y
 
-{-# COMPILE AGDA2HS MonadFail existing-class #-}
+    iMonadTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monad (a × b ×_)
+    iMonadTuple₃ = record {DefaultMonad iDefaultMonadTuple₃}
 
-instance
-  MonadFailList : MonadFail List
-  MonadFailList .fail _ = []
+    iDefaultMonadIO : DefaultMonad IO
+    iDefaultMonadIO ._>>=_ = bindIO
 
-  MonadFailMaybe : MonadFail Maybe
-  MonadFailMaybe .fail _ = Nothing
+    iMonadIO : Monad IO
+    iMonadIO = record {DefaultMonad iDefaultMonadIO}
+open Instances public
diff --git a/lib/base/Haskell/Prim/MonadFail.agda b/lib/base/Haskell/Prim/MonadFail.agda
new file mode 100644
index 00000000..293ab9a4
--- /dev/null
+++ b/lib/base/Haskell/Prim/MonadFail.agda
@@ -0,0 +1,32 @@
+module Haskell.Prim.MonadFail where
+
+open import Haskell.Prim
+open import Haskell.Prim.Monad
+  renaming (module Instances to MonadInstances)
+open import Haskell.Prim.String
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.IO
+
+
+--------------------------------------------------------------------------------
+-- MonadFail
+
+record MonadFail (m : Type → Type) : Type₁ where
+  field
+    fail : String → m a
+    overlap ⦃ super ⦄ : Monad m
+
+open MonadFail ⦃...⦄ public
+{-# COMPILE AGDA2HS MonadFail existing-class #-}
+
+module Instances where
+  instance
+    MonadFailList : MonadFail List
+    MonadFailList .fail _ = []
+
+    MonadFailMaybe : MonadFail Maybe
+    MonadFailMaybe .fail _ = Nothing
+
+    iMonadFailIO : MonadFail IO
+    iMonadFailIO .fail = failIO
+open Instances public
diff --git a/lib/base/Haskell/Prim/MonadPlus.agda b/lib/base/Haskell/Prim/MonadPlus.agda
new file mode 100644
index 00000000..21d9aa66
--- /dev/null
+++ b/lib/base/Haskell/Prim/MonadPlus.agda
@@ -0,0 +1,62 @@
+module Haskell.Prim.MonadPlus where
+
+open import Haskell.Prim
+open import Haskell.Prim.Alternative
+  renaming (module Instances to AlternativeInstances)
+open import Haskell.Prim.Monad
+  renaming (module Instances to MonadInstances)
+open import Haskell.Prim.IO
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+
+
+--------------------------------------------------------------------------------
+-- MonadPlus
+
+-- ** base
+record MonadPlus (m : Type → Type) : Type₁ where
+  field
+    overlap ⦃ super₁ ⦄ : Alternative m
+    overlap ⦃ super₂ ⦄ : Monad m
+    mzero : m a
+    mplus : m a → m a → m a
+
+-- ** default
+record DefaultMonadPlus (m : Type → Type) : Type₁ where
+  field
+    overlap ⦃ super₁ ⦄ : Alternative m
+    overlap ⦃ super₂ ⦄ : Monad m
+
+  mzero : m a
+  mzero = empty
+
+  mplus : m a → m a → m a
+  mplus = _<|>_
+
+-- ** export
+open MonadPlus ⦃...⦄ public
+{-# COMPILE AGDA2HS MonadPlus existing-class #-}
+
+-- ** instances
+module Instances where
+  instance
+    open DefaultMonadPlus
+
+    iDefaultMonadPlusList : DefaultMonadPlus List
+    iDefaultMonadPlusList = record {}
+
+    iMonadPlusList : MonadPlus List
+    iMonadPlusList = record {DefaultMonadPlus iDefaultMonadPlusList}
+
+    iDefaultMonadPlusMaybe : DefaultMonadPlus Maybe
+    iDefaultMonadPlusMaybe = record {}
+
+    iMonadPlusMaybe : MonadPlus Maybe
+    iMonadPlusMaybe = record {DefaultMonadPlus iDefaultMonadPlusMaybe}
+
+    iDefaultMonadPlusIO : DefaultMonadPlus IO
+    iDefaultMonadPlusIO = record {}
+
+    iMonadPlusIO : MonadPlus IO
+    iMonadPlusIO = record {DefaultMonadPlus iDefaultMonadPlusIO}
+open Instances public
diff --git a/lib/base/Haskell/Prim/Monoid.agda b/lib/base/Haskell/Prim/Monoid.agda
index a011cd11..f56d99c2 100644
--- a/lib/base/Haskell/Prim/Monoid.agda
+++ b/lib/base/Haskell/Prim/Monoid.agda
@@ -1,50 +1,16 @@
-
 module Haskell.Prim.Monoid where
 
 open import Haskell.Prim
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
 open import Haskell.Prim.Bool
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Either
 open import Haskell.Prim.Tuple
 
---------------------------------------------------
--- Semigroup
-
-record Semigroup (a : Type) : Type where
-  infixr 6 _<>_
-  field _<>_ : a → a → a
-open Semigroup ⦃...⦄ public
-{-# COMPILE AGDA2HS Semigroup existing-class #-}
-
-instance
-  iSemigroupList : Semigroup (List a)
-  iSemigroupList ._<>_ = _++_
-
-  iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a)
-  iSemigroupMaybe ._<>_          Nothing m = m
-  iSemigroupMaybe ._<>_ m        Nothing   = m
-  iSemigroupMaybe ._<>_ (Just x) (Just y)  = Just (x <> y)
-
-  iSemigroupEither : Semigroup (Either a b)
-  iSemigroupEither ._<>_ (Left _) e = e
-  iSemigroupEither ._<>_ e        _ = e
-
-  iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b)
-  iSemigroupFun ._<>_ f g x = f x <> g x
-
-  iSemigroupUnit : Semigroup ⊤
-  iSemigroupUnit ._<>_ _ _ = tt
-
 
-  iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b)
-  iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂
-
-  iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c)
-  iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂
-
-
---------------------------------------------------
+--------------------------------------------------------------------------------
 -- Monoid
 
 -- ** base
@@ -54,6 +20,7 @@ record Monoid (a : Type) : Type where
     overlap ⦃ super ⦄ : Semigroup a
     mappend : a → a → a
     mconcat : List a → a
+
 -- ** defaults
 record DefaultMonoid (a : Type) : Type where
   field
@@ -66,53 +33,57 @@ record DefaultMonoid (a : Type) : Type where
   mconcat : List a → a
   mconcat []       = mempty
   mconcat (x ∷ xs) = x <> mconcat xs
+
 -- ** export
 open Monoid ⦃...⦄ public
 {-# COMPILE AGDA2HS Monoid existing-class #-}
+
 -- ** instances
-instance
-  iDefaultMonoidList : DefaultMonoid (List a)
-  iDefaultMonoidList .DefaultMonoid.mempty = []
+module Instances where
+  instance
+    iDefaultMonoidList : DefaultMonoid (List a)
+    iDefaultMonoidList .DefaultMonoid.mempty = []
 
-  iMonoidList : Monoid (List a)
-  iMonoidList = record{DefaultMonoid iDefaultMonoidList}
+    iMonoidList : Monoid (List a)
+    iMonoidList = record{DefaultMonoid iDefaultMonoidList}
 
-  iDefaultMonoidMaybe : ⦃ Semigroup a ⦄ → DefaultMonoid (Maybe a)
-  iDefaultMonoidMaybe .DefaultMonoid.mempty = Nothing
+    iDefaultMonoidMaybe : ⦃ Semigroup a ⦄ → DefaultMonoid (Maybe a)
+    iDefaultMonoidMaybe .DefaultMonoid.mempty = Nothing
 
-  iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a)
-  iMonoidMaybe = record{DefaultMonoid iDefaultMonoidMaybe}
+    iMonoidMaybe : ⦃ Semigroup a ⦄ → Monoid (Maybe a)
+    iMonoidMaybe = record{DefaultMonoid iDefaultMonoidMaybe}
 
-  iDefaultMonoidFun : ⦃ Monoid b ⦄ → DefaultMonoid (a → b)
-  iDefaultMonoidFun .DefaultMonoid.mempty = λ _ → mempty
+    iDefaultMonoidFun : ⦃ Monoid b ⦄ → DefaultMonoid (a → b)
+    iDefaultMonoidFun .DefaultMonoid.mempty = λ _ → mempty
 
-  iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b)
-  iMonoidFun = record{DefaultMonoid iDefaultMonoidFun}
+    iMonoidFun : ⦃ Monoid b ⦄ → Monoid (a → b)
+    iMonoidFun = record{DefaultMonoid iDefaultMonoidFun}
 
-  iDefaultMonoidUnit : DefaultMonoid ⊤
-  iDefaultMonoidUnit .DefaultMonoid.mempty = tt
+    iDefaultMonoidUnit : DefaultMonoid ⊤
+    iDefaultMonoidUnit .DefaultMonoid.mempty = tt
 
-  iMonoidUnit : Monoid ⊤
-  iMonoidUnit = record{DefaultMonoid iDefaultMonoidUnit}
+    iMonoidUnit : Monoid ⊤
+    iMonoidUnit = record{DefaultMonoid iDefaultMonoidUnit}
 
-  iDefaultMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonoid (a × b)
-  iDefaultMonoidTuple₂ .DefaultMonoid.mempty = (mempty , mempty)
+    iDefaultMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → DefaultMonoid (a × b)
+    iDefaultMonoidTuple₂ .DefaultMonoid.mempty = (mempty , mempty)
 
-  iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b)
-  iMonoidTuple₂ = record{DefaultMonoid iDefaultMonoidTuple₂}
+    iMonoidTuple₂ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → Monoid (a × b)
+    iMonoidTuple₂ = record{DefaultMonoid iDefaultMonoidTuple₂}
 
-  iDefaultMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → DefaultMonoid (a × b × c)
-  iDefaultMonoidTuple₃ .DefaultMonoid.mempty = (mempty , mempty , mempty)
+    iDefaultMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ → DefaultMonoid (a × b × c)
+    iDefaultMonoidTuple₃ .DefaultMonoid.mempty = (mempty , mempty , mempty)
 
-  iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →  Monoid (a × b × c)
-  iMonoidTuple₃ = record{DefaultMonoid iDefaultMonoidTuple₃}
+    iMonoidTuple₃ : ⦃ Monoid a ⦄ → ⦃ Monoid b ⦄ → ⦃ Monoid c ⦄ →  Monoid (a × b × c)
+    iMonoidTuple₃ = record{DefaultMonoid iDefaultMonoidTuple₃}
+open Instances public
 
 open DefaultMonoid
 
 MonoidEndo : Monoid (a → a)
 MonoidEndo = record {DefaultMonoid (λ where
-      .mempty → id
-      .super ._<>_ → _∘_)}
+  .mempty      → id
+  .super ._<>_ → _∘_)}
 
 MonoidEndoᵒᵖ : Monoid (a → a)
 MonoidEndoᵒᵖ = record {DefaultMonoid (λ where
@@ -128,3 +99,17 @@ MonoidDisj : Monoid Bool
 MonoidDisj = record {DefaultMonoid (λ where
   .mempty      → False
   .super ._<>_ → _||_)}
+
+MonoidFirst : Monoid (Maybe a)
+MonoidFirst = record {DefaultMonoid (λ where
+  .mempty      → Nothing
+  .super ._<>_ → λ where
+    Nothing b → b
+    a       _ → a)}
+
+MonoidLast : Monoid (Maybe a)
+MonoidLast = record {DefaultMonoid (λ where
+  .mempty      → Nothing
+  .super ._<>_ → λ where
+    a Nothing → a
+    _       b → b)}
diff --git a/lib/base/Haskell/Prim/Num.agda b/lib/base/Haskell/Prim/Num.agda
index c7c6bb60..cec6a7b4 100644
--- a/lib/base/Haskell/Prim/Num.agda
+++ b/lib/base/Haskell/Prim/Num.agda
@@ -3,15 +3,21 @@
 module Haskell.Prim.Num where
 
 open import Haskell.Prim
+open import Haskell.Prim.Eq
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord
+  renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
+open import Haskell.Prim.Monoid
+  renaming (module Instances to MonoidInstances)
 open import Haskell.Prim.Word
 open import Haskell.Prim.Int
 open import Haskell.Prim.Integer
 open import Haskell.Prim.Double
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Ord
-open import Haskell.Prim.Monoid
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Num
 
 record Num (a : Type) : Type₁ where
@@ -33,88 +39,87 @@ record Num (a : Type) : Type₁ where
     overlap ⦃ numOne ⦄  : number .Number.Constraint 1
 
 open Num ⦃...⦄ public hiding (FromIntegerOK; number)
-
 {-# COMPILE AGDA2HS Num existing-class #-}
 
-instance
-  iNumNat : Num Nat
-  iNumNat .MinusOK n m      = IsFalse (ltNat n m)
-  iNumNat .NegateOK 0       = ⊤
-  iNumNat .NegateOK (suc _) = ⊥
-  iNumNat .Num.FromIntegerOK (negsuc _) = ⊥
-  iNumNat .Num.FromIntegerOK (pos _) = ⊤
-  iNumNat ._+_ n m = addNat n m
-  iNumNat ._-_ n m = monusNat n m
-  iNumNat ._*_ n m = mulNat n m
-  iNumNat .negate n = n
-  iNumNat .abs    n = n
-  iNumNat .signum 0       = 0
-  iNumNat .signum (suc n) = 1
-  iNumNat .fromInteger (pos n) = n
-  iNumNat .fromInteger (negsuc _) ⦃ () ⦄
+module Instances where
+  instance
+    iNumNat : Num Nat
+    iNumNat .MinusOK n m      = IsFalse (ltNat n m)
+    iNumNat .NegateOK 0       = ⊤
+    iNumNat .NegateOK (suc _) = ⊥
+    iNumNat .Num.FromIntegerOK (negsuc _) = ⊥
+    iNumNat .Num.FromIntegerOK (pos _) = ⊤
+    iNumNat ._+_ n m = addNat n m
+    iNumNat ._-_ n m = monusNat n m
+    iNumNat ._*_ n m = mulNat n m
+    iNumNat .negate n = n
+    iNumNat .abs    n = n
+    iNumNat .signum 0       = 0
+    iNumNat .signum (suc n) = 1
+    iNumNat .fromInteger (pos n) = n
+    iNumNat .fromInteger (negsuc _) ⦃ () ⦄
 
-  iNumInt : Num Int
-  iNumInt .MinusOK _ _         = ⊤
-  iNumInt .NegateOK _          = ⊤
-  iNumInt .Num.FromIntegerOK _ = ⊤
-  iNumInt ._+_ x y             = addInt x y
-  iNumInt ._-_ x y             = subInt x y
-  iNumInt ._*_ x y             = mulInt x y
-  iNumInt .negate x            = negateInt x
-  iNumInt .abs x               = absInt x
-  iNumInt .signum x            = signInt x
-  iNumInt .fromInteger n       = integerToInt n
+    iNumInt : Num Int
+    iNumInt .MinusOK _ _         = ⊤
+    iNumInt .NegateOK _          = ⊤
+    iNumInt .Num.FromIntegerOK _ = ⊤
+    iNumInt ._+_ x y             = addInt x y
+    iNumInt ._-_ x y             = subInt x y
+    iNumInt ._*_ x y             = mulInt x y
+    iNumInt .negate x            = negateInt x
+    iNumInt .abs x               = absInt x
+    iNumInt .signum x            = signInt x
+    iNumInt .fromInteger n       = integerToInt n
 
-  iNumInteger : Num Integer
-  iNumInteger .MinusOK _ _ = ⊤
-  iNumInteger .NegateOK _          = ⊤
-  iNumInteger .Num.FromIntegerOK _ = ⊤
-  iNumInteger ._+_ x y             = addInteger x y
-  iNumInteger ._-_ x y             = subInteger x y
-  iNumInteger ._*_ x y             = mulInteger x y
-  iNumInteger .negate x            = negateInteger x
-  iNumInteger .abs x               = absInteger x
-  iNumInteger .signum x            = signInteger x
-  iNumInteger .fromInteger n       = n
+    iNumInteger : Num Integer
+    iNumInteger .MinusOK _ _ = ⊤
+    iNumInteger .NegateOK _          = ⊤
+    iNumInteger .Num.FromIntegerOK _ = ⊤
+    iNumInteger ._+_ x y             = addInteger x y
+    iNumInteger ._-_ x y             = subInteger x y
+    iNumInteger ._*_ x y             = mulInteger x y
+    iNumInteger .negate x            = negateInteger x
+    iNumInteger .abs x               = absInteger x
+    iNumInteger .signum x            = signInteger x
+    iNumInteger .fromInteger n       = n
 
-  iNumWord : Num Word
-  iNumWord .MinusOK _ _         = ⊤
-  iNumWord .NegateOK _          = ⊤
-  iNumWord .Num.FromIntegerOK _ = ⊤
-  iNumWord ._+_ x y             = addWord x y
-  iNumWord ._-_ x y             = subWord x y
-  iNumWord ._*_ x y             = mulWord x y
-  iNumWord .negate x            = negateWord x
-  iNumWord .abs x               = x
-  iNumWord .signum x            = if x == 0 then 0 else 1
-  iNumWord .fromInteger n       = integerToWord n
+    iNumWord : Num Word
+    iNumWord .MinusOK _ _         = ⊤
+    iNumWord .NegateOK _          = ⊤
+    iNumWord .Num.FromIntegerOK _ = ⊤
+    iNumWord ._+_ x y             = addWord x y
+    iNumWord ._-_ x y             = subWord x y
+    iNumWord ._*_ x y             = mulWord x y
+    iNumWord .negate x            = negateWord x
+    iNumWord .abs x               = x
+    iNumWord .signum x            = if x == 0 then 0 else 1
+    iNumWord .fromInteger n       = integerToWord n
 
-  iNumDouble : Num Double
-  iNumDouble .MinusOK _ _         = ⊤
-  iNumDouble .NegateOK _          = ⊤
-  iNumDouble .Num.FromIntegerOK _ = ⊤
-  iNumDouble ._+_ x y             = primFloatPlus x y
-  iNumDouble ._-_ x y             = primFloatMinus x y
-  iNumDouble ._*_ x y             = primFloatTimes x y
-  iNumDouble .negate x            = primFloatMinus 0.0 x
-  iNumDouble .abs x               = if x < 0.0 then primFloatMinus 0.0 x else x
-  iNumDouble .signum x            = case compare x 0.0 of λ where
-                                      LT → -1.0
-                                      EQ → x
-                                      GT → 1.0
-  iNumDouble .fromInteger (pos    n) = fromNat n
-  iNumDouble .fromInteger (negsuc n) = fromNeg (suc n)
+    iNumDouble : Num Double
+    iNumDouble .MinusOK _ _         = ⊤
+    iNumDouble .NegateOK _          = ⊤
+    iNumDouble .Num.FromIntegerOK _ = ⊤
+    iNumDouble ._+_ x y             = primFloatPlus x y
+    iNumDouble ._-_ x y             = primFloatMinus x y
+    iNumDouble ._*_ x y             = primFloatTimes x y
+    iNumDouble .negate x            = primFloatMinus 0.0 x
+    iNumDouble .abs x               = if x < 0.0 then primFloatMinus 0.0 x else x
+    iNumDouble .signum x            = case compare x 0.0 of λ where
+                                        LT → -1.0
+                                        EQ → x
+                                        GT → 1.0
+    iNumDouble .fromInteger (pos    n) = fromNat n
+    iNumDouble .fromInteger (negsuc n) = fromNeg (suc n)
+open Instances public
 
 open DefaultMonoid
 
 MonoidSum : ⦃ iNum : Num a ⦄ → Monoid a
 MonoidSum = record {DefaultMonoid (λ where
   .mempty      → 0
-  .super ._<>_ → _+_
- )}
+  .super ._<>_ → _+_)}
 
 MonoidProduct : ⦃ iNum : Num a ⦄ → Monoid a
 MonoidProduct = record {DefaultMonoid (λ where
   .mempty      → 1
-  .super ._<>_ → _*_
- )}
+  .super ._<>_ → _*_)}
diff --git a/lib/base/Haskell/Prim/Ord.agda b/lib/base/Haskell/Prim/Ord.agda
index beda7476..d3f5eaa9 100644
--- a/lib/base/Haskell/Prim/Ord.agda
+++ b/lib/base/Haskell/Prim/Ord.agda
@@ -3,18 +3,23 @@ module Haskell.Prim.Ord where
 
 open import Haskell.Prim
 open import Haskell.Prim.Eq
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Semigroup
+  renaming (module Instances to SemigroupInstances)
+open import Haskell.Prim.Monoid
+  renaming (module Instances to MonoidInstances)
 open import Haskell.Prim.Bool
 open import Haskell.Prim.Int
 open import Haskell.Prim.Word
 open import Haskell.Prim.Integer
 open import Haskell.Prim.Double
 open import Haskell.Prim.Tuple
-open import Haskell.Prim.Monoid
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Either
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Ordering
 
 data Ordering : Type where
@@ -35,7 +40,8 @@ instance
   iMonoidOrdering : Monoid Ordering
   iMonoidOrdering = record {DefaultMonoid (record {mempty = EQ})}
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Ord
 
 record Ord (a : Type) : Type where
@@ -97,9 +103,7 @@ record OrdFromLessThan (a : Type) : Type where
   min  : a → a → a
   min x y = if y < x then y else x
 
-
 open Ord ⦃...⦄ public
-
 {-# COMPILE AGDA2HS Ord existing-class #-}
 
 private
@@ -117,118 +121,120 @@ private
   minNat (suc x) zero    = zero
   minNat (suc x) (suc y) = suc (minNat x y)
 
-instance
-  iOrdFromLessThanNat : OrdFromLessThan Nat
-  iOrdFromLessThanNat .OrdFromLessThan._<_ = ltNat
-
-  iOrdNat : Ord Nat
-  iOrdNat = record
-    { OrdFromLessThan iOrdFromLessThanNat
-    ; max = maxNat
-    ; min = minNat
-    }
-
-  iOrdFromLessThanInteger : OrdFromLessThan Integer
-  iOrdFromLessThanInteger .OrdFromLessThan._<_ = ltInteger
-
-  iOrdInteger : Ord Integer
-  iOrdInteger = record {OrdFromLessThan iOrdFromLessThanInteger}
-
-  iOrdFromLessThanInt : OrdFromLessThan Int
-  iOrdFromLessThanInt .OrdFromLessThan._<_ = ltInt
-
-  iOrdInt : Ord Int
-  iOrdInt = record {OrdFromLessThan iOrdFromLessThanInt}
-
-  iOrdFromLessThanWord : OrdFromLessThan Word
-  iOrdFromLessThanWord .OrdFromLessThan._<_ = ltWord
-
-  iOrdWord : Ord Word
-  iOrdWord = record {OrdFromLessThan iOrdFromLessThanWord}
-
-  iOrdFromLessThanDouble : OrdFromLessThan Double
-  iOrdFromLessThanDouble .OrdFromLessThan._<_ = primFloatLess
-
-  iOrdDouble : Ord Double
-  iOrdDouble = record {OrdFromLessThan iOrdFromLessThanDouble}
-
-  iOrdFromLessThanChar : OrdFromLessThan Char
-  iOrdFromLessThanChar .OrdFromLessThan._<_ x y = c2n x < c2n y
-
-  iOrdChar : Ord Char
-  iOrdChar = record {OrdFromLessThan iOrdFromLessThanChar}
-
-  iOrdFromCompareBool : OrdFromCompare Bool
-  iOrdFromCompareBool .OrdFromCompare.compare = λ where
-    False True  → LT
-    True  False → GT
-    _     _     → EQ
-
-  iOrdBool : Ord Bool
-  iOrdBool = record {OrdFromCompare iOrdFromCompareBool}
-
-  iOrdFromCompareUnit : OrdFromCompare ⊤
-  iOrdFromCompareUnit .OrdFromCompare.compare = λ _ _ → EQ
-
-  iOrdUnit : Ord ⊤
-  iOrdUnit = record {OrdFromCompare iOrdFromCompareUnit}
-
-  iOrdFromCompareTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (a × b)
-  iOrdFromCompareTuple₂ .OrdFromCompare.compare = λ where
-    (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂
-
-  iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b)
-  iOrdTuple₂ = record {OrdFromCompare iOrdFromCompareTuple₂}
+private
+  compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
+  compareList []       []       = EQ
+  compareList []       (_ ∷ _)  = LT
+  compareList (_ ∷ _)  []       = GT
+  compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys
 
-  iOrdFromCompareTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → OrdFromCompare (a × b × c)
-  iOrdFromCompareTuple₃ .OrdFromCompare.compare = λ where
-    (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂
+module Instances where
+  instance
+    iOrdFromLessThanNat : OrdFromLessThan Nat
+    iOrdFromLessThanNat .OrdFromLessThan._<_ = ltNat
 
-  iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c)
-  iOrdTuple₃ = record {OrdFromCompare iOrdFromCompareTuple₃}
+    iOrdNat : Ord Nat
+    iOrdNat = record
+      { OrdFromLessThan iOrdFromLessThanNat
+      ; max = maxNat
+      ; min = minNat
+      }
+
+    iOrdFromLessThanInteger : OrdFromLessThan Integer
+    iOrdFromLessThanInteger .OrdFromLessThan._<_ = ltInteger
+
+    iOrdInteger : Ord Integer
+    iOrdInteger = record {OrdFromLessThan iOrdFromLessThanInteger}
+
+    iOrdFromLessThanInt : OrdFromLessThan Int
+    iOrdFromLessThanInt .OrdFromLessThan._<_ = ltInt
+
+    iOrdInt : Ord Int
+    iOrdInt = record {OrdFromLessThan iOrdFromLessThanInt}
+
+    iOrdFromLessThanWord : OrdFromLessThan Word
+    iOrdFromLessThanWord .OrdFromLessThan._<_ = ltWord
+
+    iOrdWord : Ord Word
+    iOrdWord = record {OrdFromLessThan iOrdFromLessThanWord}
+
+    iOrdFromLessThanDouble : OrdFromLessThan Double
+    iOrdFromLessThanDouble .OrdFromLessThan._<_ = primFloatLess
+
+    iOrdDouble : Ord Double
+    iOrdDouble = record {OrdFromLessThan iOrdFromLessThanDouble}
+
+    iOrdFromLessThanChar : OrdFromLessThan Char
+    iOrdFromLessThanChar .OrdFromLessThan._<_ x y = c2n x < c2n y
+
+    iOrdChar : Ord Char
+    iOrdChar = record {OrdFromLessThan iOrdFromLessThanChar}
+
+    iOrdFromCompareBool : OrdFromCompare Bool
+    iOrdFromCompareBool .OrdFromCompare.compare = λ where
+      False True  → LT
+      True  False → GT
+      _     _     → EQ
+
+    iOrdBool : Ord Bool
+    iOrdBool = record {OrdFromCompare iOrdFromCompareBool}
+
+    iOrdFromCompareUnit : OrdFromCompare ⊤
+    iOrdFromCompareUnit .OrdFromCompare.compare = λ _ _ → EQ
+
+    iOrdUnit : Ord ⊤
+    iOrdUnit = record {OrdFromCompare iOrdFromCompareUnit}
+
+    iOrdFromCompareTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (a × b)
+    iOrdFromCompareTuple₂ .OrdFromCompare.compare = λ where
+      (x₁ , y₁) (x₂ , y₂) → compare x₁ x₂ <> compare y₁ y₂
+
+    iOrdTuple₂ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (a × b)
+    iOrdTuple₂ = record {OrdFromCompare iOrdFromCompareTuple₂}
+
+    iOrdFromCompareTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → OrdFromCompare (a × b × c)
+    iOrdFromCompareTuple₃ .OrdFromCompare.compare = λ where
+      (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) → compare x₁ x₂ <> compare y₁ y₂ <> compare z₁ z₂
+
+    iOrdTuple₃ : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → ⦃ Ord c ⦄ → Ord (a × b × c)
+    iOrdTuple₃ = record {OrdFromCompare iOrdFromCompareTuple₃}
+
+    iOrdFromCompareList : ⦃ Ord a ⦄ → OrdFromCompare (List a)
+    iOrdFromCompareList .OrdFromCompare.compare = compareList
+
+    iOrdList : ⦃ Ord a ⦄ → Ord (List a)
+    iOrdList = record {OrdFromCompare iOrdFromCompareList}
+
+    iOrdFromCompareMaybe : ⦃ Ord a ⦄ → OrdFromCompare (Maybe a)
+    iOrdFromCompareMaybe .OrdFromCompare.compare = λ where
+      Nothing  Nothing  → EQ
+      Nothing  (Just _) → LT
+      (Just _) Nothing  → GT
+      (Just x) (Just y) → compare x y
+
+    iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a)
+    iOrdMaybe = record {OrdFromCompare iOrdFromCompareMaybe}
+
+    iOrdFromCompareEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (Either a b)
+    iOrdFromCompareEither .OrdFromCompare.compare = λ where
+      (Left  x) (Left  y) → compare x y
+      (Left  _) (Right _) → LT
+      (Right _) (Left  _) → GT
+      (Right x) (Right y) → compare x y
+
+    iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b)
+    iOrdEither = record {OrdFromCompare iOrdFromCompareEither}
 
-compareList : ⦃ Ord a ⦄ → List a → List a → Ordering
-compareList []       []       = EQ
-compareList []       (_ ∷ _)  = LT
-compareList (_ ∷ _)  []       = GT
-compareList (x ∷ xs) (y ∷ ys) = compare x y <> compareList xs ys
+    iOrdFromCompareOrdering : OrdFromCompare Ordering
+    iOrdFromCompareOrdering .OrdFromCompare.compare = λ where
+      LT LT → EQ
+      LT _  → LT
+      _  LT → GT
+      EQ EQ → EQ
+      EQ GT → LT
+      GT EQ → GT
+      GT GT → EQ
 
-instance
-  iOrdFromCompareList : ⦃ Ord a ⦄ → OrdFromCompare (List a)
-  iOrdFromCompareList .OrdFromCompare.compare = compareList
-
-  iOrdList : ⦃ Ord a ⦄ → Ord (List a)
-  iOrdList = record {OrdFromCompare iOrdFromCompareList}
-
-  iOrdFromCompareMaybe : ⦃ Ord a ⦄ → OrdFromCompare (Maybe a)
-  iOrdFromCompareMaybe .OrdFromCompare.compare = λ where
-    Nothing  Nothing  → EQ
-    Nothing  (Just _) → LT
-    (Just _) Nothing  → GT
-    (Just x) (Just y) → compare x y
-
-  iOrdMaybe : ⦃ Ord a ⦄ → Ord (Maybe a)
-  iOrdMaybe = record {OrdFromCompare iOrdFromCompareMaybe}
-
-  iOrdFromCompareEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → OrdFromCompare (Either a b)
-  iOrdFromCompareEither .OrdFromCompare.compare = λ where
-    (Left  x) (Left  y) → compare x y
-    (Left  _) (Right _) → LT
-    (Right _) (Left  _) → GT
-    (Right x) (Right y) → compare x y
-
-  iOrdEither : ⦃ Ord a ⦄ → ⦃ Ord b ⦄ → Ord (Either a b)
-  iOrdEither = record {OrdFromCompare iOrdFromCompareEither}
-
-  iOrdFromCompareOrdering : OrdFromCompare Ordering
-  iOrdFromCompareOrdering .OrdFromCompare.compare = λ where
-    LT LT → EQ
-    LT _  → LT
-    _  LT → GT
-    EQ EQ → EQ
-    EQ GT → LT
-    GT EQ → GT
-    GT GT → EQ
-
-  iOrdOrdering : Ord Ordering
-  iOrdOrdering = record {OrdFromCompare iOrdFromCompareOrdering}
+    iOrdOrdering : Ord Ordering
+    iOrdOrdering = record {OrdFromCompare iOrdFromCompareOrdering}
+open Instances public
diff --git a/lib/base/Haskell/Prim/Semigroup.agda b/lib/base/Haskell/Prim/Semigroup.agda
new file mode 100644
index 00000000..25bcbf5e
--- /dev/null
+++ b/lib/base/Haskell/Prim/Semigroup.agda
@@ -0,0 +1,48 @@
+module Haskell.Prim.Semigroup where
+
+open import Haskell.Prim
+open import Haskell.Prim.List
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Either
+open import Haskell.Prim.Tuple
+
+
+--------------------------------------------------------------------------------
+-- Semigroup
+
+-- ** base
+record Semigroup (a : Type) : Type where
+  infixr 6 _<>_
+  field _<>_ : a → a → a
+
+-- ** export
+open Semigroup ⦃...⦄ public
+{-# COMPILE AGDA2HS Semigroup existing-class #-}
+
+-- ** instances
+module Instances where
+  instance
+    iSemigroupList : Semigroup (List a)
+    iSemigroupList ._<>_ = _++_
+
+    iSemigroupMaybe : ⦃ Semigroup a ⦄ → Semigroup (Maybe a)
+    iSemigroupMaybe ._<>_          Nothing m = m
+    iSemigroupMaybe ._<>_ m        Nothing   = m
+    iSemigroupMaybe ._<>_ (Just x) (Just y)  = Just (x <> y)
+
+    iSemigroupEither : Semigroup (Either a b)
+    iSemigroupEither ._<>_ (Left _) e = e
+    iSemigroupEither ._<>_ e        _ = e
+
+    iSemigroupFun : ⦃ Semigroup b ⦄ → Semigroup (a → b)
+    iSemigroupFun ._<>_ f g x = f x <> g x
+
+    iSemigroupUnit : Semigroup ⊤
+    iSemigroupUnit ._<>_ _ _ = tt
+
+    iSemigroupTuple₂ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → Semigroup (a × b)
+    iSemigroupTuple₂ ._<>_ (x₁ , y₁) (x₂ , y₂) = x₁ <> x₂ , y₁ <> y₂
+
+    iSemigroupTuple₃ : ⦃ Semigroup a ⦄ → ⦃ Semigroup b ⦄ → ⦃ Semigroup c ⦄ → Semigroup (a × b × c)
+    iSemigroupTuple₃ ._<>_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ <> x₂ , y₁ <> y₂ , z₁ <> z₂
+open Instances public
diff --git a/lib/base/Haskell/Prim/Show.agda b/lib/base/Haskell/Prim/Show.agda
index 601512b1..01f26b26 100644
--- a/lib/base/Haskell/Prim/Show.agda
+++ b/lib/base/Haskell/Prim/Show.agda
@@ -2,22 +2,25 @@
 module Haskell.Prim.Show where
 
 open import Haskell.Prim
+open import Haskell.Prim.Eq
+  renaming (module Instances to EqInstances)
+open import Haskell.Prim.Ord
+  renaming (module Instances to OrdInstances)
+open import Haskell.Prim.Foldable
+  renaming (module Instances to FoldableInstances)
 open import Haskell.Prim.String
 open import Haskell.Prim.List
 open import Haskell.Prim.Word
 open import Haskell.Prim.Double
 open import Haskell.Prim.Maybe
-open import Haskell.Prim.Eq
 open import Haskell.Prim.Tuple
-open import Haskell.Prim.Ord
 open import Haskell.Prim.Either
 open import Haskell.Prim.Integer
 open import Haskell.Prim.Bool
 open import Haskell.Prim.Int
-open import Haskell.Prim.Foldable
 
 
---------------------------------------------------
+--------------------------------------------------------------------------------
 -- Show
 
 ShowS : Type
@@ -72,88 +75,90 @@ shows = showsPrec 0
 {-# COMPILE AGDA2HS Show existing-class #-}
 
 -- ** instances
-instance
-  iShow₂Nat : Show₂ Nat
-  iShow₂Nat .Show₂.show = primStringToList ∘ primShowNat
+module Instances where
+  instance
+    iShow₂Nat : Show₂ Nat
+    iShow₂Nat .Show₂.show = primStringToList ∘ primShowNat
 
-  iShowNat : Show Nat
-  iShowNat = record {Show₂ iShow₂Nat}
+    iShowNat : Show Nat
+    iShowNat = record {Show₂ iShow₂Nat}
 
-  iShow₂Integer : Show₂ Integer
-  iShow₂Integer .Show₂.show = showInteger
+    iShow₂Integer : Show₂ Integer
+    iShow₂Integer .Show₂.show = showInteger
 
-  iShowInteger : Show Integer
-  iShowInteger = record {Show₂ iShow₂Integer}
+    iShowInteger : Show Integer
+    iShowInteger = record {Show₂ iShow₂Integer}
 
-  iShow₂Int : Show₂ Int
-  iShow₂Int .Show₂.show = showInt
+    iShow₂Int : Show₂ Int
+    iShow₂Int .Show₂.show = showInt
 
-  iShowInt : Show Int
-  iShowInt = record{Show₂ iShow₂Int}
+    iShowInt : Show Int
+    iShowInt = record{Show₂ iShow₂Int}
 
-  iShow₂Word : Show₂ Word
-  iShow₂Word .Show₂.show = showWord
+    iShow₂Word : Show₂ Word
+    iShow₂Word .Show₂.show = showWord
 
-  iShowWord : Show Word
-  iShowWord = record{Show₂ iShow₂Word}
+    iShowWord : Show Word
+    iShowWord = record{Show₂ iShow₂Word}
 
-  iShow₂Double : Show₂ Double
-  iShow₂Double .Show₂.show = primStringToList ∘ primShowFloat
+    iShow₂Double : Show₂ Double
+    iShow₂Double .Show₂.show = primStringToList ∘ primShowFloat
 
-  iShowDouble : Show Double
-  iShowDouble = record{Show₂ iShow₂Double}
+    iShowDouble : Show Double
+    iShowDouble = record{Show₂ iShow₂Double}
 
-  iShow₂Bool : Show₂ Bool
-  iShow₂Bool .Show₂.show = λ where False → "False"; True → "True"
+    iShow₂Bool : Show₂ Bool
+    iShow₂Bool .Show₂.show = λ where False → "False"; True → "True"
 
-  iShowBool : Show Bool
-  iShowBool = record{Show₂ iShow₂Bool}
+    iShowBool : Show Bool
+    iShowBool = record{Show₂ iShow₂Bool}
 
-  iShow₁Char : Show₁ Char
-  iShow₁Char .Show₁.showsPrec _ = showString ∘ primStringToList ∘ primShowChar
+    iShow₁Char : Show₁ Char
+    iShow₁Char .Show₁.showsPrec _ = showString ∘ primStringToList ∘ primShowChar
 
-  iShowChar : Show Char
-  iShowChar = record{Show₁ iShow₁Char}
+    iShowChar : Show Char
+    iShowChar = record{Show₁ iShow₁Char}
 
-  iShow₁List : ⦃ Show a ⦄ → Show₁ (List a)
-  iShow₁List .Show₁.showsPrec _ = showList
+    iShow₁List : ⦃ Show a ⦄ → Show₁ (List a)
+    iShow₁List .Show₁.showsPrec _ = showList
 
-  iShowList : ⦃ Show a ⦄ → Show (List a)
-  iShowList = record{Show₁ iShow₁List}
+    iShowList : ⦃ Show a ⦄ → Show (List a)
+    iShowList = record{Show₁ iShow₁List}
 
-private
-  showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS
-  showApp₁ p tag x = showParen (p > 10) $
-    showString tag ∘ showString " " ∘ showsPrec 11 x
+  private
+    showApp₁ : ⦃ Show a ⦄ → Int → String → a → ShowS
+    showApp₁ p tag x = showParen (p > 10) $
+      showString tag ∘ showString " " ∘ showsPrec 11 x
 
-instance
-  iShow₁Maybe : ⦃ Show a ⦄ → Show₁ (Maybe a)
-  iShow₁Maybe .Show₁.showsPrec = λ where
-    p Nothing  → showString "Nothing"
-    p (Just x) → showApp₁ p "Just" x
+  instance
+    iShow₁Maybe : ⦃ Show a ⦄ → Show₁ (Maybe a)
+    iShow₁Maybe .Show₁.showsPrec = λ where
+      p Nothing  → showString "Nothing"
+      p (Just x) → showApp₁ p "Just" x
 
-  iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
-  iShowMaybe = record{Show₁ iShow₁Maybe}
+    iShowMaybe : ⦃ Show a ⦄ → Show (Maybe a)
+    iShowMaybe = record{Show₁ iShow₁Maybe}
 
-  iShow₁Either : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (Either a b)
-  iShow₁Either .Show₁.showsPrec = λ where
-    p (Left  x) → showApp₁ p "Left"  x
-    p (Right y) → showApp₁ p "Right" y
+    iShow₁Either : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (Either a b)
+    iShow₁Either .Show₁.showsPrec = λ where
+      p (Left  x) → showApp₁ p "Left"  x
+      p (Right y) → showApp₁ p "Right" y
 
-  iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b)
-  iShowEither = record{Show₁ iShow₁Either}
+    iShowEither : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (Either a b)
+    iShowEither = record{Show₁ iShow₁Either}
 
-instance
-  iShow₁Tuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (a × b)
-  iShow₁Tuple₂ .Show₁.showsPrec = λ _ → λ where
-    (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")"
+  instance
+    iShow₁Tuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show₁ (a × b)
+    iShow₁Tuple₂ .Show₁.showsPrec = λ _ → λ where
+      (x , y) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ")"
 
-  iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b)
-  iShowTuple₂ = record{Show₁ iShow₁Tuple₂}
+    iShowTuple₂ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → Show (a × b)
+    iShowTuple₂ = record{Show₁ iShow₁Tuple₂}
 
-  iShow₁Tuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show₁ (a × b × c)
-  iShow₁Tuple₃ .Show₁.showsPrec = λ _ → λ where
-    (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")"
+    iShow₁Tuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show₁ (a × b × c)
+    iShow₁Tuple₃ .Show₁.showsPrec = λ _ → λ where
+      (x , y , z) → showString "(" ∘ shows x ∘ showString ", " ∘ shows y ∘ showString ", " ∘ shows z ∘ showString ")"
 
-  iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c)
-  iShowTuple₃ = record{Show₁ iShow₁Tuple₃}
+    iShowTuple₃ : ⦃ Show a ⦄ → ⦃ Show b ⦄ → ⦃ Show c ⦄ → Show (a × b × c)
+    iShowTuple₃ = record{Show₁ iShow₁Tuple₃}
+open Instances public
diff --git a/lib/base/Haskell/Prim/String.agda b/lib/base/Haskell/Prim/String.agda
index 8024ce07..d5e80f22 100644
--- a/lib/base/Haskell/Prim/String.agda
+++ b/lib/base/Haskell/Prim/String.agda
@@ -2,51 +2,18 @@
 module Haskell.Prim.String where
 
 open import Haskell.Prim
-open import Haskell.Prim.List
-open import Haskell.Prim.Foldable
+
 
 --------------------------------------------------
 -- String
+
 -- This is _not_ the builtin String type of Agda
 -- which is defined by postulates.
 -- `fromString` can be used to convert back
 -- to builtin Agda strings.
-
 String = List Char
 
 instance
   iIsStringString : IsString String
   iIsStringString .IsString.Constraint _ = ⊤
   iIsStringString .fromString s = primStringToList s
-
-private
-  cons : Char → List String → List String
-  cons c []       = (c ∷ []) ∷ []
-  cons c (s ∷ ss) = (c ∷ s) ∷ ss
-
-lines : String → List String
-lines []         = []
-lines ('\n' ∷ s) = [] ∷ lines s
-lines (c    ∷ s) = cons c (lines s)
-
-private
- mutual
-  space : String → List String
-  space [] = []
-  space (c ∷ s) = if primIsSpace c then space s else cons c (word s)
-
-  word  : String → List String
-  word []      = []
-  word (c ∷ s) = if primIsSpace c then [] ∷ space s else cons c (word s)
-
-words : String → List String
-words [] = []
-words s@(c ∷ s₁) = if primIsSpace c then space s₁ else word s
-
-unlines : List String → String
-unlines = concatMap (_++ "\n")
-
-unwords : List String → String
-unwords [] = ""
-unwords (w ∷ []) = w
-unwords (w ∷ ws) = w ++ ' ' ∷ unwords ws
diff --git a/lib/base/Haskell/Prim/Traversable.agda b/lib/base/Haskell/Prim/Traversable.agda
index 0c97fbe7..d4749c74 100644
--- a/lib/base/Haskell/Prim/Traversable.agda
+++ b/lib/base/Haskell/Prim/Traversable.agda
@@ -1,18 +1,21 @@
-
-
 module Haskell.Prim.Traversable where
 
 open import Haskell.Prim
-open import Haskell.Prim.Applicative
 open import Haskell.Prim.Functor
-open import Haskell.Prim.Foldable
+  renaming (module Instances to FunctorInstances)
+open import Haskell.Prim.Applicative
+  renaming (module Instances to ApplicativeInstances)
 open import Haskell.Prim.Monad
+  renaming (module Instances to MonadInstances)
+open import Haskell.Prim.Foldable
+  renaming (module Instances to FoldableInstances)
 open import Haskell.Prim.List
 open import Haskell.Prim.Maybe
 open import Haskell.Prim.Either
 open import Haskell.Prim.Tuple
 
---------------------------------------------------
+
+--------------------------------------------------------------------------------
 -- Traversable
 
 -- ** base
@@ -25,6 +28,7 @@ record Traversable (t : Type → Type) : Type₁ where
     sequenceA : ⦃ Applicative f ⦄ → t (f a) → f (t a)
     mapM : ⦃ Monad m ⦄ → (a → m b) → t a → m (t b)
     sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
+
 -- ** defaults
 record DefaultTraversable (t : Type → Type) : Type₁ where
   field
@@ -40,39 +44,44 @@ record DefaultTraversable (t : Type → Type) : Type₁ where
 
   sequence : ⦃ Monad m ⦄ → t (m a) → m (t a)
   sequence = sequenceA
+
 -- ** export
 open Traversable ⦃...⦄ public
 {-# COMPILE AGDA2HS Traversable existing-class #-}
+
 -- ** instances
-private
-  mkTraversable : DefaultTraversable t → Traversable t
-  mkTraversable x = record {DefaultTraversable x}
-
-  infix 0 traverse=_
-  traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄
-            → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b))
-            → Traversable t
-  traverse= x = record {DefaultTraversable (record {traverse = x})}
-instance
-  open DefaultTraversable
-
-  iTraversableList : Traversable List
-  iTraversableList = traverse= traverseList
-    where
-      traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b)
-      traverseList f []       = pure []
-      traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈
-
-  iTraversableMaybe : Traversable Maybe
-  iTraversableMaybe = traverse= λ where
-    f Nothing  → pure Nothing
-    f (Just x) → Just <$> f x
-
-  iTraversableEither : Traversable (Either a)
-  iTraversableEither = traverse= λ where
-    f (Left  x) → pure (Left x)
-    f (Right y) → Right <$> f y
-
-  iTraversablePair : Traversable (a ×_)
-  iTraversablePair = traverse= λ
-    f (x , y) → (x ,_) <$> f y
+module Instances where
+  private
+    mkTraversable : DefaultTraversable t → Traversable t
+    mkTraversable x = record {DefaultTraversable x}
+
+    infix 0 traverse=_
+    traverse=_ : ⦃ Functor t ⦄ → ⦃ Foldable t ⦄
+              → (∀ {f a b} → ⦃ Applicative f ⦄ → (a → f b) → t a → f (t b))
+              → Traversable t
+    traverse= x = record {DefaultTraversable (record {traverse = x})}
+
+  instance
+    open DefaultTraversable
+
+    iTraversableList : Traversable List
+    iTraversableList = traverse= traverseList
+      where
+        traverseList : ⦃ Applicative f ⦄ → (a → f b) → List a → f (List b)
+        traverseList f []       = pure []
+        traverseList f (x ∷ xs) = ⦇ f x ∷ traverseList f xs ⦈
+
+    iTraversableMaybe : Traversable Maybe
+    iTraversableMaybe = traverse= λ where
+      f Nothing  → pure Nothing
+      f (Just x) → fmap Just (f x)
+
+    iTraversableEither : Traversable (Either a)
+    iTraversableEither = traverse= λ where
+      f (Left  x) → pure (Left x)
+      f (Right y) → fmap Right (f y)
+
+    iTraversablePair : Traversable (a ×_)
+    iTraversablePair = traverse= λ
+      f (x , y) → fmap (x ,_) (f y)
+open Instances public
diff --git a/test/Succeed/Issue421.agda b/test/Succeed/Issue421.agda
index 250cf454..bc61acb7 100644
--- a/test/Succeed/Issue421.agda
+++ b/test/Succeed/Issue421.agda
@@ -18,12 +18,12 @@ instance
   iFunctorIdentity : Functor Identity
   iFunctorIdentity = record {DefaultFunctor iDefaultFunctorIdentity}
 
-  iDefaultApplicativeIdentity : DefaultApplicative Identity
-  iDefaultApplicativeIdentity .DefaultApplicative.pure = MkIdentity
-  iDefaultApplicativeIdentity .DefaultApplicative._<*>_ (MkIdentity f) (MkIdentity x) = MkIdentity (f x)
+  iDefaultApplicativeIdentity : ApplicativeFrom<*> Identity
+  iDefaultApplicativeIdentity .ApplicativeFrom<*>.pure = MkIdentity
+  iDefaultApplicativeIdentity .ApplicativeFrom<*>._<*>_ (MkIdentity f) (MkIdentity x) = MkIdentity (f x)
 
   iApplicativeIdentity : Applicative Identity
-  iApplicativeIdentity = record {DefaultApplicative iDefaultApplicativeIdentity}
+  iApplicativeIdentity = record {ApplicativeFrom<*> iDefaultApplicativeIdentity}
 
 {-# COMPILE AGDA2HS iFunctorIdentity #-}
 {-# COMPILE AGDA2HS iApplicativeIdentity #-}      -- generates pure and (<*>) multiple times