diff options
-rw-r--r-- | compiler/GHC/Core/Coercion.hs | 14 | ||||
-rw-r--r-- | compiler/GHC/Core/Coercion.hs-boot | 3 | ||||
-rw-r--r-- | compiler/GHC/Core/Coercion/Opt.hs | 14 | ||||
-rw-r--r-- | compiler/GHC/Core/Lint.hs | 12 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/FVs.hs | 39 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs | 68 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Rep.hs-boot | 1 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Subst.hs | 8 | ||||
-rw-r--r-- | compiler/GHC/Core/TyCo/Tidy.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Core/Type.hs | 43 | ||||
-rw-r--r-- | compiler/GHC/CoreToIface.hs | 10 | ||||
-rw-r--r-- | compiler/GHC/IfaceToCore.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 32 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 17 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/Zonk.hs | 9 | ||||
-rw-r--r-- | compiler/GHC/Types/Unique/DSet.hs | 13 | ||||
-rw-r--r-- | testsuite/tests/dependent/should_compile/T14729.stderr | 4 | ||||
-rw-r--r-- | testsuite/tests/rep-poly/T20363_show_co.stderr | 4 |
18 files changed, 223 insertions, 73 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 4e13e02bc7..861a0002a7 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -126,7 +126,13 @@ module GHC.Core.Coercion ( hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy, - setCoHoleType + setCoHoleType, + + FreeCoVarsHoles, + mkFreeCoVarsHoles, updateFreeCoVars, updateFreeCoVarsM, + sizeFreeCoVarsHoles, + freeCoVars, freeCoHoles, + ) where import {-# SOURCE #-} GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs) @@ -1337,7 +1343,7 @@ mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r (mkCoercionTy g1) (mkCoercionTy g2) -- | TODO (RAE): Comment -mkZappedCo :: Role -> Type -> Type -> DCoVarSet -> Coercion +mkZappedCo :: Role -> Type -> Type -> FreeCoVarsHoles -> Coercion mkZappedCo = ZappedCo {- @@ -2347,7 +2353,7 @@ seqCo (InstCo co arg) = seqCo co `seq` seqCo arg seqCo (KindCo co) = seqCo co seqCo (SubCo co) = seqCo co seqCo (AxiomRuleCo _ cs) = seqCos cs -seqCo (ZappedCo r t1 t2 cvs) = r `seq` seqType t1 `seq` seqType t2 `seq` seqDVarSet cvs +seqCo (ZappedCo r t1 t2 _vs) = r `seq` seqType t1 `seq` seqType t2 seqProv :: UnivCoProvenance -> () seqProv (PhantomProv co) = seqCo co @@ -2776,4 +2782,4 @@ hasThisCoercionHoleTy ty hole = Monoid.getAny (f ty) -- | Set the type of a 'CoercionHole' setCoHoleType :: CoercionHole -> Type -> CoercionHole -setCoHoleType h t = setCoHoleCoVar h (setVarType (coHoleCoVar h) t) +setCoHoleType h t = setCoHoleCoVar h (setVarType (coHoleCoVar h) t)
\ No newline at end of file diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot index 2d90b8e210..0c1f81b7cb 100644 --- a/compiler/GHC/Core/Coercion.hs-boot +++ b/compiler/GHC/Core/Coercion.hs-boot @@ -10,7 +10,6 @@ import {-# SOURCE #-} GHC.Core.TyCon import GHC.Types.Basic ( LeftOrRight ) import GHC.Core.Coercion.Axiom import GHC.Types.Var -import GHC.Types.Var.Set import GHC.Data.Pair import GHC.Utils.Misc @@ -34,7 +33,7 @@ mkKindCo :: Coercion -> Coercion mkSubCo :: HasDebugCallStack => Coercion -> Coercion mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion -mkZappedCo :: Role -> Type -> Type -> DCoVarSet -> Coercion +mkZappedCo :: Role -> Type -> Type -> FreeCoVarsHoles -> Coercion isGReflCo :: Coercion -> Bool isReflCo :: Coercion -> Bool diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs index 3c81d3f349..4ebe2379c3 100644 --- a/compiler/GHC/Core/Coercion/Opt.hs +++ b/compiler/GHC/Core/Coercion/Opt.hs @@ -36,6 +36,7 @@ import GHC.Utils.Trace import Control.Monad ( zipWithM ) import GHC.Core.TyCo.FVs +import GHC.Types.Unique.DSet {- %************************************************************************ @@ -471,22 +472,23 @@ opt_co4 env sym rep r (AxiomRuleCo co cs) wrapSym sym $ AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs) -opt_co4 env sym rep r (ZappedCo _r t1 t2 cvs) +opt_co4 env sym rep r (ZappedCo _r t1 t2 vs) | assert (r == _r) $ + assert (isEmptyUniqDSet (freeCoHoles vs)) $ t1' `eqType` t2' = mkReflCo (chooseRole rep r) t1' | sym - = ZappedCo (chooseRole rep r) t2' t1' cvs' + = ZappedCo (chooseRole rep r) t2' t1' vs' | otherwise - = ZappedCo (chooseRole rep r) t1' t2' cvs' + = ZappedCo (chooseRole rep r) t1' t2' vs' where t1' = substTy (lcSubstLeft env) t1 t2' = substTy (lcSubstRight env) t2 - cvs' = coVarsOfCosDSet $ map opt (dVarSetElems cvs) + vs' = updateFreeCoVars vs (coVarsOfCosDSet . map opt . dVarSetElems) opt cv = opt_covar env False False (coVarRole cv) cv @@ -702,10 +704,10 @@ opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2) = fireTransRule "PushLR" in_co1 in_co2 $ mkLRCo d1 (opt_trans is co1 co2) -opt_trans_rule _is in_co1@(ZappedCo r1 t1 _ cvs1) in_co2@(ZappedCo r2 _ t2 cvs2) +opt_trans_rule _is in_co1@(ZappedCo r1 t1 _ vs1) in_co2@(ZappedCo r2 _ t2 vs2) = assert (r1 == r2) $ fireTransRule "PushZapped" in_co1 in_co2 $ - mkZappedCo r1 t1 t2 (cvs1 `unionDVarSet` cvs2) + mkZappedCo r1 t1 t2 (vs1 `mappend` vs2) -- Push transitivity inside instantiation opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2) diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index eda7407dbe..b9b3d5ca1d 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -96,6 +96,7 @@ import Data.List ( partition ) import Data.Maybe import GHC.Data.Pair import qualified GHC.LanguageExtensions as LangExt +import GHC.Types.Unique.DSet {- Note [Core Lint guarantee] @@ -2409,14 +2410,17 @@ lintCoercion (HoleCo h) = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h ; lintCoercion (CoVarCo (coHoleCoVar h)) } -lintCoercion (ZappedCo r t1 t2 cvs) +lintCoercion co@(ZappedCo r t1 t2 vs) = do { t1' <- lintType t1 ; t2' <- lintType t2 - ; substed_cvs <- mapM lintCoVar (dVarSetElems cvs) - ; let cvs' = coVarsOfCosDSet substed_cvs + ; vs' <- updateFreeCoVarsM vs $ \cvs -> + coVarsOfCosDSet <$> mapM lintCoVar (dVarSetElems cvs) - ; return (ZappedCo r t1' t2' cvs') } + ; checkL (isEmptyUniqDSet (freeCoHoles vs)) $ + text "Unzonked coercion hole in ZappedCo:" <+> ppr co + + ; return (ZappedCo r t1' t2' vs') } lintCoVar :: CoVar -> LintM LintedCoercion lintCoVar cv diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs index 9d9cd6b169..c2921ec057 100644 --- a/compiler/GHC/Core/TyCo/FVs.hs +++ b/compiler/GHC/Core/TyCo/FVs.hs @@ -16,11 +16,13 @@ module GHC.Core.TyCo.FVs tyCoVarsOfCo, tyCoVarsOfCos, tyCoVarsOfMCo, coVarsOfType, coVarsOfTypes, coVarsOfCo, coVarsOfCos, - coVarsOfCoDSet, coVarsOfCosDSet, + coVarsOfCosDSet, tyCoVarsOfCoDSet, tyCoVarsOfCosDSet, tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoList, + coVarsHolesOfCo, coVarsHolesOfCos, + almostDevoidCoVarOfCo, -- Injective free vars @@ -52,7 +54,7 @@ import GHC.Core.TyCo.Rep import GHC.Core.TyCon import GHC.Types.Var import GHC.Utils.FV - +import GHC.Types.Unique.DSet import GHC.Types.Unique.FM import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -431,9 +433,6 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView -- See Note [CoercionHoles and coercion free variables] -- in GHC.Core.TyCo.Rep -coVarsOfCoDSet :: Coercion -> DCoVarSet -coVarsOfCoDSet = fvDVarSet . filterFV isCoVar . tyCoFVsOfCo - coVarsOfCosDSet :: [Coercion] -> DCoVarSet coVarsOfCosDSet = fvDVarSet . filterFV isCoVar . tyCoFVsOfCos @@ -648,7 +647,11 @@ tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in tyCoFVsOfCo (SubCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (AxiomRuleCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc tyCoFVsOfCo (ZappedCo _ a b vs) fv_cand in_scope acc - = (tyCoFVsOfType a `unionFV` tyCoFVsOfType b `unionFV` mkFVs (dVarSetElems vs)) + = (tyCoFVsOfType a `unionFV` + tyCoFVsOfType b `unionFV` + mapUnionFV tyCoFVsOfCoVar (dVarSetElems (freeCoVars vs)) `unionFV` + mapUnionFV (tyCoFVsOfCoVar . coHoleCoVar) (uniqDSetToList (freeCoHoles vs))) + -- See Note [CoercionHoles and coercion free variables] fv_cand in_scope acc tyCoFVsOfCoVar :: CoVar -> FV @@ -717,10 +720,12 @@ almost_devoid_co_var_of_co (SubCo co) cv = almost_devoid_co_var_of_co co cv almost_devoid_co_var_of_co (AxiomRuleCo _ cs) cv = almost_devoid_co_var_of_cos cs cv -almost_devoid_co_var_of_co (ZappedCo _ t1 t2 cvs) cv +almost_devoid_co_var_of_co (ZappedCo _ t1 t2 vs) cv = almost_devoid_co_var_of_type t1 cv && almost_devoid_co_var_of_type t2 cv - && not (cv `elemDVarSet` cvs) + && not (cv `elemDVarSet` freeCoVars vs) + && not (cv `elemDVarSet` mapUniqDSet coHoleCoVar (freeCoHoles vs)) + -- there should be no holes here, anyway almost_devoid_co_var_of_cos :: [Coercion] -> CoVar -> Bool almost_devoid_co_var_of_cos [] _ = True @@ -1014,3 +1019,21 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList -- | Get the free vars of types in scoped order tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar] tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList + +{- ********************************************************************* +* * + Free coercion holes +* * +********************************************************************* -} + +coVarsHolesOfCo :: Coercion -> FreeCoVarsHoles +coVarsHolesOfCos :: [Coercion] -> FreeCoVarsHoles +(coVarsHolesOfCo, coVarsHolesOfCos) = (go_co, go_cos) + where + (go_ty, _, go_co, go_cos) = foldTyCo folder () + folder = TyCoFolder { tcf_view = noView + , tcf_tyvar = \ _ tv -> go_ty (varType tv) + , tcf_covar = \ _ cv -> mkFreeCoVarsHoles (unitDVarSet cv) mempty `mappend` + go_ty (varType cv) + , tcf_hole = \ _ h -> mkFreeCoVarsHoles mempty (unitUniqDSet h) + , tcf_tycobinder = const2 } diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 79dea31396..ee9712281e 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -41,6 +41,12 @@ module GHC.Core.TyCo.Rep ( CoercionN, CoercionR, CoercionP, KindCoercion, MCoercion(..), MCoercionR, MCoercionN, + FreeCoVarsHoles, + mkFreeCoVarsHoles, updateFreeCoVars, updateFreeCoVarsM, + sizeFreeCoVarsHoles, + freeCoVars, freeCoHoles, + + -- * Functions over types mkNakedTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, @@ -98,6 +104,10 @@ import GHC.Utils.Panic -- libraries import qualified Data.Data as Data hiding ( TyCon ) import Data.IORef ( IORef ) -- for CoercionHole +import GHC.Types.Unique.DSet +import qualified Data.Semigroup -- for (<>) in a Semigroup instance only +import GHC.Utils.Panic.Plain + {- ********************************************************************** * * @@ -1209,7 +1219,7 @@ data Coercion | HoleCo CoercionHole -- ^ See Note [Coercion holes] -- Only present during typechecking - | ZappedCo Role Type Type DCoVarSet -- TODO (RAE): Comment + | ZappedCo Role Type Type !FreeCoVarsHoles -- TODO (RAE): Comment deriving Data.Data type CoercionN = Coercion -- always nominal @@ -1661,6 +1671,55 @@ instance Outputable CoercionHole where instance Uniquable CoercionHole where getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv +-- | Stores the free covars and coercion holes from a type or coercion; +-- these are often needed together +data FreeCoVarsHoles = FCVH_Empty -- avoid allocating a new FCVH node at every <> + | FCVH !DCoVarSet !(UniqDSet CoercionHole) + deriving Data.Data + +mkFreeCoVarsHoles :: DCoVarSet -> UniqDSet CoercionHole -> FreeCoVarsHoles +mkFreeCoVarsHoles = FCVH + +-- this one preserves FCVH_Empty +-- Pre-condition: f empty == empty +updateFreeCoVars :: FreeCoVarsHoles -> (DCoVarSet -> DCoVarSet) -> FreeCoVarsHoles +updateFreeCoVars FCVH_Empty f = assert (isEmptyDVarSet (f emptyDVarSet)) + FCVH_Empty +updateFreeCoVars (FCVH cvs hs) f = FCVH (f cvs) hs + +-- this one preserves FCVH_Empty +-- Pre-condition: f empty == empty (and has no side effects) +updateFreeCoVarsM :: Applicative m => FreeCoVarsHoles -> (DCoVarSet -> m DCoVarSet) + -> m FreeCoVarsHoles +updateFreeCoVarsM FCVH_Empty _ = pure FCVH_Empty +updateFreeCoVarsM (FCVH cvs hs) f = FCVH <$> f cvs <*> pure hs + +freeCoVars :: FreeCoVarsHoles -> DCoVarSet +freeCoVars FCVH_Empty = emptyDVarSet +freeCoVars (FCVH cvs _) = cvs + +freeCoHoles :: FreeCoVarsHoles -> UniqDSet CoercionHole +freeCoHoles FCVH_Empty = emptyUniqDSet +freeCoHoles (FCVH _ hs) = hs + +sizeFreeCoVarsHoles :: FreeCoVarsHoles -> Int +sizeFreeCoVarsHoles FCVH_Empty = 0 +sizeFreeCoVarsHoles (FCVH cvs hs) = sizeDVarSet cvs + sizeUniqDSet hs + +instance Outputable FreeCoVarsHoles where + ppr FCVH_Empty = braces empty + ppr (FCVH vs hs) = braces (fcat (punctuate comma (map ppr (dVarSetElems vs))) <> vbar <> + fcat (punctuate comma (map ppr (uniqDSetToList hs)))) + +instance Semigroup FreeCoVarsHoles where + FCVH_Empty <> FCVH_Empty = FCVH_Empty + FCVH_Empty <> other = other + other <> FCVH_Empty = other + FCVH vs1 hs1 <> FCVH vs2 hs2 = FCVH (vs1 `mappend` vs2) (hs1 `mappend` hs2) + +instance Monoid FreeCoVarsHoles where + mempty = FCVH_Empty + {- Note [Phantom coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1936,9 +1995,10 @@ foldTyCo (TyCoFolder { tcf_view = view go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg go_co env (KindCo co) = go_co env co go_co env (SubCo co) = go_co env co - go_co env (ZappedCo _ t1 t2 cvs) = go_ty env t1 `mappend` + go_co env (ZappedCo _ t1 t2 vs) = go_ty env t1 `mappend` go_ty env t2 `mappend` - foldMap (covar env) cvs + foldMap (covar env) (freeCoVars vs) `mappend` + foldMap (cohole env) (freeCoHoles vs) go_co env (ForAllCo tv kind_co co) = go_co env kind_co `mappend` go_ty env (varType tv) `mappend` go_co env' co @@ -2004,7 +2064,7 @@ coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg coercionSize (KindCo co) = 1 + coercionSize co coercionSize (SubCo co) = 1 + coercionSize co coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs) -coercionSize (ZappedCo _ a b vs) = 1 + typeSize a + typeSize b + sizeDVarSet vs +coercionSize (ZappedCo _ a b vs) = 1 + typeSize a + typeSize b + sizeFreeCoVarsHoles vs provSize :: UnivCoProvenance -> Int provSize (PhantomProv co) = 1 + coercionSize co diff --git a/compiler/GHC/Core/TyCo/Rep.hs-boot b/compiler/GHC/Core/TyCo/Rep.hs-boot index f2e59d534f..89138ebf3a 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs-boot +++ b/compiler/GHC/Core/TyCo/Rep.hs-boot @@ -8,6 +8,7 @@ import {-# SOURCE #-} GHC.Core.TyCon ( TyCon ) data Type data Coercion +data FreeCoVarsHoles data UnivCoProvenance data TyLit data TyCoBinder diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs index defdad591c..e9a16d60e8 100644 --- a/compiler/GHC/Core/TyCo/Subst.hs +++ b/compiler/GHC/Core/TyCo/Subst.hs @@ -85,6 +85,7 @@ import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Data.List (mapAccumL) +import GHC.Types.Unique.DSet {- %************************************************************************ @@ -859,8 +860,11 @@ subst_co subst co go (AxiomRuleCo c cs) = let cs1 = map go cs in cs1 `seqList` AxiomRuleCo c cs1 go (HoleCo h) = HoleCo $! go_hole h - go (ZappedCo r t1 t2 vs) = ((mkZappedCo r $! go_ty t1) $! go_ty t2) $! - coVarsOfCosDSet (map (substCoVar subst) (dVarSetElems vs)) + go (ZappedCo r t1 t2 vs) = ((mkZappedCo r $! go_ty t1) $! go_ty t2) $! new_vs + where + cos_from_vs = map (substCoVar subst) (dVarSetElems (freeCoVars vs)) + new_vs = coVarsHolesOfCos cos_from_vs `mappend` + mkFreeCoVarsHoles mempty (mapUniqDSet go_hole (freeCoHoles vs)) go_prov (PhantomProv kco) = PhantomProv (go kco) go_prov (ProofIrrelProv kco) = ProofIrrelProv (go kco) diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs index 28f4a1f504..880dc3c725 100644 --- a/compiler/GHC/Core/TyCo/Tidy.hs +++ b/compiler/GHC/Core/TyCo/Tidy.hs @@ -248,7 +248,7 @@ tidyCo env@(_, subst) co go (SubCo co) = SubCo $! go co go (AxiomRuleCo ax cos) = AxiomRuleCo ax $ strictMap go cos go (ZappedCo r t1 t2 vs) = ((ZappedCo r $! tidyType env t1) $! tidyType env t2) $! - mapDVarSet go_covar vs + updateFreeCoVars vs (mapDVarSet go_covar) go_covar cv | Just cv' <- lookupVarEnv subst cv = cv' diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 01e26e0d73..1c84383e50 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -296,6 +296,7 @@ import GHC.Types.Unique ( nonDetCmpUnique ) import GHC.Data.Maybe ( orElse, expectJust ) import Data.Maybe ( isJust ) import Control.Monad ( guard ) +import GHC.Types.Unique.DSet -- import GHC.Utils.Trace -- $type_classification @@ -622,9 +623,10 @@ expandTypeSynonyms ty = AxiomRuleCo ax (map (go_co subst) cs) go_co _ (HoleCo h) = pprPanic "expandTypeSynonyms hit a hole" (ppr h) - go_co subst (ZappedCo r t1 t2 cvs) - = mkZappedCo r (go subst t1) (go subst t2) - (coVarsOfCosDSet (map (substCoVar subst) (dVarSetElems cvs))) + go_co subst (ZappedCo r t1 t2 vs) + = assert (isEmptyUniqDSet (freeCoHoles vs)) $ + mkZappedCo r (go subst t1) (go subst t2) + (updateFreeCoVars vs (coVarsOfCosDSet . map (substCoVar subst) . dVarSetElems)) go_prov subst (PhantomProv co) = PhantomProv (go_co subst co) go_prov subst (ProofIrrelProv co) = ProofIrrelProv (go_co subst co) @@ -976,9 +978,16 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar ; co' <- go_co env' co ; return $ mkForAllCo tv' kind_co' co' } -- See Note [Efficiency for ForAllCo case of mapTyCoX] - go_co env (ZappedCo r t1 t2 cvs) - = ZappedCo r <$> go_ty env t1 <*> go_ty env t2 <*> - (coVarsOfCosDSet <$> mapM (covar env) (dVarSetElems cvs)) + go_co env (ZappedCo r t1 t2 vs) + = do { t1' <- go_ty env t1 + ; t2' <- go_ty env t2 + ; let cvs = freeCoVars vs + hs = freeCoHoles vs + ; cos_from_cvs <- mapM (covar env) (dVarSetElems cvs) + ; cos_from_hs <- mapM (cohole env) (uniqDSetToList hs) + ; let new_vs = coVarsHolesOfCos cos_from_cvs `mappend` coVarsHolesOfCos cos_from_hs + ; return $ mkZappedCo r t1' t2' new_vs } + go_prov env (PhantomProv co) = PhantomProv <$> go_co env co go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co @@ -2532,7 +2541,7 @@ getRuntimeRep_maybe :: HasDebugCallStack getRuntimeRep_maybe = kindRep_maybe . typeKind -- | Extract the RuntimeRep classifier of a type. For instance, --- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible. +-- @getRuntimeRep Int = LiftedRep@. Panics if this is not possible. getRuntimeRep :: HasDebugCallStack => Type -> Type getRuntimeRep ty = case getRuntimeRep_maybe ty of @@ -3372,11 +3381,11 @@ occCheckExpand vs_to_avoid ty ; co2' <- go_co cxt co2 ; w' <- go_co cxt w ; return (mkFunCo r w' co1' co2') } - go_co env (CoVarCo cv) = do { cv' <- go_covar env cv + go_co cxt (CoVarCo cv) = do { cv' <- go_covar cxt cv ; return (mkCoVarCo cv') } - go_co (as,_) co@(HoleCo h) - | bad_var_occ as (ch_co_var h) = Nothing - | otherwise = return co + go_co cxt co@(HoleCo h) + | ok_hole cxt h = return co + | otherwise = Nothing go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args ; return (mkAxiomInstCo ax ind args') } @@ -3402,16 +3411,20 @@ occCheckExpand vs_to_avoid ty ; return (mkSubCo co') } go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs ; return (mkAxiomRuleCo ax cs') } - go_co cxt (ZappedCo r t1 t2 cvs) = do { t1' <- go cxt t1 - ; t2' <- go cxt t2 - ; cvs' <- mapM (go_covar cxt) (dVarSetElems cvs) - ; return (mkZappedCo r t1' t2' (mkDVarSet cvs')) } + go_co cxt (ZappedCo r t1 t2 vs) + = do { t1' <- go cxt t1 + ; t2' <- go cxt t2 + ; vs' <- updateFreeCoVarsM vs $ \cvs -> + mkDVarSet <$> mapM (go_covar cxt) (dVarSetElems cvs) + ; guard (all (ok_hole cxt) (uniqDSetToList (freeCoHoles vs))) + ; return (mkZappedCo r t1' t2' vs') } go_covar (as,env) cv | Just cv' <- lookupVarEnv env cv = return cv' | bad_var_occ as cv = Nothing | otherwise = return cv + ok_hole (as,_) h = not (bad_var_occ as (ch_co_var h)) ------------------ go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs index 24bf2f656a..b40750c8a1 100644 --- a/compiler/GHC/CoreToIface.hs +++ b/compiler/GHC/CoreToIface.hs @@ -84,6 +84,7 @@ import GHC.Utils.Misc import GHC.Utils.Trace import Data.Maybe ( catMaybes ) +import GHC.Types.Unique.DSet {- Note [Avoiding space leaks in toIface*] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -296,9 +297,14 @@ toIfaceCoercionX fr co go (KindCo c) = IfaceKindCo (go c) go (SubCo co) = IfaceSubCo (go co) go (ZappedCo r t1 t2 vs)= IfaceZappedCo r (toIfaceTypeX fr t1) (toIfaceTypeX fr t2) - free_cvs (map toIfaceCoVar (dVarSetElems bound_cvs)) + (free_cvs1 `unionDVarSet` free_cvs2) + (map toIfaceCoVar (dVarSetElems bound_cvs)) where - (free_cvs, bound_cvs) = partitionDVarSet (`elemVarSet` fr) vs + cvs = freeCoVars vs + hs = freeCoHoles vs + (free_cvs1, bound_cvs) = partitionDVarSet (`elemVarSet` fr) cvs + free_cvs2 = mkDVarSet (map coHoleCoVar (uniqDSetToList hs)) + go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (coaxrName co) (map go cs) go (AxiomInstCo c i cs) = IfaceAxiomInstCo (coAxiomName c) i (map go cs) go (UnivCo p r t1 t2) = IfaceUnivCo (go_prov p) r diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs index df1bf0eb65..6999077a10 100644 --- a/compiler/GHC/IfaceToCore.hs +++ b/compiler/GHC/IfaceToCore.hs @@ -1429,7 +1429,8 @@ tcIfaceCo = go go (IfaceHoleCo c) = pprPanic "tcIfaceCo:IfaceHoleCo" (ppr c) go (IfaceZappedCo r t1 t2 free_cvs bound_cvs) = assert (isEmptyDVarSet free_cvs) $ - ZappedCo r <$> tcIfaceType t1 <*> tcIfaceType t2 <*> (mkDVarSet <$> mapM go_var bound_cvs) + ZappedCo r <$> tcIfaceType t1 <*> tcIfaceType t2 <*> + (mkFreeCoVarsHoles <$> (mkDVarSet <$> mapM go_var bound_cvs) <*> pure mempty) go_var :: FastString -> IfL CoVar go_var = tcIfaceLclId diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 43436347b8..baedbef2ef 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -1127,22 +1127,23 @@ mk_maybe_roles ReprEq roles = Just roles data UsedCoVars = JustZonked -- ^ we only zonked; nothing else interesting happened -- consequence: a coercion between the output and the input is just Refl - | UsedCoVars DCoVarSet -- ^ something interesting happened, with the given set + | UsedCoVars !FreeCoVarsHoles + -- ^ something interesting happened, with the given sets -- of free covars. NB: UsedCoVars <empty> is *not* the same -- as JustZonked! instance Semigroup UsedCoVars where - JustZonked <> JustZonked = JustZonked - UsedCoVars cvs <> JustZonked = UsedCoVars cvs - JustZonked <> UsedCoVars cvs = UsedCoVars cvs - UsedCoVars cvs1 <> UsedCoVars cvs2 = UsedCoVars (cvs1 `unionDVarSet` cvs2) + JustZonked <> JustZonked = JustZonked + other <> JustZonked = other + JustZonked <> other = other + UsedCoVars vs1 <> UsedCoVars vs2 = UsedCoVars (vs1 `mappend` vs2) instance Monoid UsedCoVars where mempty = JustZonked coercionUsedCoVars :: Coercion -> UsedCoVars coercionUsedCoVars co | isReflCo co = JustZonked - | otherwise = UsedCoVars (coVarsOfCoDSet co) + | otherwise = UsedCoVars (coVarsHolesOfCo co) rewrite_zapped :: Type -> RewriteM (Xi, UsedCoVars) @@ -1173,7 +1174,7 @@ rewrite_zapped (TyVarTy tv) ; when wrw $ recordRewriter ctev ; (xi, ucv) <- bumpDepth $ rewrite_zapped rhs_ty - ; return (xi, ucv `mappend` UsedCoVars (coVarsOfCoDSet (ctEvCoercion ctev))) } + ; return (xi, ucv `mappend` coercionUsedCoVars (ctEvCoercion ctev)) } ; _ -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv ; return (mkTyVarTy tv', JustZonked) }}}}} @@ -1201,8 +1202,15 @@ rewrite_zapped (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 <- setEqRel NomEq $ liftA3 (,,) (rewrite_zapped mult) (rewrite_zapped arg_rep) (rewrite_zapped res_rep) - ; let arg_ki_co = build_zapped_mco arg_rep arg_rep_xi ucv4 - res_ki_co = build_zapped_mco res_rep res_rep_xi ucv5 + ; let arg_rr_mco = build_zapped_mco arg_rep arg_rep_xi ucv4 + res_rr_mco = build_zapped_mco res_rep res_rep_xi ucv5 + + mk_TYPE_mco MRefl = MRefl + mk_TYPE_mco (MCo rr_co) = MCo (mkTyConAppCo Nominal tYPETyCon [rr_co]) + + arg_ki_co = mk_TYPE_mco arg_rr_mco + res_ki_co = mk_TYPE_mco res_rr_mco + ; return ( mkFunTy vis mult_xi (xi1 `mkCastTyMCo` arg_ki_co) (xi2 `mkCastTyMCo` res_ki_co) , mconcat [ucv1, ucv2, ucv3, ucv4, ucv5] ) } @@ -1431,7 +1439,7 @@ rewrite_args_slow_zapped orig_binders orig_inner_ki fvs orig_roles orig_tys build_zapped_mco :: Kind -> Kind -> UsedCoVars -> MCoercionN build_zapped_mco _ki1 _ki2 JustZonked = MRefl build_zapped_mco ki1 ki2 _ | ki1 `eqType` ki2 = MRefl -build_zapped_mco ki1 ki2 (UsedCoVars cvs) = MCo $ mkZappedCo Nominal ki1 ki2 cvs +build_zapped_mco ki1 ki2 (UsedCoVars vs) = MCo $ mkZappedCo Nominal ki1 ki2 vs build_zapped_co :: Role -> Type -> Type -> UsedCoVars -> Coercion build_zapped_co r t1 t2 ucv @@ -1439,4 +1447,6 @@ build_zapped_co r t1 t2 ucv | otherwise = mkReflCo r t2 -- t2 is more zonked, generally -- TODO (RAE): Make mode where both rewriters run, comparing the results --- TODO (RAE): Fix rw in HEAD
\ No newline at end of file +-- TODO (RAE): Fix rw in HEAD +-- TODO (RAE): Make reduction strict in HEAD +-- TODO (RAE): Make reduction use MCo in HEAD
\ No newline at end of file diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 4f69413a86..038fc5027b 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -1581,15 +1581,11 @@ collect_cand_qtvs_co orig_ty bound = go_co go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2] go_co dv (KindCo co) = go_co dv co go_co dv (SubCo co) = go_co dv co + go_co dv (HoleCo hole) = go_hole dv hole go_co dv (ZappedCo _ t1 t2 vs) = do dv1 <- collect_cand_qtvs orig_ty True bound dv t1 dv2 <- collect_cand_qtvs orig_ty True bound dv1 t2 - foldlM go_cv dv2 vs - - go_co dv (HoleCo hole) - = do m_co <- unpackCoercionHole_maybe hole - case m_co of - Just co -> go_co dv co - Nothing -> go_cv dv (coHoleCoVar hole) + dv3 <- foldlM go_cv dv2 (freeCoVars vs) + foldlM go_hole dv3 (freeCoHoles vs) go_co dv (CoVarCo cv) = go_cv dv cv @@ -1615,6 +1611,13 @@ collect_cand_qtvs_co orig_ty bound = go_co (dv { dv_cvs = cvs `extendVarSet` cv }) (idType cv) + go_hole :: CandidatesQTvs -> CoercionHole -> TcM CandidatesQTvs + go_hole dv hole = do + m_co <- unpackCoercionHole_maybe hole + case m_co of + Just co -> go_co dv co + Nothing -> go_cv dv (coHoleCoVar hole) + is_bound tv = tv `elemVarSet` bound {- Note [Order of accumulation] diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index b0af88d813..6a0380469b 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -1911,10 +1911,15 @@ zonkScaledTcTypeToTypeX env (Scaled m ty) = Scaled <$> zonkTcTypeToTypeX env m zonkTcTypeToTypeX :: ZonkEnv -> TcType -> TcM Type zonkTcTypesToTypesX :: ZonkEnv -> [TcType] -> TcM [Type] -zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion -(zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo, _) +zonkCoToCo_, zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion -- "RAE" +(zonkTcTypeToTypeX, zonkTcTypesToTypesX, zonkCoToCo_, _) = mapTyCoX zonk_tycomapper +zonkCoToCo env co = do { traceTc "RAE1" (ppr co) + ; co' <- zonkCoToCo_ env co + ; traceTc "RAE2" (ppr co') + ; return co' } + zonkScaledTcTypesToTypesX :: ZonkEnv -> [Scaled TcType] -> TcM [Scaled Type] zonkScaledTcTypesToTypesX env scaled_tys = mapM (zonkScaledTcTypeToTypeX env) scaled_tys diff --git a/compiler/GHC/Types/Unique/DSet.hs b/compiler/GHC/Types/Unique/DSet.hs index d1602e2c6e..c67a183e3c 100644 --- a/compiler/GHC/Types/Unique/DSet.hs +++ b/compiler/GHC/Types/Unique/DSet.hs @@ -33,7 +33,8 @@ module GHC.Types.Unique.DSet ( lookupUniqDSet, uniqDSetToList, partitionUniqDSet, - mapUniqDSet + mapUniqDSet, + seqUniqDSet, ) where import GHC.Prelude @@ -45,6 +46,7 @@ import GHC.Types.Unique import Data.Coerce import Data.Data +import qualified Data.Semigroup -- See Note [UniqSet invariant] in GHC.Types.Unique.Set for why we want a newtype here. -- Beyond preserving invariants, we may also want to 'override' typeclass @@ -53,6 +55,12 @@ import Data.Data newtype UniqDSet a = UniqDSet {getUniqDSet' :: UniqDFM a a} deriving (Data) +instance Semigroup (UniqDSet a) where + (<>) = unionUniqDSets + +instance Monoid (UniqDSet a) where + mempty = emptyUniqDSet + instance Foldable UniqDSet where foldr f z = foldr f z . uniqDSetToList @@ -143,3 +151,6 @@ instance Outputable a => Outputable (UniqDSet a) where pprUniqDSet :: (a -> SDoc) -> UniqDSet a -> SDoc pprUniqDSet f = braces . pprWithCommas f . uniqDSetToList + +seqUniqDSet :: UniqDSet a -> () +seqUniqDSet set = sizeUniqDSet set `seq` ()
\ No newline at end of file diff --git a/testsuite/tests/dependent/should_compile/T14729.stderr b/testsuite/tests/dependent/should_compile/T14729.stderr index ac0108be7c..3155500ff7 100644 --- a/testsuite/tests/dependent/should_compile/T14729.stderr +++ b/testsuite/tests/dependent/should_compile/T14729.stderr @@ -1,5 +1,7 @@ TYPE SIGNATURES - x :: forall (x :: Bool). P (F Int) (x |> Sym (T14729.D:R:FInt[0])) + x :: + forall (x :: Bool). + P (F Int) (x |> Sym (Zapped nominal (F Int) Bool {} [])) y :: forall {x :: Bool}. P Bool x TYPE CONSTRUCTORS type family F{1} :: * -> * diff --git a/testsuite/tests/rep-poly/T20363_show_co.stderr b/testsuite/tests/rep-poly/T20363_show_co.stderr index 6b18496208..b213307622 100644 --- a/testsuite/tests/rep-poly/T20363_show_co.stderr +++ b/testsuite/tests/rep-poly/T20363_show_co.stderr @@ -3,8 +3,8 @@ T20363_show_co.hs:23:10: error: • The newtype constructor pattern does not have a fixed runtime representation. Its type is: - ((# #) |> (TYPE (Sym (T20363_show_co.D:R:NilRep[0])))_N) :: TYPE - NilRep + ((# #) |> (TYPE + (Sym (Zapped nominal NilRep ZeroBitRep {} [])))_N) :: TYPE NilRep NB: GHC does not (yet) support rewriting in runtime representations. Please comment on GHC ticket #13105 if this is causing you trouble. <https://gitlab.haskell.org/ghc/ghc/-/issues/13105> |