Reduce inside arithmetic equations

clash-lang · Mar 9, 2020 · 9e7eb8a · 9e7eb8a
1 parent ae29109
commit 9e7eb8a
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 1 deletion.
diff --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs
@@ -76,7 +76,7 @@ normaliseNat defs (TyConApp tc tys) = do
   tyM    <- lift (matchFam tc tys')
   case tyM of
     Just (_,ty) -> normaliseNat defs ty
-    _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys)))
+    _ -> let q = fst (runWriter (Normalise.normaliseNat (TyConApp tc tys')))
          in  return (C (CType (Normalise.reifySOP q)))
 
 normaliseNat _ t = return (C (CType t))

diff --git a/tests/Main.hs b/tests/Main.hs
@@ -183,6 +183,14 @@ test51
   -> Proxy (2+((2^n)*2))
 test51 _ = id
 
+type family BitPack a :: Nat
+
+test52
+  :: Proxy a
+  -> Proxy (1 + BitPack a)
+  -> Proxy (Max 0 (BitPack a) + CLog 2 2)
+test52 _ = id
+
 main :: IO ()
 main = defaultMain tests
 
@@ -342,6 +350,9 @@ tests = testGroup "ghc-typelits-natnormalise"
     , testCase "forall n . Max (((2 ^ n) + 1) + ((2 ^ n) + 1)) 1 ~ 2 + ((2 ^ n) * 2)" $
       show (test51 Proxy Proxy) @?=
       "Proxy"
+    , testCase "forall a . (1 + BitPack a) ~ (Max 0 (BitPack a) + CLog 2 2" $
+      show (test52 Proxy Proxy) @?=
+      "Proxy"
     ]
   , testGroup "errors"
     [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors