ghc-typelits-knownnat 0.7 → 0.7.1
raw patch · 4 files changed
+42/−8 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.md +4/−0
- ghc-typelits-knownnat.cabal +2/−2
- src/GHC/TypeLits/KnownNat/Solver.hs +26/−6
- tests/Main.hs +10/−0
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 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)+ ## 0.7 *August 26th 2018* * Solve "known" type-level Booleans, also inside `If` (GHC 8.6+)
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.7+version: 0.7.1 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -91,7 +91,7 @@ ghc-tcplugins-extra >= 0.3, ghc-typelits-natnormalise >= 0.6 && <0.8, transformers >= 0.5.2.0 && <0.6,- template-haskell >= 2.11.0.0 && <2.15+ template-haskell >= 2.11.0.0 && <2.16 hs-source-dirs: src default-language: Haskell2010 if flag(deverror)
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -150,6 +150,9 @@ #endif mkNonCanonical, setCtLoc, setCtLocSpan) import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon)+#if MIN_VERSION_ghc(8,4,0)+import TcTypeNats (typeNatDivTyCon)+#endif import Type (EqRel (NomEq), PredTree (ClassPred,EqPred), PredType, classifyPredType, dropForAlls, eqType, funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp,@@ -491,11 +494,12 @@ knowns = mapMaybe (unKn . unCType . fst) givens -- Get all the rewritten KNs knownsR = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns+ knownsX = knowns ++ knownsR -- pair up the sum-of-products KnownNat constraints -- with the original Nat operation subWant = mkTyConApp typeNatSubTyCon . (:[want]) exploded = map (fst . runWriter . normaliseNat . subWant &&& id)- (knowns ++ knownsR)+ knownsX -- interesting cases for us are those where -- wanted and given only differ by a constant examineDiff (S [P [I n]]) entire = Just (entire,I n)@@ -504,11 +508,27 @@ interesting = mapMaybe (uncurry examineDiff) exploded -- convert the first suitable evidence ((h,corr):_) <- pure interesting- let x = case corr of- 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]])]+ x <- case corr of+ I 0 -> pure h+ I i | i < 0+ -> pure (mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)])+ | otherwise+ -> pure (mkTyConApp typeNatSubTyCon [h,mkNumLitTy i])+ -- If the offset between a given and a wanted is again the wanted+ -- then the given is twice the wanted; so we can just divide+ -- the given by two. Only possible in GHC 8.4+; for 8.2 we simply+ -- fail because we don't know how to divide.+ c | CType (reifySOP (S [P [c]])) == CType want ->+#if MIN_VERSION_ghc(8,4,0)+ pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])])+#else+ MaybeT (pure Nothing)+#endif+ -- Only solve with a variable offset if we have [G]iven knownnat for it+ -- Failing to do this check results in #30+ V v | all (not . eqType (TyVarTy v)) knownsX+ -> MaybeT (pure Nothing)+ _ -> pure (mkTyConApp typeNatSubTyCon [h,reifySOP (S [P [corr]])]) MaybeT (go x) makeWantedEv
tests/Main.hs view
@@ -183,6 +183,11 @@ test27 _ _ = natVal (Proxy :: Proxy (If (n <=? m) n m)) #endif +#if __GLASGOW_HASKELL__ >= 804+test28 :: forall m n . (KnownNat m, (2*n) ~ m) => Proxy m -> Natural+test28 _ = natVal @n Proxy+#endif+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality"@@ -219,6 +224,11 @@ , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $ show (test22 (Proxy @3) (Proxy @4))@?= "48"+#if __GLASGOW_HASKELL__ >= 804+ , testCase "KnownNat m, 2 * n ~ m, m = 10 ~ 5" $+ show (test28 (Proxy @10)) @?=+ "5"+#endif ], testGroup "Implications" [ testCase "KnownNat m => KnownNat (m*m); @ 5" $