ghc-typelits-knownnat 0.4.1 → 0.4.2
raw patch · 3 files changed
+107/−11 lines, 3 filesdep ~ghc-tcplugins-extradep ~ghc-typelits-natnormalisePVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc-tcplugins-extra, ghc-typelits-natnormalise
API changes (from Hackage documentation)
Files
- CHANGELOG.md +3/−0
- ghc-typelits-knownnat.cabal +6/−5
- src/GHC/TypeLits/KnownNat/Solver.hs +98/−6
CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.4.2 *April 15th 2018*+* Add support for GHC 8.5.20180306+ ## 0.4.1 *March 17th, 2018* * Add support for GHC 8.4.1
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.4.1+version: 0.4.2 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -53,7 +53,8 @@ extra-source-files: README.md CHANGELOG.md cabal-version: >=1.10-tested-with: GHC==8.0.2, GHC == 8.2.2, GHC == 8.4.1+tested-with: GHC==8.0.2, GHC == 8.2.2, GHC == 8.4.1, GHC == 8.4.2,+ GHC == 8.5.0 source-repository head type: git@@ -86,8 +87,8 @@ ViewPatterns build-depends: base >= 4.9 && <5, ghc >= 8.0.1 && <8.6,- ghc-tcplugins-extra >= 0.2.4,- ghc-typelits-natnormalise >= 0.5.2 && <0.6,+ ghc-tcplugins-extra >= 0.2.5,+ ghc-typelits-natnormalise >= 0.5.10 && <0.6, transformers >= 0.5.2.0 && <0.6, template-haskell >= 2.11.0.0 && <2.14 hs-source-dirs: src@@ -103,7 +104,7 @@ Other-Modules: TestFunctions build-depends: base >= 4.8 && <5, ghc-typelits-knownnat,- ghc-typelits-natnormalise >= 0.5.9 && <0.6,+ ghc-typelits-natnormalise >= 0.5.10 && <0.6, tasty >= 0.10, tasty-hunit >= 0.9, tasty-quickcheck >= 0.8
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -113,18 +113,32 @@ import FastString (fsLit) import Id (idType) import InstEnv (instanceDFunId,lookupUniqueInstEnv)+#if MIN_VERSION_ghc(8,5,0)+import MkCore (mkNaturalExpr)+#endif import Module (mkModuleName, moduleName, moduleNameString) import Name (nameModule_maybe, nameOccName) import OccName (mkTcOcc, occNameString) import Plugins (Plugin (..), defaultPlugin) import PrelNames (knownNatClassName)+#if MIN_VERSION_ghc(8,5,0)+import TcEvidence (EvTerm (..), EvExpr, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)+#else import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo)+#endif+#if MIN_VERSION_ghc(8,5,0)+import TcPluginM (unsafeTcPluginTcM)+#endif #if !MIN_VERSION_ghc(8,4,0) import TcPluginM (zonkCt) #endif import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs) import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc,+#if MIN_VERSION_ghc(8,5,0)+ ctEvPred, ctEvExpr, ctLoc, ctLocSpan, isWanted,+#else ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted,+#endif mkNonCanonical, setCtLoc, setCtLocSpan) import TcTypeNats (typeNatAddTyCon, typeNatSubTyCon) import Type@@ -261,7 +275,11 @@ -- 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@@ -272,10 +290,18 @@ _ -> Nothing -- | Create a look-up entry for a [G]iven constraint.+#if MIN_VERSION_ghc(8,5,0)+toGivenEntry :: Ct -> (CType,EvExpr)+#else toGivenEntry :: Ct -> (CType,EvTerm)+#endif toGivenEntry ct = let ct_ev = ctEvidence ct c_ty = ctEvPred ct_ev+#if MIN_VERSION_ghc(8,5,0)+ ev = ctEvExpr ct_ev+#else ev = ctEvTerm ct_ev+#endif in (CType c_ty,ev) -- | Normalise a type to Sum-of-Product type form as defined in the@@ -304,10 +330,21 @@ myPackage = fsLit "ghc-typelits-knownnat" -- | Try to create evidence for a wanted constraint-constraintToEvTerm :: KnownNatDefs -- ^ The "magic" KnownNatN classes- -> [(CType,EvTerm)] -- All the [G]iven constraints- -> KnConstraint- -> TcPluginM (Maybe ((EvTerm,Ct),[Ct]))+constraintToEvTerm+ :: 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+ -> 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. Normalise to SOP normal form let ty = normaliseSOP op@@ -324,7 +361,11 @@ -- 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@@ -353,18 +394,30 @@ -- This plugin only solves Literal KnownNat's that needed to be normalised -- first | otherwise+#if MIN_VERSION_ghc(8,5,0)+ = (fmap (,[])) <$> makeLitDict cls op i+#else = return ((,[]) <$> makeLitDict cls op i)+#endif go _ = return Nothing -- Get EvTerm arguments for type-level operations. If they do not exist -- as [G]iven constraints, then generate new [W]anted constraints+#if MIN_VERSION_ghc(8,5,0)+ go_arg :: PredType -> TcPluginM (EvExpr,[Ct])+#else go_arg :: PredType -> TcPluginM (EvTerm,[Ct])+#endif go_arg ty = case lookup (CType ty) givens of Just ev -> return (ev,[]) _ -> do -- Create a new wanted constraint wantedCtEv <- newWanted (ctLoc ct) ty+#if MIN_VERSION_ghc(8,5,0)+ let ev = ctEvExpr wantedCtEv+#else let ev = ctEvTerm wantedCtEv+#endif wanted = mkNonCanonical wantedCtEv -- Set the source-location of the new wanted constraint to the source -- location of the [W]anted constraint we are currently trying to solve@@ -375,7 +428,11 @@ -- 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]@@ -386,7 +443,11 @@ -- 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@@ -448,8 +509,15 @@ -> Class -- ^ KnownNat class -> [Type] -- ^ Argument types -> Type -- ^ Type of the result- -> [EvTerm] -- ^ Evidence arguments+#if MIN_VERSION_ghc(8,5,0)+ -> [EvExpr]+ -- ^ Evidence arguments+ -> Maybe EvExpr+#else+ -> [EvTerm]+ -- ^ 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@@ -469,7 +537,11 @@ $ idType op_meth -- forall f a b . KnownNat2 f a b => SNatKn (KnownNatF2 f a b) , 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+#else , let dfun_inst = EvDFunApp dfid (tail tyArgs) evArgs+#endif -- KnownNatAdd a b op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep))@@ -495,8 +567,15 @@ makeKnCoercion :: Class -- ^ KnownNat class -> Type -- ^ Type of the argument -> Type -- ^ Type of the result- -> EvTerm -- ^ KnownNat dictionary for the argument+#if MIN_VERSION_ghc(8,5,0)+ -> EvExpr+ -- ^ KnownNat dictionary for the argument+ -> Maybe EvExpr+#else+ -> EvTerm+ -- ^ 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@@ -523,7 +602,11 @@ -- -- 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)+#else makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm+#endif makeLitDict clas ty i | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] -- co_dict :: KnownNat n ~ SNat n@@ -534,7 +617,16 @@ $ idType meth -- forall n. KnownNat n => SNat n , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] -- SNat n ~ Integer+#if MIN_VERSION_ghc(8,5,0)+ = do+ et <- unsafeTcPluginTcM (mkNaturalExpr i)+ let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))+ return (Just ev_tm)+ | otherwise+ = return Nothing+#else , let ev_tm = mkEvCast (EvLit (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep)) = Just ev_tm | otherwise = Nothing+#endif