ghc-typelits-natnormalise 0.5.5 → 0.5.6

raw patch · 4 files changed

+21/−3 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

CHANGELOG.md +4/−0
ghc-typelits-natnormalise.cabal +1/−1
src/GHC/TypeLits/Normalise/Unify.hs +2/−2
tests/Tests.hs +14/−0

CHANGELOG.md view

@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5.6 *October 31st 2017*+* Fixes bugs:+  * `(x + 1) ~ (2 * y)` no longer implies `((2 * (y - 1)) + 1) ~ x`+ ## 0.5.5 *October 22nd 2017* * Solve inequalities when their normal forms are the same, i.e.   * `(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`

ghc-typelits-natnormalise.cabal view

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.5.5+version:             0.5.6 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ of types of kind

src/GHC/TypeLits/Normalise/Unify.hs view

@@ -389,9 +389,9 @@  -- (a + c) ~ (b + c) ==> [a := b] unifiers' ct (S ps1)       (S ps2)-    | null psx  = case zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2 of+    | null psx  = case concat (zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2) of                     [] -> unifiers'' ct (S ps1) (S ps2)-                    ks -> nub (concat ks)+                    ks -> nub ks     | otherwise = unifiers' ct (S ps1'') (S ps2'')   where     ps1'  = ps1 \\ psx

tests/Tests.hs view

@@ -254,6 +254,15 @@ proxyEq2 :: Proxy (((2 ^ x) - 2) * (2 ^ (x + x))) -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1)))) proxyEq2 = id +proxyEq3+  :: forall x y+   . ((x + 1) ~ (2 * y))+  => Proxy x+  -> Proxy y+  -> Proxy (((2 * (y - 1)) + 1))+  -> Proxy x+proxyEq3 _ _ x = x+ proxyInEqImplication :: (2 <= (2 ^ (n + d)))   => Proxy d   -> Proxy n@@ -309,6 +318,11 @@       "Proxy"     , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $       show (proxyEq2 Proxy) @?=+      "Proxy"+    ]+  , testGroup "Implications"+    [ testCase "(x + 1) ~ (2 * y)) implies (((2 * (y - 1)) + 1)) ~ x" $+      show (proxyEq3 (Proxy :: Proxy 3) (Proxy :: Proxy 2) Proxy) @?=       "Proxy"     ]   , testGroup "Inequality"