ghc-typelits-knownnat 0.7.1 → 0.7.2

raw patch · 7 files changed

+78/−64 lines, 7 filesdep ~ghcdep ~ghc-primdep ~ghc-tcplugins-extraPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc, ghc-prim, ghc-tcplugins-extra, ghc-typelits-natnormalise, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• README.md +2/−2
• ghc-typelits-knownnat.cabal +7/−7
• src/GHC/TypeLits/KnownNat.hs +3/−3
• src/GHC/TypeLits/KnownNat/Solver.hs +21/−10
• tests/Main.hs +39/−39
• tests/TestFunctions.hs +3/−3

@@ -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)

@@ -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 #-}

@@ -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

@@ -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 -- @

@@ -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

@@ -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)) @?=

@@ -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)