ghc-typelits-natnormalise 0.4 → 0.4.1
raw patch · 4 files changed
+29/−4 lines, 4 files
Files
- CHANGELOG.md +4/−0
- README.md +1/−1
- ghc-typelits-natnormalise.cabal +1/−1
- src/GHC/TypeLits/Normalise.hs +23/−2
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.4.1 *February 4th 2016*+* Find more unifications:+ * `F x y k z ~ F x y (k-1+1) z` ==> [k := k], where `F` can be any type function+ ## 0.4 *January 19th 2016* * Stop using 'provenance' hack to create conditional evidence (GHC 8.0+ only) * Find more unifications:
README.md view
@@ -1,4 +1,4 @@-# ghc-tynat-normalise+# ghc-typelits-natnormalise [](http://travis-ci.org/clash-lang/ghc-typelits-natnormalise) [](https://hackage.haskell.org/package/ghc-typelits-natnormalise)
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.4+version: 0.4.1 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.hs view
@@ -55,6 +55,7 @@ -- external import Data.IORef (IORef, newIORef,readIORef, modifyIORef)+import Data.List (intersect) import Data.Maybe (catMaybes, mapMaybe) import GHC.TcPluginM.Extra (evByFiat, newGiven, tracePlugin) @@ -81,6 +82,13 @@ import TcType (mkEqPred, typeKind) import GHC.TcPluginM.Extra (newWantedWithProvenance, failWithProvenace) #endif+#if __GLASGOW_HASKELL__ >= 711+import TyCoRep (Type (..))+#else+import TypeRep (Type (..))+#endif+import TcTypeNats (typeNatAddTyCon, typeNatExpTyCon, typeNatMulTyCon,+ typeNatSubTyCon) -- internal@@ -250,10 +258,23 @@ toNatEquality :: Ct -> Maybe NatEquality toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2- | isNatKind (typeKind t1) || isNatKind (typeKind t1)- -> Just (ct,normaliseNat t1,normaliseNat t2)+ -> go t1 t2 _ -> Nothing where+ go (TyConApp tc xs) (TyConApp tc' ys)+ | tc == tc'+ , null ([tc,tc'] `intersect` [typeNatAddTyCon,typeNatSubTyCon+ ,typeNatMulTyCon,typeNatExpTyCon])+ = case filter (uncurry (/=)) (zip xs ys) of+ [(x,y)] | isNatKind (typeKind x) && isNatKind (typeKind y)+ -> Just (ct, normaliseNat x, normaliseNat y)+ _ -> Nothing+ go x y+ | isNatKind (typeKind x) && isNatKind (typeKind y)+ = Just (ct,normaliseNat x,normaliseNat y)+ | otherwise+ = Nothing+ isNatKind :: Kind -> Bool isNatKind = (== typeNatKind)