diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.3 *May 15th 2017* +* GHC 8.2.1 support: Underlying representation for `KnownNat` in GHC 8.2 is `Natural`, meaning users of this plugin will need to update their code to use `Natural` for GHC 8.2 as well. + ## 0.2.4 *April 10th 2017* * New features: * Derive constraints for unary functions via a `KnownNat1` instance; thanks to @nshepperd [#11](https://github.com/clash-lang/ghc-typelits-knownnat/pull/11) diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-knownnat -version: 0.2.4 +version: 0.3 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ @@ -81,8 +81,8 @@ TypeInType UndecidableInstances ViewPatterns - build-depends: base >= 4.9 && <4.10, - ghc >= 8.0.1 && <8.2, + build-depends: base >= 4.9 && <5, + ghc >= 8.0.1 && <8.4, ghc-tcplugins-extra >= 0.2, ghc-typelits-natnormalise >= 0.5.2 && <0.6, singletons >= 2.2 && <3.0, diff --git a/src/GHC/TypeLits/KnownNat.hs b/src/GHC/TypeLits/KnownNat.hs --- a/src/GHC/TypeLits/KnownNat.hs +++ b/src/GHC/TypeLits/KnownNat.hs @@ -85,6 +85,7 @@ -} {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE KindSignatures #-} @@ -116,15 +117,29 @@ import Data.Bits (shiftL) import Data.Proxy (Proxy (..)) +#if MIN_VERSION_ghc(8,2,0) +import GHC.TypeNats + (KnownNat, Nat, type (+), type (*), type (^), type (-), type (<=), natVal) +import GHC.TypeLits (Symbol) +#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 (represented by an integer) -newtype SNatKn (n :: Nat) = SNatKn Integer +-- | Singleton natural number +newtype SNatKn (n :: Nat) = +#if MIN_VERSION_ghc(8,2,0) + SNatKn Natural +#else + SNatKn Integer +#endif -- | Class for arithmetic functions with /one/ argument. -- @@ -171,7 +186,7 @@ natSing2 = let x = natVal (Proxy @ a) y = natVal (Proxy @ b) z = case x of - 2 -> shiftL 1 (fromInteger y) + 2 -> shiftL 1 (fromIntegral y) _ -> x ^ y in SNatKn z {-# INLINE natSing2 #-} diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, +{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -8,7 +8,12 @@ import Data.Proxy import Data.Type.Equality ((:~:)(..)) +#if __GLASGOW_HASKELL__ >= 802 +import GHC.TypeNats +import Numeric.Natural +#else import GHC.TypeLits +#endif import Test.Tasty import Test.Tasty.HUnit import Test.Tasty.QuickCheck @@ -16,14 +21,20 @@ import TestFunctions -addT :: Integer -> Integer -> Integer +#if __GLASGOW_HASKELL__ >= 802 +type Number = Natural +#else +type Number = Integer +#endif + +addT :: Number -> Number -> Number addT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (a + b)) -subT :: Integer -> Integer -> Integer +subT :: Number -> Number -> Number subT a b | a >= b = withNat a $ \(Proxy :: Proxy a) -> @@ -34,77 +45,77 @@ natVal (Proxy :: Proxy (a - b)) | otherwise = error "a - b < 0" -mulT :: Integer -> Integer -> Integer +mulT :: Number -> Number -> Number mulT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (a * b)) -maxT :: Integer -> Integer -> Integer +maxT :: Number -> Number -> Number maxT a b = withNat a $ \(Proxy :: Proxy a) -> withNat b $ \(Proxy :: Proxy b) -> natVal (Proxy :: Proxy (Max a b)) -logT :: Integer -> Integer +logT :: Number -> Number logT n = withNat n $ \(Proxy :: Proxy n) -> natVal (Proxy :: Proxy (Log n)) -test1 :: forall n . KnownNat n => Proxy n -> Integer +test1 :: forall n . KnownNat n => Proxy n -> Number test1 _ = natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy (n+2)) -test2 :: forall n . KnownNat n => Proxy n -> Integer +test2 :: forall n . KnownNat n => Proxy n -> Number test2 _ = natVal (Proxy :: Proxy (n*3)) -test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test3 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test3 _ _ = natVal (Proxy :: Proxy (n+m)) -test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test4 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test4 _ _ = natVal (Proxy :: Proxy (n*m)) -test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test5 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test5 _ _ = natVal (Proxy :: Proxy (n^m)) -test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Integer +test6 :: forall n m . (KnownNat n, KnownNat m) => Proxy n -> Proxy m -> Number test6 _ _ = natVal (Proxy :: Proxy ((n^m)+(n*m))) -test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Integer +test7 :: forall n m . (KnownNat m, KnownNat n) => Proxy n -> Proxy m -> Number test7 _ _ = natVal (Proxy :: Proxy (Max n m + 1)) -test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Integer +test8 :: forall n m . (KnownNat (Min n m)) => Proxy n -> Proxy m -> Number test8 _ _ = natVal (Proxy :: Proxy (Min n m + 1)) -test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Integer +test9 :: forall n m . (KnownNat m, KnownNat n, n <= m) => Proxy m -> Proxy n -> Number test9 _ _ = natVal (Proxy :: Proxy (m-n)) -test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Integer +test10 :: forall (n :: Nat) m . (KnownNat m) => Proxy m -> Proxy n -> Number test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) -test11 :: forall m . (KnownNat m) => Proxy m -> Integer +test11 :: forall m . (KnownNat m) => Proxy m -> Number test11 _ = natVal (Proxy @ (m*m)) -test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Integer +test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number test12 = natVal -test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Integer +test13 :: forall m . (KnownNat (m+3)) => Proxy m -> Number test13 = natVal -test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Integer +test14 :: forall m . (KnownNat (4+m)) => Proxy (7+m) -> Number test14 = natVal type family Foo (m :: Nat) = (result :: Nat) | result -> m fakeFooEvidence :: 1 :~: Foo 1 fakeFooEvidence = unsafeCoerce Refl -test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Integer +test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Number test15 _ _ = natVal (Proxy @ (Foo 1 + 7)) -test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Integer +test16 :: KnownNat (4 + Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1 + Foo 1) -> Number test16 _ _ = natVal (Proxy @ (Foo 1 + 7 + Foo 1)) -test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Integer +test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Number test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1)) data SNat :: Nat -> * where @@ -131,19 +142,19 @@ test19 :: SNat (a+b) -> SNat b -> SNat a test19 = subSNat -test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Integer +test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Number test20 _ = natVal (Proxy @ (2 * a)) -test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer +test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Number test21 _ _ = natVal (Proxy :: Proxy n) -test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer +test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Number test22 _ _ = natVal (Proxy :: Proxy (y*x*y)) test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1)) test23 SNat = SNat -test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Integer +test24 :: (KnownNat n, n ~ (m+1)) => proxy m -> Number test24 = natVal tests :: TestTree diff --git a/tests/TestFunctions.hs b/tests/TestFunctions.hs --- a/tests/TestFunctions.hs +++ b/tests/TestFunctions.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds, FlexibleInstances, GADTs, KindSignatures, +{-# LANGUAGE CPP, DataKinds, FlexibleInstances, GADTs, KindSignatures, MultiParamTypeClasses, RankNTypes, ScopedTypeVariables, TemplateHaskell, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-} @@ -9,7 +9,12 @@ import Data.Singletons.TH (genDefunSymbols) import Data.Type.Bool (If) import GHC.TypeLits.KnownNat +#if __GLASGOW_HASKELL__ >= 802 +import GHC.TypeNats +import Numeric.Natural +#else import GHC.TypeLits +#endif type family Max (a :: Nat) (b :: Nat) :: Nat where Max 0 b = b -- See [Note: single equation TFs are treated like synonyms] @@ -38,17 +43,26 @@ Min a b = If (a <=? b) a b -- Unary functions. - +#if __GLASGOW_HASKELL__ >= 802 +withNat :: Natural -> (forall n. (KnownNat n) => Proxy n -> r) -> r +withNat n f = case someNatVal n of + SomeNat proxy -> f proxy +#else withNat :: Integer -> (forall n. (KnownNat n) => Proxy n -> r) -> r withNat n f = case someNatVal n of Just (SomeNat proxy) -> f proxy Nothing -> error ("withNat: negative value (" ++ show n ++ ")") +#endif type family Log (n :: Nat) :: Nat where genDefunSymbols [''Log] +#if __GLASGOW_HASKELL__ >= 802 +logInt :: Natural -> Natural +#else logInt :: Integer -> Integer +#endif logInt 0 = error "log 0" logInt n = go 0 where