ghc-typelits-knownnat 0.2.1 → 0.2.2

raw patch · 4 files changed

+17/−5 lines, 4 files

Files

• CHANGELOG.md +4/−0
• ghc-typelits-knownnat.cabal +1/−1
• src/GHC/TypeLits/KnownNat/Solver.hs +6/−4
• tests/Main.hs +6/−0

@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.2.2 *September 29th 2016*+* New features:+  * Derive smaller constraints from larger constraints when they differ by a single variable, i.e. `KnownNat (a + b), KnownNat b` implies `KnownNat a`.+ ## 0.2.1 *August 19th 2016* * Fixes bugs:   * Source location of derived wanted constraints is, erroneously, always set to line 1, column 1

@@ -1,5 +1,5 @@ name:                ghc-typelits-knownnat-version:             0.2.1+version:             0.2.2 synopsis:            Derive KnownNat constraints from other KnownNat constraints description:   A type checker plugin for GHC that can derive \"complex\" @KnownNat@

@@ -374,15 +374,17 @@           exploded = map (normaliseNat . subWant &&& id) knowns           -- interesting cases for us are those where           -- wanted and given only differ by a constant-          examineDiff (S [P [I n]]) entire  = Just (entire,n)+          examineDiff (S [P [I n]]) entire = Just (entire,I n)+          examineDiff (S [P [V v]]) entire = Just (entire,V v)           examineDiff _ _ = Nothing           interesting = mapMaybe (uncurry examineDiff) exploded       -- convert the first suitable evidence       ((h,corr):_) <- pure interesting       let x = case corr of-                0 -> h-                _ | corr < 0  -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate corr)]-                  | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy corr]+                I 0 -> h+                I i | i < 0     -> mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)]+                    | otherwise -> mkTyConApp typeNatSubTyCon [h,mkNumLitTy i]+                _ -> mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]       MaybeT (go x)  {- |

@@ -97,6 +97,9 @@ test20 :: forall a . (KnownNat (3 * a - a)) => Proxy a -> Integer test20 _ = natVal (Proxy @ (2 * a)) +test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer+test21 _ _ = natVal (Proxy :: Proxy n)+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise"   [ testGroup "Basic functionality"@@ -162,6 +165,9 @@     , 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)) @?=+      "2"     ],     testGroup "Normalisation"     [ testCase "KnownNat (m-n+n) ~ KnownNat m" $