ghc-typelits-knownnat 0.5 → 0.5.1
raw patch · 5 files changed
+35/−37 lines, 5 filesdep ~ghcdep ~template-haskellPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc, template-haskell
API changes (from Hackage documentation)
Files
- CHANGELOG.md +3/−0
- ghc-typelits-knownnat.cabal +4/−4
- src/GHC/TypeLits/KnownNat.hs +3/−0
- src/GHC/TypeLits/KnownNat/Solver.hs +20/−31
- tests/Main.hs +5/−2
CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.5.1 *July 10th 2018*+* Add support for GHC 8.6.1-alpha1+ ## 0.5 *May 9th 2018* * Fix Inferred constraint is too strong [#19](https://github.com/clash-lang/ghc-typelits-knownnat/issues/19)
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.5+version: 0.5.1 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -54,7 +54,7 @@ CHANGELOG.md cabal-version: >=1.10 tested-with: GHC==8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2,- GHC == 8.5.0+ GHC == 8.6 source-repository head type: git@@ -86,11 +86,11 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5,- ghc >= 8.0.1 && <8.6,+ ghc >= 8.0.1 && <8.8, ghc-tcplugins-extra >= 0.3, ghc-typelits-natnormalise >= 0.6 && <0.7, transformers >= 0.5.2.0 && <0.6,- template-haskell >= 2.11.0.0 && <2.14+ template-haskell >= 2.11.0.0 && <2.15 hs-source-dirs: src default-language: Haskell2010 if flag(deverror)
src/GHC/TypeLits/KnownNat.hs view
@@ -93,6 +93,9 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-}+#if MIN_VERSION_ghc(8,6,0)+{-# LANGUAGE NoStarIsType #-}+#endif {-# LANGUAGE Trustworthy #-}
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -121,6 +121,9 @@ import Name (nameModule_maybe, nameOccName) import OccName (mkTcOcc, occNameString) import Plugins (Plugin (..), defaultPlugin)+#if MIN_VERSION_ghc(8,6,0)+import Plugins (purePlugin)+#endif import PrelNames (knownNatClassName) #if MIN_VERSION_ghc(8,5,0) import TcEvidence (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)@@ -242,7 +245,13 @@ -} plugin :: Plugin-plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin }+plugin+ = defaultPlugin+ { tcPlugin = const $ Just normalisePlugin+#if MIN_VERSION_ghc(8,6,0)+ , pluginRecompile = purePlugin+#endif+ } normalisePlugin :: TcPlugin normalisePlugin = tracePlugin "ghc-typelits-knownnat"@@ -277,11 +286,7 @@ -- Try to solve the wanted KnownNat constraints given the [G]iven -- KnownNat constraints (solved,new) <- (unzip . catMaybes) <$> (mapM (constraintToEvTerm defs given_map) kn_wanteds)-#if MIN_VERSION_ghc(8,5,0)- return (TcPluginOk (map (first EvExpr) solved) (concat new))-#else return (TcPluginOk solved (concat new))-#endif -- | Get the KnownNat constraints toKnConstraint :: Ct -> Maybe KnConstraint@@ -331,17 +336,13 @@ :: KnownNatDefs -- ^ The "magic" KnownNatN classes #if MIN_VERSION_ghc(8,5,0) -> [(CType,EvExpr)]- -- All the [G]iven constraints #else -> [(CType,EvTerm)]- -- All the [G]iven constraints #endif+ -- All the [G]iven constraints+ -> KnConstraint-#if MIN_VERSION_ghc(8,5,0)- -> TcPluginM (Maybe ((EvExpr,Ct),[Ct]))-#else -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))-#endif constraintToEvTerm defs givens (ct,cls,op) = do -- 1. Determine if we are an offset apart from a [G]iven constraint offsetM <- offset op@@ -356,11 +357,7 @@ -- Determine whether the outer type-level operation has a corresponding -- KnownNat<N> instance, where /N/ corresponds to the arity of the -- type-level operation-#if MIN_VERSION_ghc(8,5,0)- go :: Type -> TcPluginM (Maybe (EvExpr,[Ct]))-#else go :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))-#endif go (go_other -> Just ev) = return (Just (ev,[])) go ty@(TyConApp tc args) | let tcNm = tyConName tc@@ -411,26 +408,22 @@ -- Fall through case: look up the normalised [W]anted constraint in the list -- of [G]iven constraints.-#if MIN_VERSION_ghc(8,5,0)- go_other :: Type -> Maybe EvExpr-#else go_other :: Type -> Maybe EvTerm-#endif go_other ty = let knClsTc = classTyCon cls kn = mkTyConApp knClsTc [ty] cast = if CType ty == CType op+#if MIN_VERSION_ghc(8,6,0)+ then Just . EvExpr+#else then Just+#endif else makeKnCoercion cls ty op in cast =<< lookup (CType kn) givens -- Find a known constraint for a wanted, so that (modulo normalization) -- the two are a constant offset apart.-#if MIN_VERSION_ghc(8,5,0)- offset :: Type -> TcPluginM (Maybe (EvExpr,[Ct]))-#else offset :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))-#endif offset want = runMaybeT $ do let -- Get the knownnat contraints unKn ty' = case classifyPredType ty' of@@ -519,13 +512,11 @@ -> Type -- ^ Type of the result #if MIN_VERSION_ghc(8,5,0) -> [EvExpr]- -- ^ Evidence arguments- -> Maybe EvExpr #else -> [EvTerm]+#endif -- ^ Evidence arguments -> Maybe EvTerm-#endif makeOpDict (opCls,dfid) knCls tyArgs z evArgs | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] -- KnownNat n ~ SNat n@@ -546,7 +537,7 @@ , Just (_, op_co_rep) <- tcInstNewTyCon_maybe op_tcRep op_args -- SNatKn (a+b) ~ Integer #if MIN_VERSION_ghc(8,5,0)- , let dfun_inst = evDFunApp dfid (tail tyArgs) evArgs+ , let EvExpr dfun_inst = evDFunApp dfid (tail tyArgs) evArgs #else , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs #endif@@ -577,13 +568,11 @@ -> Type -- ^ Type of the result #if MIN_VERSION_ghc(8,5,0) -> EvExpr- -- ^ KnownNat dictionary for the argument- -> Maybe EvExpr #else -> EvTerm+#endif -- ^ KnownNat dictionary for the argument -> Maybe EvTerm-#endif makeKnCoercion knCls x z xEv | Just (_, kn_co_dict_z) <- tcInstNewTyCon_maybe (classTyCon knCls) [z] -- KnownNat z ~ SNat z@@ -611,7 +600,7 @@ -- Integer -> SNat n -- representation of literal to singleton -- SNat n -> KnownNat n -- singleton to dictionary #if MIN_VERSION_ghc(8,5,0)-makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvExpr)+makeLitDict :: Class -> Type -> Integer -> TcPluginM (Maybe EvTerm) #else makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm #endif
tests/Main.hs view
@@ -1,6 +1,8 @@ {-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, ScopedTypeVariables, TypeOperators, TypeApplications, TypeFamilies, TypeFamilyDependencies, FlexibleContexts #-}-+#if __GLASGOW_HASKELL__ >= 805+{-# LANGUAGE NoStarIsType #-}+#endif {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-} #if __GLASGOW_HASKELL__ >= 802@@ -9,6 +11,7 @@ module Main where +import Data.Kind (Type) import Data.Proxy import Data.Type.Equality ((:~:)(..)) #if __GLASGOW_HASKELL__ >= 802@@ -126,7 +129,7 @@ test17 :: KnownNat (4 + 2 * Foo 1 + Foo 1) => Proxy (Foo 1) -> Proxy (4 + 2 * Foo 1 + Foo 1) -> Number test17 _ _ = natVal (Proxy @ (2 * Foo 1 + 7 + Foo 1)) -data SNat :: Nat -> * where+data SNat :: Nat -> Type where SNat :: KnownNat n => SNat n instance Show (SNat n) where