fix the built-in typeclasses mess

src/Data/Nat.hs

@@ -16,12 +16,10 @@ module Data.Nat where
 
 import Relation.Equality
 import Data.Bool
-import Data.Integer              (Integer)
-import Data.Function             (id, const, (∘))
-import Data.TypeClass            (Eq, Show, Num, Enum, Bounded)
+import Data.Integer
+import Data.Function
 import Data.Singletons.TH hiding ((:<), (:>), (%:<), Refl, Min, sMin, Max, sMax)
-
-import qualified Data.TypeClass as T
+import Data.TypeClass     as T
 
 singletons [d|
 
@@ -29,7 +27,6 @@ singletons [d|
   data ℕ ∷ ★ where
     Z ∷ ℕ     -- ^ Zero
     S ∷ ℕ → ℕ -- ^ Successor
-    deriving (Eq, Show)
 
   infixl 6 +
   infixl 7 ×
@@ -86,37 +83,40 @@ singletons [d|
   fact (S n) = (S n) × (fact n)
   |]
 
+deriving instance Eq ℕ
+
+deriving instance Show ℕ
 
 instance Num ℕ where
-  (+) = (+)
-  (-) = (-)
-  (*) = (×)
+  (+) = (Data.Nat.+)
+  (-) = (Data.Nat.-)
+  (*) = (Data.Nat.×)
   abs = id
   signum = const 1
   negate = id
-  fromInteger = fromInteger
+  fromInteger = _ℤtoℕ
 
 instance Enum ℕ where
-  toEnum   = fromInteger ∘ T.toInteger
-  fromEnum = T.fromInteger ∘ toInteger
+  toEnum   = _ℤtoℕ ∘ T.toInteger
+  fromEnum = T.fromInteger ∘ _ℕtoℤ
 
 instance Bounded ℕ where
   minBound = Z
   maxBound = (∞)
 
 
--- | Convert a natural into an 'Integer'
-toInteger ∷ ℕ → Integer
-toInteger Z     = 0
-toInteger (S n) = 1 T.+ toInteger n
+-- | Convert a natural into an integer
+_ℕtoℤ ∷ ℕ → ℤ
+_ℕtoℤ Z     = 0
+_ℕtoℤ (S n) = 1 T.+ _ℕtoℤ n
 
 
--- | Convert an 'Integer' into a natural
-fromInteger ∷ Integer → ℕ
-fromInteger 0 = Z
-fromInteger n
-  | n T.<= 0 = 0
-  | n T.>  0 = S (fromInteger (T.pred n)) 
+-- | Convert an integer into a natural
+_ℤtoℕ ∷ ℤ → ℕ
+_ℤtoℕ 0 = Z
+_ℤtoℕ n
+  | n T.<= 0 = Z
+  | n T.>  0 = S (_ℤtoℕ (T.pred n))
 
 
 -- | Infinity

src/Data/TypeClass.hs

@@ -1,10 +1,13 @@
+{-# LANGUAGE UnicodeSyntax         #-}
+{-# LANGUAGE RebindableSyntax      #-}
+
 -- | Exports haskell built-in typeclasses
 module Data.TypeClass
   ( Eq(..)
   , Ord(..)
   , Enum(..)
   , Bounded(..)
-  , Num(..)
+  , Num(..), (×)
   , Integral(..)
   , Show(..)
   , Read(..)
@@ -17,3 +20,10 @@ import GHC.Show
 import GHC.Read
 import GHC.Num
 import GHC.Exts
+import Prelude (Eq(..), Ord(..), Integral(..))
+
+-- * Aliases
+
+-- | Multiplication
+(×) ∷ Num a ⇒ a → a → a
+(×) = (*)

src/Data/Vec.hs

@@ -8,10 +8,9 @@
 {-# LANGUAGE ScopedTypeVariables   #-}
 {-# LANGUAGE NoImplicitPrelude     #-}
 {-# LANGUAGE UndecidableInstances  #-}
-{-# LANGUAGE TemplateHaskell       #-}
-{-# LANGUAGE QuasiQuotes           #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
+{-# LANGUAGE RebindableSyntax      #-}
 
 -- | Defines a vector type, analogous to a list, that achieves
 -- type-safe operation like resizing and concatenation by using
@@ -20,14 +19,14 @@ module Data.Vec where
 
 import Relation.Equality (gcastWith)
 import Data.Kind         (Type)
-import Data.Nat
+import Data.Nat          hiding ((+), (-), (×), min, max)
 import Data.Bool
+import Data.Maybe        (Maybe(..))
 import Data.Char         (Char)
 import Data.Function     ((∘))
-import Data.TypeClass    (Show, Eq, Ord, Num, IsList, IsString)
 import Data.Singletons   (SingI, sing)
 
-import qualified Data.TypeClass as T
+import Data.TypeClass
 
 
 infixr 5 :-
@@ -45,12 +44,12 @@ type String n = Vec Char n
 deriving instance Eq a ⇒ Eq (Vec a n)
 
 instance Show a ⇒ Show (Vec a n) where
-  showsPrec d = T.showsPrec d ∘ toList
+  showsPrec d = showsPrec d ∘ vecToList
 
 instance SingI n ⇒ IsList (Vec a n) where
   type Item (Vec a n) = a
-  fromList = fromList
-  toList   = toList
+  fromList = listToVec
+  toList   = vecToList
 
 instance SingI n ⇒ IsString (String n) where
   fromString = fromList
@@ -60,9 +59,9 @@ instance SingI n ⇒ IsString (String n) where
 -- * Conversions
 
 -- | Convert a 'Vec' into a List
-toList ∷ Vec a n → [a]
-toList Nil = []
-toList (x :- xs) = x : toList xs
+vecToList ∷ Vec a n → [a]
+vecToList Nil = []
+vecToList (x :- xs) = x : vecToList xs
 
 
 -- | Convert a List into a 'Vec'
@@ -70,8 +69,8 @@ toList (x :- xs) = x : toList xs
 -- It's not possible to convert an infinite list to a vector
 -- as haskell does not permit constructing infinite type,
 -- which the resulting vector length would be.
-fromList ∷ SingI n ⇒ [a] → Vec a n
-fromList = f sing
+listToVec ∷ SingI n ⇒ [a] → Vec a n
+listToVec = f sing
   where  f ∷ Sℕ n → [a] → Vec a n
          f SZ     _      = Nil
          f (SS n) (x:xs) = x :- f n xs
@@ -278,24 +277,27 @@ all p (x :- xs) = and (map p (x :- xs))
 
 -- | The least element of a vector.
 minimum ∷ Ord a ⇒ Vec a (S n) → a
-minimum = foldr₁ T.min
+minimum = foldr₁ min
 
 
 -- | The largest element of a vector.
 maximum ∷ Ord a ⇒ Vec a (S n) → a
-maximum = foldr₁ T.max
+maximum = foldr₁ max
 
 
 -- | The 'sum' function computes the sum of the numbers of a vector.
 sum ∷ Num a ⇒ Vec a n → a
-sum = foldr (T.+) 0
+sum = foldr (+) 0
 
 
 -- | The 'product' function computes the product of the numbers of a vector.
 product ∷ Num a ⇒ Vec a n → a
-product = foldr (T.*) 0
+product = foldr (×) 1
 
 
+-- * Subvectors
+-- Extracting subvectors
+
 -- | 'take' returns the first @n@ element of the vector
 take ∷ ∀ a n m. SingI n ⇒ Vec a m → Vec a n
 take = take' (sing ∷ Sℕ n)