Drop singletons dependency

Solves #15

CHANGELOG.md

@@ -1,5 +1,9 @@
 # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package
 
+## 0.4
+* Drop `singletons` dependency [#15](https://github.com/clash-lang/ghc-typelits-knownnat/issues/15)
+  * `KnownNatN` classes no longer have the `KnownNatFN` associated type family
+
 ## 0.3.1 *August 17th 2017*
 * Fix testsuite for GHC 8.2.1
 

README.md

@@ -52,15 +52,12 @@ And, given the type family `Max`:
 type family Max (a :: Nat) (b :: Nat) :: Nat where
   Max 0 b = b
   Max a b = If (a <=? b) b a
-
-$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol
 ```
 
 and corresponding `KnownNat2` instance:
 
 ```haskell
 instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where
-  type KnownNatF2 "TestFunctions.Max" = MaxSym0
   natSing2 = let x = natVal (Proxy @ a)
                  y = natVal (Proxy @ b)
                  z = max x y

ghc-typelits-knownnat.cabal

@@ -1,5 +1,5 @@
 name:                ghc-typelits-knownnat
-version:             0.3.1
+version:             0.4
 synopsis:            Derive KnownNat constraints from other KnownNat constraints
 description:
   A type checker plugin for GHC that can derive \"complex\" @KnownNat@
@@ -85,7 +85,6 @@ library
                        ghc                       >= 8.0.1    && <8.4,
                        ghc-tcplugins-extra       >= 0.2,
                        ghc-typelits-natnormalise >= 0.5.2    && <0.6,
-                       singletons                >= 2.2      && <2.4,
                        transformers              >= 0.5.2.0  && <0.6,
                        template-haskell          >= 2.11.0.0 && <2.13
   hs-source-dirs:      src
@@ -102,7 +101,6 @@ test-suite test-ghc-typelits-knownnat
   build-depends:       base                      >= 4.8   && <5,
                        ghc-typelits-knownnat,
                        ghc-typelits-natnormalise >= 0.5   && <0.6,
-                       singletons                >= 2.2   && <2.4,
                        tasty                     >= 0.10,
                        tasty-hunit               >= 0.9,
                        tasty-quickcheck          >= 0.8

src/GHC/TypeLits/KnownNat.hs

@@ -30,13 +30,9 @@ of @Max@, then you must define:
              UndecidableInstances \#-\}
 
 import Data.Proxy            (Proxy (..))
-import Data.Singletons.TH    (genDefunSymbols)
 import GHC.TypeLits.KnownNat
 
-$(genDefunSymbols [''Max]) -- creates the \'MaxSym0\' symbol
-
 instance (KnownNat a, KnownNat b) => 'KnownNat2' $('nameToSymbol' ''Max) a b where
-  type 'KnownNatF2' $('nameToSymbol' ''Max) = MaxSym0
   natSing2 = let x = natVal (Proxy @a)
                  y = natVal (Proxy @b)
                  z = max x y
@@ -95,8 +91,6 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where
 {-# LANGUAGE TypeApplications      #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE TypeFamilies          #-}
-{-# LANGUAGE TypeInType            #-}
-{-# LANGUAGE UndecidableInstances  #-}
 
 {-# LANGUAGE Trustworthy #-}
 
@@ -121,20 +115,16 @@ import Data.Proxy             (Proxy (..))
 import GHC.TypeNats
   (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=), natVal)
 import GHC.TypeLits           (Symbol)
+import Numeric.Natural        (Natural)
 #else
 import GHC.TypeLits           (KnownNat, Nat, Symbol, type (+), type (*),
                                type (^), type (-), type (<=), natVal)
 #endif
-import Data.Singletons        (type (~>), type (@@))
-import Data.Promotion.Prelude (type (:+$), type (:*$), type (:^$), type (:-$))
-#if MIN_VERSION_ghc(8,2,0)
-import Numeric.Natural        (Natural)
-#endif
 
 import GHC.TypeLits.KnownNat.TH
 
 -- | Singleton natural number
-newtype SNatKn (n :: Nat) =
+newtype SNatKn (f :: Symbol) =
 #if MIN_VERSION_ghc(8,2,0)
   SNatKn Natural
 #else
@@ -147,42 +137,36 @@ newtype SNatKn (n :: Nat) =
 -- type-level operation. Use 'nameToSymbol' to get the fully qualified
 -- TH Name as a 'Symbol'
 class KnownNat1 (f :: Symbol) (a :: Nat) where
-  type KnownNatF1 f :: Nat ~> Nat
-  natSing1 :: SNatKn (KnownNatF1 f @@ a)
+  natSing1 :: SNatKn f
 
 -- | Class for arithmetic functions with /two/ arguments.
 --
 -- The 'Symbol' /f/ must correspond to the fully qualified name of the
 -- type-level operation. Use 'nameToSymbol' to get the fully qualified
 -- TH Name as a 'Symbol'
 class KnownNat2 (f :: Symbol) (a :: Nat) (b :: Nat) where
-  type KnownNatF2 f :: Nat ~> Nat ~> Nat
-  natSing2 :: SNatKn (KnownNatF2 f @@ a @@ b)
+  natSing2 :: SNatKn f
 
 -- | Class for arithmetic functions with /three/ arguments.
 --
 -- The 'Symbol' /f/ must correspond to the fully qualified name of the
 -- type-level operation. Use 'nameToSymbol' to get the fully qualified
 -- TH Name as a 'Symbol'
 class KnownNat3 (f :: Symbol) (a :: Nat) (b :: Nat) (c :: Nat) where
-  type KnownNatF3 f :: Nat ~> Nat ~> Nat ~> Nat
-  natSing3 :: SNatKn (KnownNatF3 f @@ a @@ b @@ c)
+  natSing3 :: SNatKn f
 
 -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.+'
 instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(+)) a b where
-  type KnownNatF2 $(nameToSymbol ''(+)) = (:+$)
   natSing2 = SNatKn (natVal (Proxy @a) + natVal (Proxy @b))
   {-# INLINE natSing2 #-}
 
 -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.*'
 instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(*)) a b where
-  type KnownNatF2 $(nameToSymbol ''(*)) = (:*$)
   natSing2 = SNatKn (natVal (Proxy @a) * natVal (Proxy @b))
   {-# INLINE natSing2 #-}
 
 -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^'
 instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where
-  type KnownNatF2 $(nameToSymbol ''(^)) = (:^$)
   natSing2 = let x = natVal (Proxy @ a)
                  y = natVal (Proxy @ b)
                  z = case x of
@@ -193,6 +177,5 @@ instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where
 
 -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.-'
 instance (KnownNat a, KnownNat b, b <= a) => KnownNat2 $(nameToSymbol ''(-)) a b where
-  type KnownNatF2 $(nameToSymbol ''(-)) = (:-$)
   natSing2 = SNatKn (natVal (Proxy @a) - natVal (Proxy @b))
   {-# INLINE natSing2 #-}

src/GHC/TypeLits/KnownNat/Solver.hs

@@ -51,15 +51,12 @@ And, given the type family @Max@:
 type family Max (a :: Nat) (b :: Nat) :: Nat where
   Max 0 b = b
   Max a b = If (a <=? b) b a
-
-$(genDefunSymbols [''Max]) -- creates the 'MaxSym0' symbol
 @
 
 and corresponding @KnownNat2@ instance:
 
 @
 instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where
-  type KnownNatF2 \"TestFunctions.Max\" = MaxSym0
   natSing2 = let x = natVal (Proxy @ a)
                  y = natVal (Proxy @ b)
                  z = max x y

tests/TestFunctions.hs

@@ -6,7 +6,6 @@
 module TestFunctions where
 
 import Data.Proxy            (Proxy (..))
-import Data.Singletons.TH    (genDefunSymbols)
 import Data.Type.Bool        (If)
 import GHC.TypeLits.KnownNat
 #if __GLASGOW_HASKELL__ >= 802
@@ -20,10 +19,7 @@ type family Max (a :: Nat) (b :: Nat) :: Nat where
   Max 0 b = b -- See [Note: single equation TFs are treated like synonyms]
   Max a b = If (a <=? b) b a
 
-genDefunSymbols [''Max]
-
 instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where
-  type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0
   natSing2 = let x = natVal (Proxy @ a)
                  y = natVal (Proxy @ b)
                  z = max x y
@@ -56,8 +52,6 @@ withNat n f = case someNatVal n of
 
 type family Log (n :: Nat) :: Nat where
 
-genDefunSymbols [''Log]
-
 #if __GLASGOW_HASKELL__ >= 802
 logInt :: Natural -> Natural
 #else
@@ -72,6 +66,5 @@ logInt n = go 0
              GT -> k - 1
 
 instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where
-  type KnownNatF1 $(nameToSymbol ''Log) = LogSym0
   natSing1 = let x = natVal (Proxy @ a)
              in SNatKn (logInt x)