ghc-typelits-knownnat 0.7.8 → 0.7.9
raw patch · 3 files changed
+108/−48 lines, 3 filesdep ~ghcdep ~ghc-primdep ~template-haskellPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc, ghc-prim, template-haskell
API changes (from Hackage documentation)
Files
- CHANGELOG.md +3/−0
- ghc-typelits-knownnat.cabal +7/−7
- src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +98/−41
CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.7.9 *October 10th 2023*+* Support for GHC 9.8.1+ ## 0.7.8 *February 20th 2023* * Support for GHC-9.6.0.20230210
ghc-typelits-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.7.8+version: 0.7.9 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -54,8 +54,8 @@ CHANGELOG.md cabal-version: >=1.10 tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.4, GHC == 8.6.5,- GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.6,- GHC == 9.4.4, GHC == 9.6.1+ GHC == 8.8.4, GHC == 8.10.7, GHC == 9.0.2, GHC == 9.2.8,+ GHC == 9.4.7, GHC == 9.6.3, GHC == 9.8.1 source-repository head type: git@@ -87,12 +87,12 @@ UndecidableInstances ViewPatterns build-depends: base >= 4.9 && <5,- ghc >= 8.0.1 && <9.8,- ghc-prim >= 0.4.0.0 && <0.11,+ ghc >= 8.0.1 && <9.10,+ ghc-prim >= 0.4.0.0 && <0.12, ghc-tcplugins-extra >= 0.3.1, ghc-typelits-natnormalise >= 0.7.1 && <0.8, transformers >= 0.5.2.0 && <0.7,- template-haskell >= 2.11.0.0 && <2.21+ template-haskell >= 2.11.0.0 && <2.22 hs-source-dirs: src default-language: Haskell2010 if flag(deverror)@@ -101,7 +101,7 @@ ghc-options: -Wall if impl(ghc >= 8.0) && impl(ghc < 9.4) hs-source-dirs: src-pre-ghc-9.4- if impl(ghc >= 9.4) && impl(ghc < 9.8)+ if impl(ghc >= 9.4) && impl(ghc < 9.10) hs-source-dirs: src-ghc-9.4 if impl(ghc < 8.2) build-depends: integer-gmp >= 0.5.1.0
src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs view
@@ -101,7 +101,7 @@ import Control.Arrow ((&&&), first) import Control.Monad.Trans.Maybe (MaybeT (..)) import Control.Monad.Trans.Writer.Strict-import Data.Maybe (catMaybes,mapMaybe)+import Data.Maybe (catMaybes, fromMaybe, mapMaybe) import GHC.TcPluginM.Extra (lookupModule, lookupName, newWanted, tracePlugin) import GHC.TypeLits.Normalise.SOP (SOP (..), Product (..), Symbol (..)) import GHC.TypeLits.Normalise.Unify (CType (..),normaliseNat,reifySOP)@@ -113,7 +113,9 @@ import GHC.Builtin.Types (promotedFalseDataCon, promotedTrueDataCon) import GHC.Builtin.Types.Literals (typeNatCmpTyCon) import GHC.Core.Class (Class, classMethods, className, classTyCon)-import GHC.Core.Coercion (Role (Representational), mkUnivCo)+import GHC.Core.Coercion+ (Coercion, Role (Nominal, Representational), coercionRKind, mkNomReflCo,+ mkTyConAppCo, mkUnivCo) import GHC.Core.InstEnv (instanceDFunId, lookupUniqueInstEnv) import GHC.Core.Make (mkNaturalExpr) import GHC.Core.Predicate@@ -142,12 +144,13 @@ (Ct, ctEvExpr, ctEvidence, ctEvPred, ctLoc, mkNonCanonical) #if MIN_VERSION_ghc(9,6,0) import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast)+ (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, evTermCoercion_maybe) import GHC.Plugins- (Coercion, mkSymCo, mkTransCo)+ (mkSymCo, mkTransCo) #else import GHC.Tc.Types.Evidence- (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo)+ (EvTerm (..), EvExpr, EvBindsVar, evDFunApp, mkEvCast, mkTcSymCo, mkTcTransCo,+ evTermCoercion_maybe) #endif import GHC.Types.Id (idType) import GHC.Types.Name (nameModule_maybe, nameOccName)@@ -360,15 +363,15 @@ found@Just {} -> return found -- 3.b If not, we check if the outer type-level operation -- has a corresponding KnownNat<N> instance.- _ -> go op+ _ -> go (op,Nothing) return ((first (,ct)) <$> evM) where -- Determine whether the outer type-level operation has a corresponding -- KnownNat<N> instance, where /N/ corresponds to the arity of the -- type-level operation- go :: Type -> TcPluginM (Maybe (EvTerm,[Ct]))- go (go_other -> Just ev) = return (Just (ev,[]))- go ty@(TyConApp tc args0)+ go :: (Type, Maybe Coercion) -> TcPluginM (Maybe (EvTerm,[Ct]))+ go (go_other -> Just ev, _) = return (Just (ev,[]))+ go (ty@(TyConApp tc args0), sM) | let tcNm = tyConName tc , Just m <- nameModule_maybe tcNm = do@@ -384,29 +387,29 @@ -> Just (inst,knN_cls,args0,args1) | fn0 == "Data.Type.Ord.OrdCond" , [_,cmpNat,TyConApp t1 [],TyConApp t2 [],TyConApp f1 []] <- args0- , TyConApp cmpNatTc args2 <- cmpNat+ , TyConApp cmpNatTc args2@(arg2:_) <- cmpNat , cmpNatTc == typeNatCmpTyCon , t1 == promotedTrueDataCon , t2 == promotedTrueDataCon , f1 == promotedFalseDataCon , let knN_cls = knownBoolNat2 defs- ki = typeKind (head args2)+ ki = typeKind arg2 args1N = ki:fn1:args2 , Right (inst,_) <- lookupUniqueInstEnv ienv knN_cls args1N -> Just (inst,knN_cls,args2,args1N)- | length args0 == 2+ | [arg0,_] <- args0 , let knN_cls = knownBoolNat2 defs- ki = typeKind (head args0)+ ki = typeKind arg0 args1N = ki:args1 , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N -> Just (inst,knN_cls,args0,args1N)- | length args0 == 4+ | (arg0:args0Rest) <- args0+ , length args0Rest == 3 , fn0 == "Data.Type.Bool.If"- , let args0N = tail args0- args1N = head args0:fn1:tail args0+ , let args1N = arg0:fn1:args0Rest knN_cls = knownNat2Bool defs , Right (inst, _) <- lookupUniqueInstEnv ienv knN_cls args1N- -> Just (inst,knN_cls,args0N,args1N)+ -> Just (inst,knN_cls,args0Rest,args1N) | otherwise -> Nothing case instM of@@ -454,10 +457,10 @@ -- follows 'CLog 2 n + 1', the type of the evidence will be -- 'KnownNat fsk'; the one GHC originally asked us to solve. then return ((,concat new) <$> makeOpDictByFiat df cls args1N args0N (unOrig orig) evs)- else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs)+ else return ((,concat new) <$> makeOpDict df cls args1N args0N (unOrig orig) evs (fmap (ty,) sM)) _ -> return ((,[]) <$> go_other ty) - go (LitTy (NumTyLit i))+ go ((LitTy (NumTyLit i)), _) -- Let GHC solve simple Literal constraints | LitTy _ <- op = return Nothing@@ -498,23 +501,30 @@ -> Just ty'' _ -> Nothing -- Get the rewrites- unEq ty' = case classifyPredType ty' of- EqPred NomEq ty1 ty2 -> Just (ty1,ty2)- _ -> Nothing- rewrites = mapMaybe (unEq . unCType . fst) givens+ unEq (ty',ev) = case classifyPredType ty' of+ EqPred NomEq ty1 ty2 -> Just (ty1,ty2,ev)+ _ -> Nothing+ rewrites :: [(Type,Type,EvExpr)]+ rewrites = mapMaybe (unEq . first unCType) givens -- Rewrite- rewriteTy tyK (ty1,ty2) | ty1 `eqType` tyK = Just ty2- | ty2 `eqType` tyK = Just ty1- | otherwise = Nothing+ rewriteTy tyK (ty1,ty2,ev)+ | ty1 `eqType` tyK+ = Just (ty2,Just (tyK,evTermCoercion_maybe (EvExpr ev)))+ | ty2 `eqType` tyK+ = Just (ty1,Just (tyK,fmap mkTcSymCo (evTermCoercion_maybe (EvExpr ev))))+ | otherwise+ = Nothing -- Get only the [G]iven KnownNat constraints knowns = mapMaybe (unKn . unCType . fst) givens -- Get all the rewritten KNs knownsR = catMaybes $ concatMap (\t -> map (rewriteTy t) rewrites) knowns- knownsX = knowns ++ knownsR+ knownsX :: [(Type, Maybe (Type, Maybe Coercion))]+ knownsX = fmap (,Nothing) 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)+ -- exploded :: [()]+ exploded = map (fst . runWriter . normaliseNat . subWant . fst &&& id) knownsX -- interesting cases for us are those where -- wanted and given only differ by a constant@@ -523,24 +533,60 @@ examineDiff _ _ = Nothing interesting = mapMaybe (uncurry examineDiff) exploded -- convert the first suitable evidence- ((h,corr):_) <- pure interesting+ (((h,sM),corr):_) <- pure interesting x <- case corr of- I 0 -> pure h+ I 0 -> pure (fromMaybe (h,Nothing) sM) I i | i < 0- -> pure (mkTyConApp typeNatAddTyCon [h,mkNumLitTy (negate i)])+ , let l1 = mkNumLitTy (negate i)+ -> case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatAddTyCon [q,l1]+ , fmap (mkTyConAppCo Nominal typeNatAddTyCon . (:[mkNomReflCo l1])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatAddTyCon [h,l1]+ , Nothing+ ) | otherwise- -> pure (mkTyConApp typeNatSubTyCon [h,mkNumLitTy i])+ , let l1 = mkNumLitTy i+ -> case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatSubTyCon [q,l1]+ , fmap (mkTyConAppCo Nominal typeNatSubTyCon . (:[mkNomReflCo l1])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatSubTyCon [h,l1]+ , Nothing+ ) -- 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 ->- pure (mkTyConApp typeNatDivTyCon [h,reifySOP (S [P [I 2]])])+ c | CType (reifySOP (S [P [c]])) == CType want+ , let l2 = mkNumLitTy 2+ -> case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatDivTyCon [q,l2]+ , fmap (mkTyConAppCo Nominal typeNatDivTyCon . (:[mkNomReflCo l2])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatDivTyCon [h,l2]+ , Nothing+ ) -- 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]])])+ V v | all (not . eqType (TyVarTy v) . fst) knownsX+ -> MaybeT (pure Nothing)+ _ -> let lC = reifySOP (S [P [corr]]) in+ case sM of+ Just (q,cM) -> pure+ ( mkTyConApp typeNatSubTyCon [q,lC]+ , fmap (mkTyConAppCo Nominal typeNatSubTyCon . (:[mkNomReflCo lC])) cM+ )+ Nothing -> pure+ ( mkTyConApp typeNatSubTyCon [h,lC]+ , Nothing+ ) MaybeT (go x) makeWantedEv@@ -585,16 +631,18 @@ -- ^ Type of the result -> [EvExpr] -- ^ Evidence arguments+ -> Maybe (Type, Coercion) -> Maybe EvTerm-makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs- | Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z]+makeOpDict (opCls,dfid) knCls tyArgsC tyArgsI z evArgs sM+ | let z1 = maybe z fst sM+ , Just (_, kn_co_dict) <- tcInstNewTyCon_maybe (classTyCon knCls) [z1] -- KnownNat n ~ SNat n , [ kn_meth ] <- classMethods knCls , Just kn_tcRep <- tyConAppTyCon_maybe -- SNat $ funResultTy -- SNat n $ dropForAlls -- KnownNat n => SNat n $ idType kn_meth -- forall n. KnownNat n => SNat n- , Just (_, kn_co_rep) <- tcInstNewTyCon_maybe kn_tcRep [z]+ , Just (_, kn_co_rep) <- tcInstNewTyCon_maybe kn_tcRep [z1] -- SNat n ~ Integer , Just (_, op_co_dict) <- tcInstNewTyCon_maybe (classTyCon opCls) tyArgsC -- KnownNatAdd a b ~ SNatKn (a+b)@@ -610,7 +658,16 @@ , let op_to_kn = mkTcTransCo (mkTcTransCo op_co_dict op_co_rep) (mkTcSymCo (mkTcTransCo kn_co_dict kn_co_rep)) -- KnownNatAdd a b ~ KnownNat (a+b)- ev_tm = mkEvCast dfun_inst op_to_kn+ , let op_to_kn1 = case sM of+ Nothing -> op_to_kn+ Just (_,rw) ->+ let kn_co_rw = mkTyConAppCo Representational (classTyCon knCls) [rw]+ kn_co_co = mkUnivCo (PluginProv "ghc-typelits-knownnat")+ Representational+ (coercionRKind kn_co_rw)+ (mkTyConApp (classTyCon knCls) [z])+ in mkTcTransCo op_to_kn (mkTcTransCo kn_co_rw kn_co_co)+ , let ev_tm = mkEvCast dfun_inst op_to_kn1 = Just ev_tm | otherwise = Nothing