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.7.2 *February 6th 2020* + * Add support for GHC 8.10.0-alpha2 + ## 0.7.1 *October 8th 2019* * Fix [#29](https://github.com/clash-lang/ghc-typelits-knownnat/issues/29) * Fix [#30](https://github.com/clash-lang/ghc-typelits-knownnat/issues/30) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -58,8 +58,8 @@ ```haskell instance (KnownNat a, KnownNat b) => KnownNat2 "TestFunctions.Max" a b where - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = max x y in SNatKn z {-# INLINE natSing2 #-} 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.7.1 +version: 0.7.2 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@ @@ -86,12 +86,12 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5, - ghc >= 8.0.1 && <8.9, - ghc-prim >= 0.4.0.0 && <0.6, - ghc-tcplugins-extra >= 0.3, - ghc-typelits-natnormalise >= 0.6 && <0.8, + ghc >= 8.0.1 && <8.11, + ghc-prim >= 0.4.0.0 && <0.7, + ghc-tcplugins-extra >= 0.3.1, + ghc-typelits-natnormalise >= 0.7.1 && <0.8, transformers >= 0.5.2.0 && <0.6, - template-haskell >= 2.11.0.0 && <2.16 + template-haskell >= 2.11.0.0 && <2.17 hs-source-dirs: src default-language: Haskell2010 if flag(deverror) @@ -105,7 +105,7 @@ Other-Modules: TestFunctions build-depends: base >= 4.8 && <5, ghc-typelits-knownnat, - ghc-typelits-natnormalise >= 0.6 && <0.8, + ghc-typelits-natnormalise >= 0.7.1 && <0.8, tasty >= 0.10, tasty-hunit >= 0.9, tasty-quickcheck >= 0.8 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 @@ -191,8 +191,8 @@ -- | 'KnownNat2' instance for "GHC.TypeLits"' 'GHC.TypeLits.^' instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''(^)) a b where - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = case x of 2 -> shiftL 1 (fromIntegral y) _ -> x ^ y @@ -236,7 +236,7 @@ -- -- @ -- f :: forall proxy b r . KnownBool b => r --- f = case boolSing @ b of +-- f = case boolSing @b of -- SFalse -> -- context with b ~ False -- STrue -> -- context with b ~ True -- @ diff --git a/src/GHC/TypeLits/KnownNat/Solver.hs b/src/GHC/TypeLits/KnownNat/Solver.hs --- a/src/GHC/TypeLits/KnownNat/Solver.hs +++ b/src/GHC/TypeLits/KnownNat/Solver.hs @@ -59,8 +59,8 @@ @ instance (KnownNat a, KnownNat b) => KnownNat2 \"TestFunctions.Max\" a b where - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = max x y in SNatKn z \{\-# INLINE natSing2 \#-\} @@ -142,19 +142,13 @@ import TcPluginM (zonkCt) #endif import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs) -import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc, -#if MIN_VERSION_ghc(8,5,0) - ctEvPred, ctEvExpr, ctLoc, ctLocSpan, isWanted, -#else - ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted, -#endif - mkNonCanonical, setCtLoc, setCtLocSpan) +import TcRnTypes (TcPlugin(..), TcPluginResult (..)) import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon) #if MIN_VERSION_ghc(8,4,0) import TcTypeNats (typeNatDivTyCon) #endif import Type - (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType, + (PredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe, typeKind) import TyCon (tyConName) @@ -164,6 +158,23 @@ import TysWiredIn (boolTy) #endif import Var (DFunId) + +#if MIN_VERSION_ghc(8,10,0) +import Constraint + (Ct, ctEvExpr, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, + mkNonCanonical, setCtLoc, setCtLocSpan) +import Predicate (EqRel (NomEq), Pred (ClassPred,EqPred), classifyPredType) +#else +import TcRnTypes + (Ct, ctEvidence, ctEvLoc, ctEvPred, ctLoc, ctLocSpan, isWanted, mkNonCanonical, + setCtLoc, setCtLocSpan) +import Type (EqRel (NomEq), PredTree (ClassPred,EqPred), classifyPredType) +#if MIN_VERSION_ghc(8,5,0) +import TcRnTypes (ctEvExpr) +#else +import TcRnTypes (ctEvTerm) +#endif +#endif -- | Classes and instances from "GHC.TypeLits.KnownNat" data KnownNatDefs diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -109,7 +109,7 @@ test10 _ _ = natVal (Proxy :: Proxy (m-n+n)) test11 :: forall m . (KnownNat m) => Proxy m -> Number -test11 _ = natVal (Proxy @ (m*m)) +test11 _ = natVal (Proxy @(m*m)) test12 :: forall m . (KnownNat (m+1)) => Proxy m -> Number test12 = natVal @@ -125,13 +125,13 @@ fakeFooEvidence = unsafeCoerce Refl test15 :: KnownNat (4 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + Foo 1) -> Number -test15 _ _ = natVal (Proxy @ (Foo 1 + 7)) +test15 _ _ = natVal (Proxy @(Foo 1 + 7)) 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)) +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) -> Number -test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1)) +test17 _ _ = natVal (Proxy @(2 * Foo 1 + 7 + Foo 1)) data SNat :: Nat -> Type where SNat :: KnownNat n => SNat n @@ -158,7 +158,7 @@ test19 = subSNat test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Number -test20 _ = natVal (Proxy @ (2 * a)) +test20 _ = natVal (Proxy @(2 * a)) test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Number test21 _ _ = natVal (Proxy :: Proxy n) @@ -192,34 +192,34 @@ tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality" [ testCase "KnownNat 4 + KnownNat 6 ~ 10" $ - show (test1 (Proxy @ 4)) @?= + show (test1 (Proxy @4)) @?= "10" , testCase "KnownNat 4 * KnownNat 3 ~ 12" $ - show (test2 (Proxy @ 4)) @?= + show (test2 (Proxy @4)) @?= "12" , testCase "KnownNat 2 + KnownNat 7 ~ 9" $ - show (test3 (Proxy @ 2) (Proxy @ 7)) @?= + show (test3 (Proxy @2) (Proxy @7)) @?= "9" , testCase "KnownNat 2 * KnownNat 7 ~ 14" $ - show (test4 (Proxy @ 2) (Proxy @ 7)) @?= + show (test4 (Proxy @2) (Proxy @7)) @?= "14" , testCase "KnownNat 2 ^ KnownNat 7 ~ 128" $ - show (test5 (Proxy @ 2) (Proxy @ 7)) @?= + show (test5 (Proxy @2) (Proxy @7)) @?= "128" , testCase "KnownNat 3 ^ KnownNat 7 ~ 2187" $ - show (test5 (Proxy @ 3) (Proxy @ 7)) @?= + show (test5 (Proxy @3) (Proxy @7)) @?= "2187" , testCase "(KnownNat 2 ^ KnownNat 7) + (KnownNat 2 * KnownNat 7) ~ 142" $ - show (test6 (Proxy @ 2) (Proxy @ 7)) @?= + show (test6 (Proxy @2) (Proxy @7)) @?= "142" , testCase "KnownNat (Max 7 5 + 1) ~ 8" $ - show (test7 (Proxy @ 7) (Proxy @ 5)) @?= + show (test7 (Proxy @7) (Proxy @5)) @?= "8" , testCase "KnownNat (Min 7 5 + 1) ~ 6" $ - show (test8 (Proxy @ 7) (Proxy @ 5)) @?= + show (test8 (Proxy @7) (Proxy @5)) @?= "6" , testCase "KnownNat (7 - 5) ~ 2" $ - show (test9 (Proxy @ 7) (Proxy @ 5)) @?= + show (test9 (Proxy @7) (Proxy @5)) @?= "2" , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $ show (test22 (Proxy @3) (Proxy @4))@?= @@ -231,52 +231,52 @@ #endif ], testGroup "Implications" - [ testCase "KnownNat m => KnownNat (m*m); @ 5" $ - show (test11 (Proxy @ 5)) @?= + [ testCase "KnownNat m => KnownNat (m*m); @5" $ + show (test11 (Proxy @5)) @?= "25" - , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 5" $ - show (test12 (Proxy @ 5)) @?= + , testCase "KnownNat (m+1) => KnownNat m; @m ~ 5" $ + show (test12 (Proxy @5)) @?= "5" - , testCase "KnownNat (m+1) => KnownNat m; @ m ~ 0" $ - show (test12 (Proxy @ 0)) @?= + , testCase "KnownNat (m+1) => KnownNat m; @m ~ 0" $ + show (test12 (Proxy @0)) @?= "0" - , testCase "KnownNat (m+3) => KnownNat m; @ m ~ 0" $ - show (test13 (Proxy @ 0)) @?= + , testCase "KnownNat (m+3) => KnownNat m; @m ~ 0" $ + show (test13 (Proxy @0)) @?= "0" - , testCase "KnownNat (4+m) => KnownNat (7+m); @ m ~ 1" $ - show (test14 (Proxy @ 8)) @?= + , testCase "KnownNat (4+m) => KnownNat (7+m); @m ~ 1" $ + show (test14 (Proxy @8)) @?= "8" - , testCase "KnownNat (4 + Foo 1) => KnownNat (Foo 1 + 7); @ Foo 1 ~ 1" $ + , testCase "KnownNat (4 + Foo 1) => KnownNat (Foo 1 + 7); @Foo 1 ~ 1" $ (case fakeFooEvidence of - Refl -> show $ test15 (Proxy @ (Foo 1)) (Proxy @ (4 + Foo 1))) @?= + Refl -> show $ test15 (Proxy @(Foo 1)) (Proxy @(4 + Foo 1))) @?= "8" - , testCase "KnownNat (4 + Foo 1 + Foo 1) => KnownNat (Foo 1 + 7 + Foo 1); @ Foo 1 ~ 1" $ + , testCase "KnownNat (4 + Foo 1 + Foo 1) => KnownNat (Foo 1 + 7 + Foo 1); @Foo 1 ~ 1" $ (case fakeFooEvidence of - Refl -> show $ test16 (Proxy @ (Foo 1)) (Proxy @ (4 + Foo 1 + Foo 1))) @?= + Refl -> show $ test16 (Proxy @(Foo 1)) (Proxy @(4 + Foo 1 + Foo 1))) @?= "9" - , testCase "KnownNat (4 + 2 * Foo 1 + Foo 1) => KnownNat (2 * Foo 1 + 7 + Foo 1); @ Foo 1 ~ 1" $ + , testCase "KnownNat (4 + 2 * Foo 1 + Foo 1) => KnownNat (2 * Foo 1 + 7 + Foo 1); @Foo 1 ~ 1" $ (case fakeFooEvidence of - Refl -> show $ test17 (Proxy @ (Foo 1)) (Proxy @ (4 + 2 * Foo 1 + Foo 1))) @?= + Refl -> show $ test17 (Proxy @(Foo 1)) (Proxy @(4 + 2 * Foo 1 + Foo 1))) @?= "10" - , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @ a ~ 4" $ - show (test20 (Proxy @ 4)) @?= + , testCase "KnownNat (3 * a - a) => KnownNat (2 * a); @a ~ 4" $ + show (test20 (Proxy @4)) @?= "8" - , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @ (a+b) ~ 8, b ~ 6" $ - show (test21 (Proxy @ 8) (Proxy @ 6)) @?= + , testCase "KnownNat (a + b), KnownNat b => KnownNat a; @(a+b) ~ 8, b ~ 6" $ + show (test21 (Proxy @8) (Proxy @6)) @?= "2" ], testGroup "Normalisation" [ testCase "KnownNat (m-n+n) ~ KnownNat m" $ - show (test10 (Proxy @ 12) (Proxy @8)) @?= + show (test10 (Proxy @12) (Proxy @8)) @?= "12" , testCase "SNat (a+1) - SNat a = SNat 1" $ - show (test18 (SNat @ 11) (SNat @10)) @?= + show (test18 (SNat @11) (SNat @10)) @?= "1" , testCase "SNat (a+b) - SNat b = SNat a" $ - show (test19 (SNat @ 16) (SNat @10)) @?= + show (test19 (SNat @16) (SNat @10)) @?= "6" , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $ - show (test23 (SNat @ 8)) @?= + show (test23 (SNat @8)) @?= "2" , testCase "(KnownNat n, n ~ m + 1) ~ KnownNat m" $ show (test24 (Proxy @4)) @?= diff --git a/tests/TestFunctions.hs b/tests/TestFunctions.hs --- a/tests/TestFunctions.hs +++ b/tests/TestFunctions.hs @@ -20,8 +20,8 @@ Max a b = If (a <=? b) b a instance (KnownNat a, KnownNat b) => KnownNat2 $(nameToSymbol ''Max) a b where - natSing2 = let x = natVal (Proxy @ a) - y = natVal (Proxy @ b) + natSing2 = let x = natVal (Proxy @a) + y = natVal (Proxy @b) z = max x y in SNatKn z {-# INLINE natSing2 #-} @@ -66,5 +66,5 @@ GT -> k - 1 instance (KnownNat a) => KnownNat1 $(nameToSymbol ''Log) a where - natSing1 = let x = natVal (Proxy @ a) + natSing1 = let x = natVal (Proxy @a) in SNatKn (logInt x)