diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/ghc-typelits-knownnat.cabal b/ghc-typelits-knownnat.cabal --- a/ghc-typelits-knownnat.cabal +++ b/ghc-typelits-knownnat.cabal @@ -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 diff --git a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs --- a/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs +++ b/src-ghc-9.4/GHC/TypeLits/KnownNat/Solver.hs @@ -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 instance. - _ -> go op + _ -> go (op,Nothing) return ((first (,ct)) <$> evM) where -- Determine whether the outer type-level operation has a corresponding -- KnownNat 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