diff options
| -rw-r--r-- | compiler/backpack/RnModIface.hs | 9 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreFVs.hs | 8 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreLint.hs | 25 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreOpt.hs | 2 | ||||
| -rw-r--r-- | compiler/iface/IfaceSyn.hs | 10 | ||||
| -rw-r--r-- | compiler/iface/IfaceType.hs | 106 | ||||
| -rw-r--r-- | compiler/iface/TcIface.hs | 8 | ||||
| -rw-r--r-- | compiler/iface/ToIface.hs | 7 | ||||
| -rw-r--r-- | compiler/typecheck/TcCanonical.hs | 21 | ||||
| -rw-r--r-- | compiler/typecheck/TcEvidence.hs | 14 | ||||
| -rw-r--r-- | compiler/typecheck/TcFlatten.hs | 85 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyDecls.hs | 9 | ||||
| -rw-r--r-- | compiler/typecheck/TcType.hs | 7 | ||||
| -rw-r--r-- | compiler/typecheck/TcUnify.hs | 12 | ||||
| -rw-r--r-- | compiler/typecheck/TcValidity.hs | 8 | ||||
| -rw-r--r-- | compiler/types/Coercion.hs | 334 | ||||
| -rw-r--r-- | compiler/types/Coercion.hs-boot | 4 | ||||
| -rw-r--r-- | compiler/types/FamInstEnv.hs | 16 | ||||
| -rw-r--r-- | compiler/types/OptCoercion.hs | 101 | ||||
| -rw-r--r-- | compiler/types/TyCoRep.hs | 118 | ||||
| -rw-r--r-- | compiler/types/TyCoRep.hs-boot | 3 | ||||
| -rw-r--r-- | compiler/types/Type.hs | 54 | ||||
| -rw-r--r-- | compiler/types/Unify.hs | 49 | ||||
| -rw-r--r-- | testsuite/tests/perf/compiler/all.T | 3 |
24 files changed, 637 insertions, 376 deletions
diff --git a/compiler/backpack/RnModIface.hs b/compiler/backpack/RnModIface.hs index f807b39ce8..6b958df760 100644 --- a/compiler/backpack/RnModIface.hs +++ b/compiler/backpack/RnModIface.hs @@ -641,8 +641,14 @@ rnIfaceLetBndr (IfLetBndr fs ty info jpi) rnIfaceLamBndr :: Rename IfaceLamBndr rnIfaceLamBndr (bndr, oneshot) = (,) <$> rnIfaceBndr bndr <*> pure oneshot +rnIfaceMCo :: Rename IfaceMCoercion +rnIfaceMCo IfaceMRefl = pure IfaceMRefl +rnIfaceMCo (IfaceMCo co) = IfaceMCo <$> rnIfaceCo co + rnIfaceCo :: Rename IfaceCoercion -rnIfaceCo (IfaceReflCo role ty) = IfaceReflCo role <$> rnIfaceType ty +rnIfaceCo (IfaceReflCo ty) = IfaceReflCo <$> rnIfaceType ty +rnIfaceCo (IfaceGReflCo role ty mco) + = IfaceGReflCo role <$> rnIfaceType ty <*> rnIfaceMCo mco rnIfaceCo (IfaceFunCo role co1 co2) = IfaceFunCo role <$> rnIfaceCo co1 <*> rnIfaceCo co2 rnIfaceCo (IfaceTyConAppCo role tc cos) @@ -670,7 +676,6 @@ rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c rnIfaceCo (IfaceAxiomRuleCo ax cos) = IfaceAxiomRuleCo ax <$> mapM rnIfaceCo cos rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c -rnIfaceCo (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo <$> rnIfaceCo c1 <*> rnIfaceCo c2 rnIfaceTyCon :: Rename IfaceTyCon rnIfaceTyCon (IfaceTyCon n info) diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs index a7a96e2fcd..607fb73bbe 100644 --- a/compiler/coreSyn/CoreFVs.hs +++ b/compiler/coreSyn/CoreFVs.hs @@ -366,8 +366,13 @@ orphNamesOfThings f = foldr (unionNameSet . f) emptyNameSet orphNamesOfTypes :: [Type] -> NameSet orphNamesOfTypes = orphNamesOfThings orphNamesOfType +orphNamesOfMCo :: MCoercion -> NameSet +orphNamesOfMCo MRefl = emptyNameSet +orphNamesOfMCo (MCo co) = orphNamesOfCo co + orphNamesOfCo :: Coercion -> NameSet -orphNamesOfCo (Refl _ ty) = orphNamesOfType ty +orphNamesOfCo (Refl ty) = orphNamesOfType ty +orphNamesOfCo (GRefl _ ty mco) = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 orphNamesOfCo (ForAllCo _ kind_co co) @@ -381,7 +386,6 @@ orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNames orphNamesOfCo (NthCo _ _ co) = orphNamesOfCo co orphNamesOfCo (LRCo _ co) = orphNamesOfCo co orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg -orphNamesOfCo (CoherenceCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2 orphNamesOfCo (KindCo co) = orphNamesOfCo co orphNamesOfCo (SubCo co) = orphNamesOfCo co orphNamesOfCo (AxiomRuleCo _ cs) = orphNamesOfCos cs diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 93826f5862..6dee383cd9 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -1617,15 +1617,28 @@ lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, Linted -- -- If lintCoercion co = (k1, k2, s1, s2, r) -- then co :: s1 ~r s2 --- s1 :: k2 +-- s1 :: k1 -- s2 :: k2 -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintCoercion (Refl r ty) +lintCoercion (Refl ty) + = do { k <- lintType ty + ; return (k, k, ty, ty, Nominal) } + +lintCoercion (GRefl r ty MRefl) = do { k <- lintType ty ; return (k, k, ty, ty, r) } +lintCoercion (GRefl r ty (MCo co)) + = do { k <- lintType ty + ; (_, _, k1, k2, r') <- lintCoercion co + ; ensureEqTys k k1 + (hang (text "GRefl coercion kind mis-match:" <+> ppr co) + 2 (vcat [ppr ty, ppr k, ppr k1])) + ; lintRole co Nominal r' + ; return (k1, k2, ty, mkCastTy ty co, r) } + lintCoercion co@(TyConAppCo r tc cos) | tc `hasKey` funTyConKey , [_rep1,_rep2,_co1,_co2] <- cos @@ -1646,7 +1659,7 @@ lintCoercion co@(TyConAppCo r tc cos) lintCoercion co@(AppCo co1 co2) | TyConAppCo {} <- co1 = failWithL (text "TyConAppCo to the left of AppCo:" <+> ppr co) - | Refl _ (TyConApp {}) <- co1 + | Just (TyConApp {}, _) <- isReflCo_maybe co1 = failWithL (text "Refl (TyConApp ...) to the left of AppCo:" <+> ppr co) | otherwise = do { (k1, k2, s1, s2, r1) <- lintCoercion co1 @@ -1884,12 +1897,6 @@ lintCoercion co@(AxiomInstCo con ind cos) ; return (extendTCvSubst subst_l ktv s', extendTCvSubst subst_r ktv t') } -lintCoercion (CoherenceCo co1 co2) - = do { (_, k2, t1, t2, r) <- lintCoercion co1 - ; let lhsty = mkCastTy t1 co2 - ; k1' <- lintType lhsty - ; return (k1', k2, lhsty, t2, r) } - lintCoercion (KindCo co) = do { (k1, k2, _, _, _) <- lintCoercion co ; return (liftedTypeKind, liftedTypeKind, k1, k2, Nominal) } diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs index 0353ab6a75..8684c84515 100644 --- a/compiler/coreSyn/CoreOpt.hs +++ b/compiler/coreSyn/CoreOpt.hs @@ -995,7 +995,7 @@ pushCoTyArg co ty -- kinds of the types related by a coercion between forall-types. -- See the NthCo case in CoreLint. - co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) co1) + co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1) -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ] -- Arg of mkInstCo is always nominal, hence mkNomReflCo diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 778e8d637d..4a2d228bef 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -1425,8 +1425,14 @@ freeNamesIfType (IfaceDFunTy s t) = freeNamesIfType s &&& freeNamesIfType t freeNamesIfType (IfaceCastTy t c) = freeNamesIfType t &&& freeNamesIfCoercion c freeNamesIfType (IfaceCoercionTy c) = freeNamesIfCoercion c +freeNamesIfMCoercion :: IfaceMCoercion -> NameSet +freeNamesIfMCoercion IfaceMRefl = emptyNameSet +freeNamesIfMCoercion (IfaceMCo co) = freeNamesIfCoercion co + freeNamesIfCoercion :: IfaceCoercion -> NameSet -freeNamesIfCoercion (IfaceReflCo _ t) = freeNamesIfType t +freeNamesIfCoercion (IfaceReflCo t) = freeNamesIfType t +freeNamesIfCoercion (IfaceGReflCo _ t mco) + = freeNamesIfType t &&& freeNamesIfMCoercion mco freeNamesIfCoercion (IfaceFunCo _ c1 c2) = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2 freeNamesIfCoercion (IfaceTyConAppCo _ tc cos) @@ -1452,8 +1458,6 @@ freeNamesIfCoercion (IfaceLRCo _ co) = freeNamesIfCoercion co freeNamesIfCoercion (IfaceInstCo co co2) = freeNamesIfCoercion co &&& freeNamesIfCoercion co2 -freeNamesIfCoercion (IfaceCoherenceCo c1 c2) - = freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2 freeNamesIfCoercion (IfaceKindCo c) = freeNamesIfCoercion c freeNamesIfCoercion (IfaceSubCo co) diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 5a7f761d32..e3866f5e6d 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -14,6 +14,7 @@ module IfaceType ( IfExtName, IfLclName, IfaceType(..), IfacePredType, IfaceKind, IfaceCoercion(..), + IfaceMCoercion(..), IfaceUnivCoProv(..), IfaceTyCon(..), IfaceTyConInfo(..), IfaceTyConSort(..), IsPromoted(..), IfaceTyLit(..), IfaceTcArgs(..), @@ -280,8 +281,13 @@ data IfaceTyConInfo -- Used to guide pretty-printing , ifaceTyConSort :: IfaceTyConSort } deriving (Eq) +data IfaceMCoercion + = IfaceMRefl + | IfaceMCo IfaceCoercion + data IfaceCoercion - = IfaceReflCo Role IfaceType + = IfaceReflCo IfaceType + | IfaceGReflCo Role IfaceType (IfaceMCoercion) | IfaceFunCo Role IfaceCoercion IfaceCoercion | IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion] | IfaceAppCo IfaceCoercion IfaceCoercion @@ -298,7 +304,6 @@ data IfaceCoercion | IfaceNthCo Int IfaceCoercion | IfaceLRCo LeftOrRight IfaceCoercion | IfaceInstCo IfaceCoercion IfaceCoercion - | IfaceCoherenceCo IfaceCoercion IfaceCoercion | IfaceKindCo IfaceCoercion | IfaceSubCo IfaceCoercion | IfaceFreeCoVar CoVar -- See Note [Free tyvars in IfaceType] @@ -457,8 +462,12 @@ substIfaceType env ty go (IfaceCastTy ty co) = IfaceCastTy (go ty) (go_co co) go (IfaceCoercionTy co) = IfaceCoercionTy (go_co co) - go_co (IfaceReflCo r ty) = IfaceReflCo r (go ty) - go_co (IfaceFunCo r c1 c2) = IfaceFunCo r (go_co c1) (go_co c2) + go_mco IfaceMRefl = IfaceMRefl + go_mco (IfaceMCo co) = IfaceMCo $ go_co co + + go_co (IfaceReflCo ty) = IfaceReflCo (go ty) + go_co (IfaceGReflCo r ty mco) = IfaceGReflCo r (go ty) (go_mco mco) + go_co (IfaceFunCo r c1 c2) = IfaceFunCo r (go_co c1) (go_co c2) go_co (IfaceTyConAppCo r tc cos) = IfaceTyConAppCo r tc (go_cos cos) go_co (IfaceAppCo c1 c2) = IfaceAppCo (go_co c1) (go_co c2) go_co (IfaceForAllCo {}) = pprPanic "substIfaceCoercion" (ppr ty) @@ -472,7 +481,6 @@ substIfaceType env ty go_co (IfaceNthCo n co) = IfaceNthCo n (go_co co) go_co (IfaceLRCo lr co) = IfaceLRCo lr (go_co co) go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2) - go_co (IfaceCoherenceCo c1 c2) = IfaceCoherenceCo (go_co c1) (go_co c2) go_co (IfaceKindCo co) = IfaceKindCo (go_co co) go_co (IfaceSubCo co) = IfaceSubCo (go_co co) go_co (IfaceAxiomRuleCo n cos) = IfaceAxiomRuleCo n (go_cos cos) @@ -1197,7 +1205,12 @@ pprIfaceCoercion = ppr_co topPrec pprParendIfaceCoercion = ppr_co appPrec ppr_co :: PprPrec -> IfaceCoercion -> SDoc -ppr_co _ (IfaceReflCo r ty) = angleBrackets (ppr ty) <> ppr_role r +ppr_co _ (IfaceReflCo ty) = angleBrackets (ppr ty) <> ppr_role Nominal +ppr_co _ (IfaceGReflCo r ty IfaceMRefl) + = angleBrackets (ppr ty) <> ppr_role r +ppr_co ctxt_prec (IfaceGReflCo r ty (IfaceMCo co)) + = ppr_special_co ctxt_prec + (text "GRefl" <+> ppr r <+> pprParendIfaceType ty) [co] ppr_co ctxt_prec (IfaceFunCo r co1 co2) = maybeParen ctxt_prec funPrec $ sep (ppr_co funPrec co1 : ppr_fun_tail co2) @@ -1258,8 +1271,6 @@ ppr_co ctxt_prec (IfaceLRCo lr co) = ppr_special_co ctxt_prec (ppr lr) [co] ppr_co ctxt_prec (IfaceSubCo co) = ppr_special_co ctxt_prec (text "Sub") [co] -ppr_co ctxt_prec (IfaceCoherenceCo co1 co2) - = ppr_special_co ctxt_prec (text "Coh") [co1,co2] ppr_co ctxt_prec (IfaceKindCo co) = ppr_special_co ctxt_prec (text "Kind") [co] @@ -1490,64 +1501,79 @@ instance Binary IfaceType where _ -> do n <- get bh return (IfaceLitTy n) +instance Binary IfaceMCoercion where + put_ bh IfaceMRefl = do + putByte bh 1 + put_ bh (IfaceMCo co) = do + putByte bh 2 + put_ bh co + + get bh = do + tag <- getByte bh + case tag of + 1 -> return IfaceMRefl + 2 -> do a <- get bh + return $ IfaceMCo a + _ -> panic ("get IfaceMCoercion " ++ show tag) + instance Binary IfaceCoercion where - put_ bh (IfaceReflCo a b) = do + put_ bh (IfaceReflCo a) = do putByte bh 1 put_ bh a + put_ bh (IfaceGReflCo a b c) = do + putByte bh 2 + put_ bh a put_ bh b + put_ bh c put_ bh (IfaceFunCo a b c) = do - putByte bh 2 + putByte bh 3 put_ bh a put_ bh b put_ bh c put_ bh (IfaceTyConAppCo a b c) = do - putByte bh 3 + putByte bh 4 put_ bh a put_ bh b put_ bh c put_ bh (IfaceAppCo a b) = do - putByte bh 4 + putByte bh 5 put_ bh a put_ bh b put_ bh (IfaceForAllCo a b c) = do - putByte bh 5 + putByte bh 6 put_ bh a put_ bh b put_ bh c put_ bh (IfaceCoVarCo a) = do - putByte bh 6 + putByte bh 7 put_ bh a put_ bh (IfaceAxiomInstCo a b c) = do - putByte bh 7 + putByte bh 8 put_ bh a put_ bh b put_ bh c put_ bh (IfaceUnivCo a b c d) = do - putByte bh 8 + putByte bh 9 put_ bh a put_ bh b put_ bh c put_ bh d put_ bh (IfaceSymCo a) = do - putByte bh 9 - put_ bh a - put_ bh (IfaceTransCo a b) = do putByte bh 10 put_ bh a - put_ bh b - put_ bh (IfaceNthCo a b) = do + put_ bh (IfaceTransCo a b) = do putByte bh 11 put_ bh a put_ bh b - put_ bh (IfaceLRCo a b) = do + put_ bh (IfaceNthCo a b) = do putByte bh 12 put_ bh a put_ bh b - put_ bh (IfaceInstCo a b) = do + put_ bh (IfaceLRCo a b) = do putByte bh 13 put_ bh a put_ bh b - put_ bh (IfaceCoherenceCo a b) = do + put_ bh (IfaceInstCo a b) = do putByte bh 14 put_ bh a put_ bh b @@ -1571,51 +1597,51 @@ instance Binary IfaceCoercion where tag <- getByte bh case tag of 1 -> do a <- get bh - b <- get bh - return $ IfaceReflCo a b + return $ IfaceReflCo a 2 -> do a <- get bh b <- get bh c <- get bh - return $ IfaceFunCo a b c + return $ IfaceGReflCo a b c 3 -> do a <- get bh b <- get bh c <- get bh - return $ IfaceTyConAppCo a b c + return $ IfaceFunCo a b c 4 -> do a <- get bh b <- get bh - return $ IfaceAppCo a b + c <- get bh + return $ IfaceTyConAppCo a b c 5 -> do a <- get bh b <- get bh + return $ IfaceAppCo a b + 6 -> do a <- get bh + b <- get bh c <- get bh return $ IfaceForAllCo a b c - 6 -> do a <- get bh - return $ IfaceCoVarCo a 7 -> do a <- get bh + return $ IfaceCoVarCo a + 8 -> do a <- get bh b <- get bh c <- get bh return $ IfaceAxiomInstCo a b c - 8 -> do a <- get bh + 9 -> do a <- get bh b <- get bh c <- get bh d <- get bh return $ IfaceUnivCo a b c d - 9 -> do a <- get bh - return $ IfaceSymCo a 10-> do a <- get bh - b <- get bh - return $ IfaceTransCo a b + return $ IfaceSymCo a 11-> do a <- get bh b <- get bh - return $ IfaceNthCo a b + return $ IfaceTransCo a b 12-> do a <- get bh b <- get bh - return $ IfaceLRCo a b + return $ IfaceNthCo a b 13-> do a <- get bh b <- get bh - return $ IfaceInstCo a b + return $ IfaceLRCo a b 14-> do a <- get bh b <- get bh - return $ IfaceCoherenceCo a b + return $ IfaceInstCo a b 15-> do a <- get bh return $ IfaceKindCo a 16-> do a <- get bh diff --git a/compiler/iface/TcIface.hs b/compiler/iface/TcIface.hs index bffda71f0a..58bcd8c281 100644 --- a/compiler/iface/TcIface.hs +++ b/compiler/iface/TcIface.hs @@ -1199,7 +1199,11 @@ tcIfaceTyLit (IfaceStrTyLit n) = return (StrTyLit n) tcIfaceCo :: IfaceCoercion -> IfL Coercion tcIfaceCo = go where - go (IfaceReflCo r t) = Refl r <$> tcIfaceType t + go_mco IfaceMRefl = pure MRefl + go_mco (IfaceMCo co) = MCo <$> (go co) + + go (IfaceReflCo t) = Refl <$> tcIfaceType t + go (IfaceGReflCo r t mco) = GRefl r <$> tcIfaceType t <*> go_mco mco go (IfaceFunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2 go (IfaceTyConAppCo r tc cs) = TyConAppCo r <$> tcIfaceTyCon tc <*> mapM go cs @@ -1219,8 +1223,6 @@ tcIfaceCo = go go (IfaceNthCo d c) = do { c' <- go c ; return $ mkNthCo (nthCoRole d c') d c' } go (IfaceLRCo lr c) = LRCo lr <$> go c - go (IfaceCoherenceCo c1 c2) = CoherenceCo <$> go c1 - <*> go c2 go (IfaceKindCo c) = KindCo <$> go c go (IfaceSubCo c) = SubCo <$> go c go (IfaceAxiomRuleCo ax cos) = AxiomRuleCo <$> tcIfaceCoAxiomRule ax diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs index 4b810fa687..291aea36a7 100644 --- a/compiler/iface/ToIface.hs +++ b/compiler/iface/ToIface.hs @@ -221,7 +221,11 @@ toIfaceCoercionX :: VarSet -> Coercion -> IfaceCoercion toIfaceCoercionX fr co = go co where - go (Refl r ty) = IfaceReflCo r (toIfaceTypeX fr ty) + go_mco MRefl = IfaceMRefl + go_mco (MCo co) = IfaceMCo $ go co + + go (Refl ty) = IfaceReflCo (toIfaceTypeX fr ty) + go (GRefl r ty mco) = IfaceGReflCo r (toIfaceTypeX fr ty) (go_mco mco) go (CoVarCo cv) -- See [TcTyVars in IfaceType] in IfaceType | cv `elemVarSet` fr = IfaceFreeCoVar cv @@ -234,7 +238,6 @@ toIfaceCoercionX fr co go (NthCo _r d co) = IfaceNthCo d (go co) go (LRCo lr co) = IfaceLRCo lr (go co) go (InstCo co arg) = IfaceInstCo (go co) (go arg) - go (CoherenceCo c1 c2) = IfaceCoherenceCo (go c1) (go c2) go (KindCo c) = IfaceKindCo (go c) go (SubCo co) = IfaceSubCo (go co) go (AxiomRuleCo co cs) = IfaceAxiomRuleCo (coaxrName co) (map go cs) diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index a8fff6b767..42f28c7c2b 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -1291,7 +1291,7 @@ canEqCast flat ev eq_rel swapped ty1 co1 ty2 ps_ty2 , ppr ty1 <+> text "|>" <+> ppr co1 , ppr ps_ty2 ]) ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2 - (mkTcReflCo role ty1 `mkTcCoherenceRightCo` co1) + (mkTcGReflRightCo role ty1 co1) (mkTcReflCo role ps_ty2) ; can_eq_nc flat new_ev eq_rel ty1 ty1 ty2 ps_ty2 } where @@ -1737,7 +1737,10 @@ canCFunEqCan ev fn tys fsk -- new_co :: F tys' ~ new_fsk -- co :: F tys ~ (new_fsk |> kind_co) co = mkTcSymCo lhs_co `mkTcTransCo` - (new_co `mkTcCoherenceRightCo` kind_co) + mkTcCoherenceRightCo Nominal + (mkTyVarTy new_fsk) + kind_co + new_co ; traceTcS "Discharging fmv/fsk due to hetero flattening" (ppr ev) ; dischargeFunEq ev fsk co xi @@ -1788,7 +1791,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 new_rhs = xi2 `mkCastTy` rhs_kind_co ps_rhs = ps_xi2 `mkCastTy` rhs_kind_co - rhs_co = mkTcReflCo role xi2 `mkTcCoherenceLeftCo` rhs_kind_co + rhs_co = mkTcGReflLeftCo role xi2 rhs_kind_co ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs (mkTcReflCo role xi1) rhs_co @@ -1803,8 +1806,8 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 new_rhs = xi2 `mkCastTy` sym_k2_co -- :: flat_k2 ps_rhs = ps_xi2 `mkCastTy` sym_k2_co - lhs_co = mkReflCo role xi1 `mkTcCoherenceLeftCo` sym_k1_co - rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` sym_k2_co + lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co + rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co -- lhs_co :: (xi1 |> sym k1_co) ~ xi1 -- rhs_co :: (xi2 |> sym k2_co) ~ xi2 @@ -1841,11 +1844,11 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2 homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1 rhs' = mkCastTy xi2 homo_co -- :: kind(tv1) ps_rhs' = mkCastTy ps_xi2 homo_co -- :: kind(tv1) - rhs_co = mkReflCo role xi2 `mkTcCoherenceLeftCo` homo_co + rhs_co = mkTcGReflLeftCo role xi2 homo_co -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2 lhs' = mkTyVarTy tv1 -- :: kind(tv1) - lhs_co = mkReflCo role lhs' `mkTcCoherenceRightCo` co1 + lhs_co = mkTcGReflRightCo role lhs' co1 -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1) ; traceTcS "Hetero equality gives rise to given kind equality" @@ -1895,10 +1898,10 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 ty2 _ sym_co2 = mkTcSymCo co2 ty1 = mkTyVarTy tv1 new_lhs = ty1 `mkCastTy` sym_co2 - lhs_co = mkReflCo role ty1 `mkTcCoherenceLeftCo` sym_co2 + lhs_co = mkTcGReflLeftCo role ty1 sym_co2 new_rhs = mkTyVarTy tv2 - rhs_co = mkReflCo role new_rhs `mkTcCoherenceRightCo` co2 + rhs_co = mkTcGReflRightCo role new_rhs co2 ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 66fcb7a589..50c49bc65a 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -35,7 +35,9 @@ module TcEvidence ( mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos, mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo, tcDowngradeRole, - mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo, + mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflLeftCo, mkTcPhantomCo, + mkTcCoherenceLeftCo, + mkTcCoherenceRightCo, mkTcKindCo, tcCoercionKind, coVarsOfTcCo, mkTcCoVarCo, @@ -115,8 +117,12 @@ mkTcSubCo :: TcCoercionN -> TcCoercionR maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR -mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion -mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion +mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion +mkTcGReflLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion +mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercionN + -> TcCoercion -> TcCoercion +mkTcCoherenceRightCo :: Role -> TcType -> TcCoercionN + -> TcCoercion -> TcCoercion mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP mkTcKindCo :: TcCoercion -> TcCoercionN mkTcCoVarCo :: CoVar -> TcCoercion @@ -148,6 +154,8 @@ mkTcSubCo = mkSubCo maybeTcSubCo = maybeSubCo tcDowngradeRole = downgradeRole mkTcAxiomRuleCo = mkAxiomRuleCo +mkTcGReflRightCo = mkGReflRightCo +mkTcGReflLeftCo = mkGReflLeftCo mkTcCoherenceLeftCo = mkCoherenceLeftCo mkTcCoherenceRightCo = mkCoherenceRightCo mkTcPhantomCo = mkPhantomCo diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index f6a1adf45e..ee13091681 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -1115,6 +1115,17 @@ as desired. (Why do we want Star? Because we started with something of kind Star Whew. +Note [flatten_exact_fam_app_fully performance] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The refactor of GRefl seems to cause performance trouble for T9872x: the allocation of flatten_exact_fam_app_fully_performance increased. See note [Generalized reflexive coercion] in TyCoRep for more information about GRefl and Trac #15192 for the current state. + +The explicit pattern match in homogenise_result helps with T9872a, b, c. + +Still, it increases the expected allocation of T9872d by ~2%. + +TODO: a step-by-step replay of the refactor to analyze the performance. + -} {-# INLINE flatten_args_tc #-} @@ -1208,12 +1219,12 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys -- -- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder) -- casted_xi = xi `mkCastTy` kind_co - -- casted_co = co `mkTcCoherenceLeftCo` kind_co + -- casted_co = xi |> kind_co ~r xi ; co -- -- but this isn't necessary: -- mkTcSymCo (Refl a b) = Refl a b, -- mkCastTy x (Refl _ _) = x - -- mkTcCoherenceLeftCo x (Refl _ _) = x + -- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co -- -- Also, no need to check isAnonTyBinder or isNamedTyBinder, since -- we've already established that they're all anonymous. @@ -1229,7 +1240,7 @@ flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys finish (xis, cos, binders) = (xis, cos, kind_co) where final_kind = mkPiTys binders orig_inner_ki - kind_co = mkReflCo Nominal final_kind + kind_co = mkNomReflCo final_kind {-# INLINE flatten_args_slow #-} -- | Slow path, compared to flatten_args_fast, because this one must track @@ -1283,7 +1294,7 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys ; let kind_co = mkTcSymCo $ liftCoSubst Nominal lc (tyBinderType binder) !casted_xi = xi `mkCastTy` kind_co - casted_co = co `mkTcCoherenceLeftCo` kind_co + casted_co = mkTcCoherenceLeftCo role xi kind_co co -- now, extend the lifting context with the new binding !new_lc | Just tv <- tyBinderVar_maybe binder @@ -1314,13 +1325,13 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys <- go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_tys -- cos_out :: xis_out ~ casted_tys -- we need to return cos :: xis_out ~ tys - -- - -- zipWith has the map first because it will fuse. - ; let cos = zipWith (flip mkTcCoherenceRightCo) - (map mkTcSymCo arg_cos) - cos_out + ; let cos = zipWith3 mkTcGReflRightCo + roles + casted_tys + (map mkTcSymCo arg_cos) + cos' = zipWith mkTransCo cos_out cos - ; return (xis_out, cos, res_co_out `mkTcTransCo` res_co) } + ; return (xis_out, cos', res_co_out `mkTcTransCo` res_co) } go _ _ _ _ _ _ _ = pprPanic "flatten_args wandered into deeper water than usual" (vcat []) @@ -1408,7 +1419,8 @@ flatten_one (CastTy ty g) = do { (xi, co) <- flatten_one ty ; (g', _) <- flatten_co g - ; return (mkCastTy xi g', castCoercionKind co g' g) } + ; role <- getRole + ; return (mkCastTy xi g', castCoercionKind co role xi ty g' g) } flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co @@ -1471,7 +1483,8 @@ flatten_app_ty_args fun_xi fun_co arg_tys arg_co = mkAppCos fun_co arg_cos ; return (arg_xi, arg_co, kind_co) } - ; return (homogenise_result xi co kind_co) } + ; role <- getRole + ; return (homogenise_result xi co role kind_co) } flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion) flatten_ty_con_app tc tys @@ -1479,18 +1492,21 @@ flatten_ty_con_app tc tys ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys ; let tyconapp_xi = mkTyConApp tc xis tyconapp_co = mkTyConAppCo role tc cos - ; return (homogenise_result tyconapp_xi tyconapp_co kind_co) } + ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) } -- Make the result of flattening homogeneous (Note [Flattening] (F2)) homogenise_result :: Xi -- a flattened type - -> Coercion -- :: xi ~ original ty + -> Coercion -- :: xi ~r original ty + -> Role -- r -> CoercionN -- kind_co :: typeKind(xi) ~N typeKind(ty) -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co) - -- ~ original ty) -homogenise_result xi co kind_co - = let xi' = xi `mkCastTy` kind_co - co' = co `mkTcCoherenceLeftCo` kind_co - in (xi', co') + -- ~r original ty) +homogenise_result xi co r kind_co + -- the explicit pattern match here improves the performance of T9872a, b, c by + -- ~2% + | isGReflCo kind_co = (xi `mkCastTy` kind_co, co) + | otherwise = (xi `mkCastTy` kind_co + , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co) {-# INLINE homogenise_result #-} -- Flatten a vector (list of arguments). @@ -1588,6 +1604,7 @@ flatten_fam_app tc tys -- Can be over-saturated ; flatten_app_ty_args xi1 co1 tys_rest } } } -- the [TcType] exactly saturate the TyCon +-- See note [flatten_exact_fam_app_fully performance] flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion) flatten_exact_fam_app_fully tc tys -- See Note [Reduce type family applications eagerly] @@ -1625,10 +1642,10 @@ flatten_exact_fam_app_fully tc tys -- flatten it -- fsk_co :: fsk_xi ~ fsk ; let xi = fsk_xi `mkCastTy` kind_co - co' = (fsk_co `mkTcCoherenceLeftCo` kind_co) - `mkTransCo` - maybeSubCo eq_rel (mkSymCo co) - `mkTransCo` ret_co + co' = mkTcCoherenceLeftCo role fsk_xi kind_co fsk_co + `mkTransCo` + maybeSubCo eq_rel (mkSymCo co) + `mkTransCo` ret_co ; return (xi, co') } -- :: fsk_xi ~ F xis @@ -1658,12 +1675,12 @@ flatten_exact_fam_app_fully tc tys ; traceFlat "flatten/flat-cache miss" $ (ppr tc <+> ppr xis $$ ppr fsk $$ ppr ev) - -- NB: fsk's kind is already flattend because + -- NB: fsk's kind is already flattened because -- the xis are flattened - ; let xi = mkTyVarTy fsk `mkCastTy` kind_co - co' = (maybeSubCo eq_rel (mkSymCo co) - `mkTcCoherenceLeftCo` kind_co) - `mkTransCo` ret_co + ; let fsk_ty = mkTyVarTy fsk + xi = fsk_ty `mkCastTy` kind_co + co' = mkTcCoherenceLeftCo role fsk_ty kind_co (maybeSubCo eq_rel (mkSymCo co)) + `mkTransCo` ret_co ; return (xi, co') } } @@ -1707,9 +1724,10 @@ flatten_exact_fam_app_fully tc tys ; when (eq_rel == NomEq) $ liftTcS $ extendFlatCache tc tys ( co, xi, flavour ) - ; let xi' = xi `mkCastTy` kind_co - co' = update_co $ mkSymCo co - `mkTcCoherenceLeftCo` kind_co + ; let role = eqRelRole eq_rel + xi' = xi `mkCastTy` kind_co + co' = update_co $ + mkTcCoherenceLeftCo role xi kind_co (mkSymCo co) ; return $ Just (xi', co') } Nothing -> pure Nothing } @@ -1735,9 +1753,10 @@ flatten_exact_fam_app_fully tc tys ; eq_rel <- getEqRel ; let co = maybeSubCo eq_rel norm_co `mkTransCo` mkSymCo final_co + role = eqRelRole eq_rel xi' = xi `mkCastTy` kind_co - co' = update_co $ mkSymCo co - `mkTcCoherenceLeftCo` kind_co + co' = update_co $ + mkTcCoherenceLeftCo role xi kind_co (mkSymCo co) ; return $ Just (xi', co') } Nothing -> pure Nothing } diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index cce0f02a0b..f64b9f3e73 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -32,7 +32,7 @@ import GhcPrelude import TcRnMonad import TcEnv import TcBinds( tcValBinds, addTypecheckedBinds ) -import TyCoRep( Type(..), Coercion(..), UnivCoProvenance(..) ) +import TyCoRep( Type(..), Coercion(..), MCoercion(..), UnivCoProvenance(..) ) import TcType import TysWiredIn( unitTy ) import MkCore( rEC_SEL_ERROR_ID ) @@ -111,7 +111,11 @@ synonymTyConsOfType ty -- in the same recursive group. Possibly this restriction will be -- lifted in the future but for now, this code is "just for completeness -- sake". - go_co (Refl _ ty) = go ty + go_mco MRefl = emptyNameEnv + go_mco (MCo co) = go_co co + + go_co (Refl ty) = go ty + go_co (GRefl _ ty mco) = go ty `plusNameEnv` go_mco mco go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs go_co (AppCo co co') = go_co co `plusNameEnv` go_co co' go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co' @@ -125,7 +129,6 @@ synonymTyConsOfType ty go_co (NthCo _ _ co) = go_co co go_co (LRCo _ co) = go_co co go_co (InstCo co co') = go_co co `plusNameEnv` go_co co' - go_co (CoherenceCo co co') = go_co co `plusNameEnv` go_co co' go_co (KindCo co) = go_co co go_co (SubCo co) = go_co co go_co (AxiomRuleCo _ cs) = go_co_s cs diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 092c5a1923..00bae72117 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -936,7 +936,11 @@ exactTyCoVarsOfType ty go (CastTy ty co) = go ty `unionVarSet` goCo co go (CoercionTy co) = goCo co - goCo (Refl _ ty) = go ty + goMCo MRefl = emptyVarSet + goMCo (MCo co) = goCo co + + goCo (Refl ty) = go ty + goCo (GRefl _ ty mco) = go ty `unionVarSet` goMCo mco goCo (TyConAppCo _ _ args)= goCos args goCo (AppCo co arg) = goCo co `unionVarSet` goCo arg goCo (ForAllCo tv k_co co) @@ -951,7 +955,6 @@ exactTyCoVarsOfType ty goCo (NthCo _ _ co) = goCo co goCo (LRCo _ co) = goCo co goCo (InstCo co arg) = goCo co `unionVarSet` goCo arg - goCo (CoherenceCo c1 c2) = goCo c1 `unionVarSet` goCo c2 goCo (KindCo co) = goCo co goCo (SubCo co) = goCo co goCo (AxiomRuleCo _ c) = goCos c diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index eb44bc385f..08a5c59879 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -971,7 +971,7 @@ promoteTcType dest_lvl ty , uo_thing = Nothing , uo_visible = False } ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind - ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co + ; let co = mkTcGReflRightCo Nominal ty ki_co ; return (co, ty `mkCastTy` ki_co) } {- Note [Promoting a type] @@ -1265,7 +1265,7 @@ uType, uType_defer -> CtOrigin -> TcType -- ty1 is the *actual* type -> TcType -- ty2 is the *expected* type - -> TcM Coercion + -> TcM CoercionN -------------- -- It is always safe to defer unification to the main constraint solver @@ -1300,7 +1300,7 @@ uType t_or_k origin orig_ty1 orig_ty2 else traceTc "u_tys yields coercion:" (ppr co) ; return co } where - go :: TcType -> TcType -> TcM Coercion + go :: TcType -> TcType -> TcM CoercionN -- The arguments to 'go' are always semantically identical -- to orig_ty{1,2} except for looking through type synonyms @@ -1324,15 +1324,15 @@ uType t_or_k origin orig_ty1 orig_ty2 -- See Note [Expanding synonyms during unification] go ty1@(TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 - = return $ mkReflCo Nominal ty1 + = return $ mkNomReflCo ty1 go (CastTy t1 co1) t2 = do { co_tys <- go t1 t2 - ; return (mkCoherenceLeftCo co_tys co1) } + ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) } go t1 (CastTy t2 co2) = do { co_tys <- go t1 t2 - ; return (mkCoherenceRightCo co_tys co2) } + ; return ( mkCoherenceRightCo Nominal t2 co2 co_tys) } -- See Note [Expanding synonyms during unification] -- diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 60fb2618c3..d51fa9d4b6 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -2030,8 +2030,13 @@ fvType (CoercionTy co) = fvCo co fvTypes :: [Type] -> [TyVar] fvTypes tys = concat (map fvType tys) +fvMCo :: MCoercion -> [TyCoVar] +fvMCo MRefl = [] +fvMCo (MCo co) = fvCo co + fvCo :: Coercion -> [TyCoVar] -fvCo (Refl _ ty) = fvType ty +fvCo (Refl ty) = fvType ty +fvCo (GRefl _ ty mco) = fvType ty ++ fvMCo mco fvCo (TyConAppCo _ _ args) = concatMap fvCo args fvCo (AppCo co arg) = fvCo co ++ fvCo arg fvCo (ForAllCo tv h co) = filter (/= tv) (fvCo co) ++ fvCo h @@ -2044,7 +2049,6 @@ fvCo (TransCo co1 co2) = fvCo co1 ++ fvCo co2 fvCo (NthCo _ _ co) = fvCo co fvCo (LRCo _ co) = fvCo co fvCo (InstCo co arg) = fvCo co ++ fvCo arg -fvCo (CoherenceCo co1 co2) = fvCo co1 ++ fvCo co2 fvCo (KindCo co) = fvCo co fvCo (SubCo co) = fvCo co fvCo (AxiomRuleCo _ cs) = concatMap fvCo cs diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 346190c7a7..8493a4ae82 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -23,7 +23,7 @@ module Coercion ( coercionRole, coercionKindRole, -- ** Constructing coercions - mkReflCo, mkRepReflCo, mkNomReflCo, + mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo, mkCoVarCo, mkCoVarCos, mkAxInstCo, mkUnbranchedAxInstCo, mkAxInstRHS, mkUnbranchedAxInstRHS, @@ -37,8 +37,8 @@ module Coercion ( mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo, mkAxiomInstCo, mkProofIrrelCo, downgradeRole, maybeSubCo, mkAxiomRuleCo, - mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo, - mkKindCo, castCoercionKind, + mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo, + mkKindCo, castCoercionKind, castCoercionKindI, mkHeteroCoercionType, @@ -59,7 +59,7 @@ module Coercion ( pickLR, - isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe, + isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe, isReflCoVar_maybe, -- ** Coercion variables @@ -295,13 +295,14 @@ decomposePiCos orig_kind orig_args orig_co = go [] orig_subst orig_kind orig_arg -> ([CoercionN], Coercion) go acc_arg_cos subst ki (ty:tys) co | Just (kv, inner_ki) <- splitForAllTy_maybe ki - -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2) - -- function :: forall a:s1.t1 (the function is not passed to decomposePiCos) - -- ty :: s2 - -- need arg_co :: s2 ~ s1 - -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b] + -- know co :: (forall a:s1.t1) ~ (forall b:s2.t2) + -- function :: forall a:s1.t1 + -- (the function is not passed to decomposePiCos) + -- ty :: s2 + -- need arg_co :: s2 ~ s1 + -- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b] = let arg_co = mkNthCo Nominal 0 (mkSymCo co) - res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co) + res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co) subst' = extendTCvSubst subst kv ty in go (arg_co : acc_arg_cos) subst' inner_ki tys res_co @@ -337,7 +338,8 @@ getCoVar_maybe _ = Nothing -- | Attempts to tease a coercion apart into a type constructor and the application -- of a number of coercion arguments to that constructor splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion]) -splitTyConAppCo_maybe (Refl r ty) +splitTyConAppCo_maybe co + | Just (ty, r) <- isReflCo_maybe co = do { (tc, tys) <- splitTyConApp_maybe ty ; let args = zipWith mkReflCo (tyConRolesX r tc) tys ; return (tc, args) } @@ -363,8 +365,9 @@ splitAppCo_maybe (TyConAppCo r tc args) -- Use mkTyConAppCo to preserve the invariant -- that identity coercions are always represented by Refl -splitAppCo_maybe (Refl r ty) - | Just (ty1, ty2) <- splitAppTy_maybe ty +splitAppCo_maybe co + | Just (ty, r) <- isReflCo_maybe co + , Just (ty1, ty2) <- splitAppTy_maybe ty = Just (mkReflCo r ty1, mkNomReflCo ty2) splitAppCo_maybe _ = Nothing @@ -446,23 +449,46 @@ isReflCoVar_maybe cv | isCoVar cv , Pair ty1 ty2 <- coVarTypes cv , ty1 `eqType` ty2 - = Just (Refl (coVarRole cv) ty1) + = Just (mkReflCo (coVarRole cv) ty1) | otherwise = Nothing +-- | Tests if this coercion is obviously a generalized reflexive coercion. +-- Guaranteed to work very quickly. +isGReflCo :: Coercion -> Bool +isGReflCo (GRefl{}) = True +isGReflCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl +isGReflCo _ = False + +-- | Tests if this MCoercion is obviously generalized reflexive +-- Guaranteed to work very quickly. +isGReflMCo :: MCoercion -> Bool +isGReflMCo MRefl = True +isGReflMCo (MCo co) | isGReflCo co = True +isGReflMCo _ = False + -- | Tests if this coercion is obviously reflexive. Guaranteed to work -- very quickly. Sometimes a coercion can be reflexive, but not obviously -- so. c.f. 'isReflexiveCo' isReflCo :: Coercion -> Bool -isReflCo (Refl {}) = True -isReflCo _ = False +isReflCo (Refl{}) = True +isReflCo (GRefl _ _ mco) | isGReflMCo mco = True +isReflCo _ = False + +-- | Returns the type coerced if this coercion is a generalized reflexive +-- coercion. Guaranteed to work very quickly. +isGReflCo_maybe :: Coercion -> Maybe (Type, Role) +isGReflCo_maybe (GRefl r ty _) = Just (ty, r) +isGReflCo_maybe (Refl ty) = Just (ty, Nominal) +isGReflCo_maybe _ = Nothing -- | Returns the type coerced if this coercion is reflexive. Guaranteed -- to work very quickly. Sometimes a coercion can be reflexive, but not -- obviously so. c.f. 'isReflexiveCo_maybe' isReflCo_maybe :: Coercion -> Maybe (Type, Role) -isReflCo_maybe (Refl r ty) = Just (ty, r) -isReflCo_maybe _ = Nothing +isReflCo_maybe (Refl ty) = Just (ty, Nominal) +isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r) +isReflCo_maybe _ = Nothing -- | Slowly checks if the coercion is reflexive. Don't call this in a loop, -- as it walks over the entire coercion. @@ -472,7 +498,8 @@ isReflexiveCo = isJust . isReflexiveCo_maybe -- | Extracts the coerced type from a reflexive coercion. This potentially -- walks over the entire coercion, so avoid doing this in a loop. isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role) -isReflexiveCo_maybe (Refl r ty) = Just (ty, r) +isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal) +isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r) isReflexiveCo_maybe co | ty1 `eqType` ty2 = Just (ty1, r) @@ -542,17 +569,25 @@ role is bizarre and a caller should have to ask for this behavior explicitly. -} +-- | Make a generalized reflexive coercion +mkGReflCo :: Role -> Type -> MCoercionN -> Coercion +mkGReflCo r ty mco + | isGReflMCo mco = if r == Nominal then Refl ty + else GRefl r ty MRefl + | otherwise = GRefl r ty mco + +-- | Make a reflexive coercion mkReflCo :: Role -> Type -> Coercion -mkReflCo r ty - = Refl r ty +mkReflCo Nominal ty = Refl ty +mkReflCo r ty = GRefl r ty MRefl -- | Make a representational reflexive coercion mkRepReflCo :: Type -> Coercion -mkRepReflCo = mkReflCo Representational +mkRepReflCo ty = GRefl Representational ty MRefl -- | Make a nominal reflexive coercion mkNomReflCo :: Type -> Coercion -mkNomReflCo = mkReflCo Nominal +mkNomReflCo = Refl -- | Apply a type constructor to a list of coercions. It is the -- caller's responsibility to get the roles correct on argument coercions. @@ -570,7 +605,8 @@ mkTyConAppCo r tc cos = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos | Just tys_roles <- traverse isReflCo_maybe cos - = Refl r (mkTyConApp tc (map fst tys_roles)) -- See Note [Refl invariant] + = mkReflCo r (mkTyConApp tc (map fst tys_roles)) + -- See Note [Refl invariant] | otherwise = TyConAppCo r tc cos @@ -581,7 +617,7 @@ mkFunCo r co1 co2 -- See Note [Refl invariant] | Just (ty1, _) <- isReflCo_maybe co1 , Just (ty2, _) <- isReflCo_maybe co2 - = Refl r (mkFunTy ty1 ty2) + = mkReflCo r (mkFunTy ty1 ty2) | otherwise = FunCo r co1 co2 -- | Apply a 'Coercion' to another 'Coercion'. @@ -590,11 +626,13 @@ mkFunCo r co1 co2 mkAppCo :: Coercion -- ^ :: t1 ~r t2 -> Coercion -- ^ :: s1 ~N s2, where s1 :: k1, s2 :: k2 -> Coercion -- ^ :: t1 s1 ~r t2 s2 -mkAppCo (Refl r ty1) arg - | Just (ty2, _) <- isReflCo_maybe arg - = Refl r (mkAppTy ty1 ty2) +mkAppCo co arg + | Just (ty1, r) <- isReflCo_maybe co + , Just (ty2, _) <- isReflCo_maybe arg + = mkReflCo r (mkAppTy ty1 ty2) - | Just (tc, tys) <- splitTyConApp_maybe ty1 + | Just (ty1, r) <- isReflCo_maybe co + , Just (tc, tys) <- splitTyConApp_maybe ty1 -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102) = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys) where @@ -687,27 +725,31 @@ mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3 -- The kind of the tyvar should be the left-hand kind of the kind coercion. mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion mkForAllCo tv kind_co co - | Refl r ty <- co - , Refl {} <- kind_co - = Refl r (mkInvForAllTy tv ty) + | Just (ty, r) <- isReflCo_maybe co + , isGReflCo kind_co + = mkReflCo r (mkInvForAllTy tv ty) | otherwise = ForAllCo tv kind_co co -- | Make nested ForAllCos mkForAllCos :: [(TyVar, Coercion)] -> Coercion -> Coercion -mkForAllCos bndrs (Refl r ty) +mkForAllCos bndrs co + | Just (ty, r ) <- isReflCo_maybe co = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in foldl (flip $ uncurry ForAllCo) - (Refl r $ mkInvForAllTys (reverse (map fst refls_rev'd)) ty) + (mkReflCo r (mkInvForAllTys (reverse (map fst refls_rev'd)) ty)) non_refls_rev'd -mkForAllCos bndrs co = foldr (uncurry ForAllCo) co bndrs + | otherwise + = foldr (uncurry ForAllCo) co bndrs -- | Make a Coercion quantified over a type variable; -- the variable has the same type in both sides of the coercion mkHomoForAllCos :: [TyVar] -> Coercion -> Coercion -mkHomoForAllCos tvs (Refl r ty) - = Refl r (mkInvForAllTys tvs ty) -mkHomoForAllCos tvs ty = mkHomoForAllCos_NoRefl tvs ty +mkHomoForAllCos tvs co + | Just (ty, r) <- isReflCo_maybe co + = mkReflCo r (mkInvForAllTys tvs ty) + | otherwise + = mkHomoForAllCos_NoRefl tvs co -- | Like 'mkHomoForAllCos', but doesn't check if the inner coercion -- is reflexive. @@ -834,7 +876,7 @@ mkUnivCo :: UnivCoProvenance -> Type -- ^ t2 :: k2 -> Coercion -- ^ :: t1 ~r t2 mkUnivCo prov role ty1 ty2 - | ty1 `eqType` ty2 = Refl role ty1 + | ty1 `eqType` ty2 = mkReflCo role ty1 | otherwise = UnivCo prov role ty1 ty2 -- | Create a symmetric version of the given 'Coercion' that asserts @@ -844,7 +886,7 @@ mkSymCo :: Coercion -> Coercion -- Do a few simple optimizations, but don't bother pushing occurrences -- of symmetry to the leaves; the optimizer will take care of that. -mkSymCo co@(Refl {}) = co +mkSymCo co | isReflCo co = co mkSymCo (SymCo co) = co mkSymCo (SubCo (SymCo co)) = SubCo co mkSymCo co = SymCo co @@ -852,9 +894,11 @@ mkSymCo co = SymCo co -- | Create a new 'Coercion' by composing the two given 'Coercion's transitively. -- (co1 ; co2) mkTransCo :: Coercion -> Coercion -> Coercion -mkTransCo co1 (Refl {}) = co1 -mkTransCo (Refl {}) co2 = co2 -mkTransCo co1 co2 = TransCo co1 co2 +mkTransCo co1 co2 | isReflCo co1 = co2 + | isReflCo co2 = co1 +mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2)) + = GRefl r t1 (MCo $ mkTransCo co1 co2) +mkTransCo co1 co2 = TransCo co1 co2 mkNthCo :: HasDebugCallStack => Role -- the role of the coercion you're creating @@ -867,17 +911,19 @@ mkNthCo r n co where Pair ty1 ty2 = coercionKind co - go r 0 (Refl _ ty) - | Just (tv, _) <- splitForAllTy_maybe ty + go r 0 co + | Just (ty, _) <- isReflCo_maybe co + , Just (tv, _) <- splitForAllTy_maybe ty = ASSERT( r == Nominal ) - Refl r (tyVarKind tv) - go r n (Refl r0 ty) + mkReflCo r (tyVarKind tv) + + go r n co + | Just (ty, r0) <- isReflCo_maybe co + , let tc = tyConAppTyCon ty = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty ) ASSERT( nthRole r0 tc n == r ) mkReflCo r (tyConAppArgN n ty) - where tc = tyConAppTyCon ty - - ok_tc_app :: Type -> Int -> Bool + where ok_tc_app :: Type -> Int -> Bool ok_tc_app ty n | Just (_, tys) <- splitTyConApp_maybe ty = tys `lengthExceeds` n @@ -978,43 +1024,59 @@ nthCoRole n co (Pair lty _, r) = coercionKindRole co mkLRCo :: LeftOrRight -> Coercion -> Coercion -mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty)) -mkLRCo lr co = LRCo lr co +mkLRCo lr co + | Just (ty, eq) <- isReflCo_maybe co + = mkReflCo eq (pickLR lr (splitAppTy ty)) + | otherwise + = LRCo lr co -- | Instantiates a 'Coercion'. mkInstCo :: Coercion -> Coercion -> Coercion -mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg) +mkInstCo (ForAllCo tv _kind_co body_co) co + | Just (arg, _) <- isReflCo_maybe co = substCoWithUnchecked [tv] [arg] body_co mkInstCo co arg = InstCo co arg --- This could work harder to produce Refl coercions, but that would be --- quite inefficient. Seems better not to try. -mkCoherenceCo :: Coercion -> Coercion -> Coercion -mkCoherenceCo co1 (Refl {}) = co1 -mkCoherenceCo (CoherenceCo co1 co2) co3 - = CoherenceCo co1 (co2 `mkTransCo` co3) -mkCoherenceCo co1 co2 = CoherenceCo co1 co2 - --- | A CoherenceCo c1 c2 applies the coercion c2 to the left-hand type --- in the kind of c1. This function uses sym to get the coercion on the --- right-hand type of c1. Thus, if c1 :: s ~ t, then mkCoherenceRightCo c1 c2 --- has the kind (s ~ (t |> c2)) down through type constructors. --- The second coercion must be representational. -mkCoherenceRightCo :: Coercion -> Coercion -> Coercion -mkCoherenceRightCo c1 c2 = mkSymCo (mkCoherenceCo (mkSymCo c1) c2) - --- | An explicitly directed synonym of mkCoherenceCo. The second --- coercion must be representational. -mkCoherenceLeftCo :: Coercion -> Coercion -> Coercion -mkCoherenceLeftCo = mkCoherenceCo - -infixl 5 `mkCoherenceCo` -infixl 5 `mkCoherenceRightCo` -infixl 5 `mkCoherenceLeftCo` +-- | Given @ty :: k1@, @co :: k1 ~ k2@, +-- produces @co' :: ty ~r (ty |> co)@ +mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion +mkGReflRightCo r ty co + | isGReflCo co = mkReflCo r ty + -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@ + -- instead of @isReflCo@ + | otherwise = GRefl r ty (MCo co) + +-- | Given @ty :: k1@, @co :: k1 ~ k2@, +-- produces @co' :: (ty |> co) ~r ty@ +mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion +mkGReflLeftCo r ty co + | isGReflCo co = mkReflCo r ty + -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@ + -- instead of @isReflCo@ + | otherwise = mkSymCo $ GRefl r ty (MCo co) + +-- | Given @ty :: k2@, @co :: k1 ~ k2@, @co2:: ty ~ ty'@, +-- produces @co' :: (ty |> co) ~r ty' +-- It is not only a utility function, but it saves allocation when co +-- is a GRefl coercion. +mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion +mkCoherenceLeftCo r ty co co2 + | isGReflCo co = co2 + | otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2 + +-- | Given @ty :: k2@, @co :: k1 ~ k2@, @co2:: ty' ~ ty@, +-- produces @co' :: ty' ~r (ty |> co) +-- It is not only a utility function, but it saves allocation when co +-- is a GRefl coercion. +mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion +mkCoherenceRightCo r ty co co2 + | isGReflCo co = co2 + | otherwise = co2 `mkTransCo` GRefl r ty (MCo co) -- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@. mkKindCo :: Coercion -> Coercion -mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty) +mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty) +mkKindCo (GRefl _ _ (MCo co)) = co mkKindCo (UnivCo (PhantomProv h) _ _ _) = h mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h mkKindCo co @@ -1025,14 +1087,15 @@ mkKindCo co , let tk1 = typeKind ty1 tk2 = typeKind ty2 , tk1 `eqType` tk2 - = Refl Nominal tk1 + = Refl tk1 | otherwise = KindCo co mkSubCo :: Coercion -> Coercion -- Input coercion is Nominal, result is Representational -- see also Note [Role twiddling functions] -mkSubCo (Refl Nominal ty) = Refl Representational ty +mkSubCo (Refl ty) = GRefl Representational ty MRefl +mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co mkSubCo (TyConAppCo Nominal tc cos) = TyConAppCo Representational tc (applyRoles tc cos) mkSubCo (FunCo Nominal arg res) @@ -1088,9 +1151,10 @@ mkProofIrrelCo :: Role -- ^ role of the created coercion, "r" -- if the two coercion prove the same fact, I just don't care what -- the individual coercions are. -mkProofIrrelCo r (Refl {}) g _ = Refl r (CoercionTy g) -mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r - (mkCoercionTy g1) (mkCoercionTy g2) +mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy g) + -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@ +mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r + (mkCoercionTy g1) (mkCoercionTy g2) {- %************************************************************************ @@ -1109,7 +1173,8 @@ setNominalRole_maybe r co | otherwise = setNominalRole_maybe_helper co where setNominalRole_maybe_helper (SubCo co) = Just co - setNominalRole_maybe_helper (Refl _ ty) = Just $ Refl Nominal ty + setNominalRole_maybe_helper co@(Refl _) = Just co + setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co setNominalRole_maybe_helper (TyConAppCo Representational tc cos) = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos ; return $ TyConAppCo Nominal tc cos' } @@ -1132,8 +1197,6 @@ setNominalRole_maybe r co = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co setNominalRole_maybe_helper (InstCo co arg) = InstCo <$> setNominalRole_maybe_helper co <*> pure arg - setNominalRole_maybe_helper (CoherenceCo co1 co2) - = CoherenceCo <$> setNominalRole_maybe_helper co1 <*> pure co2 setNominalRole_maybe_helper (UnivCo prov _ co1 co2) | case prov of UnsafeCoerceProv -> True -- it's always unsafe PhantomProv _ -> False -- should always be phantom @@ -1200,8 +1263,13 @@ promoteCoercion co = case co of -- The ASSERT( False )s throughout -- are these cases explicitly, but they should never fire. - Refl _ ty -> ASSERT( False ) - mkNomReflCo (typeKind ty) + Refl _ -> ASSERT( False ) + mkNomReflCo ki1 + + GRefl _ _ MRefl -> ASSERT( False ) + mkNomReflCo ki1 + + GRefl _ _ (MCo co) -> co TyConAppCo _ tc args | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args @@ -1262,9 +1330,6 @@ promoteCoercion co = case co of InstCo g _ -> promoteCoercion g - CoherenceCo g h - -> mkSymCo h `mkTransCo` promoteCoercion g - KindCo _ -> ASSERT( False ) mkNomReflCo liftedTypeKind @@ -1308,11 +1373,24 @@ instCoercions g ws ; return (piResultTy <$> g_tys <*> w_tys, g') } -- | Creates a new coercion with both of its types casted by different casts --- castCoercionKind g h1 h2, where g :: t1 ~ t2, has type (t1 |> h1) ~ (t2 |> h2) --- The second and third coercions must be nominal. -castCoercionKind :: Coercion -> Coercion -> Coercion -> Coercion -castCoercionKind g h1 h2 - = g `mkCoherenceLeftCo` h1 `mkCoherenceRightCo` h2 +-- @castCoercionKind g r t1 t2 h1 h2@, where @g :: t1 ~r t2@, +-- has type @(t1 |> h1) ~r (t2 |> h2)@. +-- @h1@ and @h2@ must be nominal. +castCoercionKind :: Coercion -> Role -> Type -> Type + -> CoercionN -> CoercionN -> Coercion +castCoercionKind g r t1 t2 h1 h2 + = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g) + +-- | Creates a new coercion with both of its types casted by different casts +-- @castCoercionKind g h1 h2@, where @g :: t1 ~r t2@, +-- has type @(t1 |> h1) ~r (t2 |> h2)@. +-- @h1@ and @h2@ must be nominal. +-- It calls @coercionKindRole@, so it's quite inefficient (which 'I' stands for) +-- Use @castCoercionKind@ instead if @t1@, @t2@, and @r@ are known beforehand. +castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion +castCoercionKindI g h1 h2 + = mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g) + where (Pair t1 t2, r) = coercionKindRole g -- See note [Newtype coercions] in TyCon @@ -1499,8 +1577,8 @@ eqCoercionX env = eqTypeX env `on` coercionType Note [Lifting coercions over types: liftCoSubst] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The KPUSH rule deals with this situation - data T a = MkK (a -> Maybe a) - g :: T t1 ~ K t2 + data T a = K (a -> Maybe a) + g :: T t1 ~ T t2 x :: t1 -> Maybe t1 case (K @t1 x) |> g of @@ -1563,7 +1641,7 @@ liftCoSubstWith r tvs cos ty -- types of the mapped coercions in @lc@, and similar for @lc_right@. liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion liftCoSubst r lc@(LC subst env) ty - | isEmptyVarEnv env = Refl r (substTy subst ty) + | isEmptyVarEnv env = mkReflCo r (substTy subst ty) | otherwise = ty_co_subst lc r ty emptyLiftingContext :: InScopeSet -> LiftingContext @@ -1583,8 +1661,10 @@ extendLiftingContext :: LiftingContext -- ^ original LC -> Coercion -- ^ ...to this lifted version -> LiftingContext -- mappings to reflexive coercions are just substitutions -extendLiftingContext (LC subst env) tv (Refl _ ty) = LC (extendTvSubst subst tv ty) env extendLiftingContext (LC subst env) tv arg + | Just (ty, _) <- isReflCo_maybe arg + = LC (extendTvSubst subst tv ty) env + | otherwise = ASSERT( isTyVar tv ) LC subst (extendVarEnv env tv arg) @@ -1611,9 +1691,10 @@ extendLiftingContextEx lc@(LC subst env) ((v,ty):rest) -- works with existentially bound variables, which are considered to have -- nominal roles. = let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty) - (extendVarEnv env v (mkSymCo $ mkCoherenceCo - (mkNomReflCo ty) - (ty_co_subst lc Nominal (tyVarKind v)))) + (extendVarEnv env v $ + mkGReflRightCo Nominal + ty + (ty_co_subst lc Nominal (tyVarKind v))) in extendLiftingContextEx lc' rest -- | Erase the environments in a lifting context @@ -1651,9 +1732,9 @@ ty_co_subst lc role ty = let (lc', v', h) = liftCoSubstVarBndr lc v in mkForAllCo v' h $! ty_co_subst lc' r ty go r ty@(LitTy {}) = ASSERT( r == Nominal ) - mkReflCo r ty - go r (CastTy ty co) = castCoercionKind (go r ty) (substLeftCo lc co) - (substRightCo lc co) + mkNomReflCo ty + go r (CastTy ty co) = castCoercionKindI (go r ty) (substLeftCo lc co) + (substRightCo lc co) go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co) (substRightCo lc co) where kco = go Nominal (coercionType co) @@ -1682,7 +1763,7 @@ liftCoSubstTyVar (LC subst env) r v = downgradeRole_maybe r (coercionRole co_arg) co_arg | otherwise - = Just $ Refl r (substTyVar subst v) + = Just $ mkReflCo r (substTyVar subst v) liftCoSubstVarBndr :: LiftingContext -> TyVar -> (LiftingContext, TyVar, Coercion) @@ -1705,7 +1786,7 @@ liftCoSubstVarBndrUsing fun lc@(LC subst cenv) old_var Pair k1 _ = coercionKind eta new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1) - lifted = Refl Nominal (TyVarTy new_var) + lifted = Refl (TyVarTy new_var) new_cenv = extendVarEnv cenv old_var lifted -- | Is a var in the domain of a lifting context? @@ -1776,8 +1857,13 @@ lcInScopeSet (LC subst _) = getTCvInScope subst %************************************************************************ -} +seqMCo :: MCoercion -> () +seqMCo MRefl = () +seqMCo (MCo co) = seqCo co + seqCo :: Coercion -> () -seqCo (Refl r ty) = r `seq` seqType ty +seqCo (Refl ty) = seqType ty +seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2 seqCo (ForAllCo tv k co) = seqType (tyVarKind tv) `seq` seqCo k @@ -1793,7 +1879,6 @@ seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2 seqCo (NthCo r n co) = r `seq` n `seq` seqCo co seqCo (LRCo lr co) = lr `seq` seqCo co seqCo (InstCo co arg) = seqCo co `seq` seqCo arg -seqCo (CoherenceCo co1 co2) = seqCo co1 `seq` seqCo co2 seqCo (KindCo co) = seqCo co seqCo (SubCo co) = seqCo co seqCo (AxiomRuleCo _ cs) = seqCos cs @@ -1844,11 +1929,14 @@ coercionKind :: Coercion -> Pair Type coercionKind co = go co where - go (Refl _ ty) = Pair ty ty + go (Refl ty) = Pair ty ty + go (GRefl _ ty MRefl) = Pair ty ty + go (GRefl _ ty (MCo co1)) = Pair ty (mkCastTy ty co1) go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos) go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2 go co@(ForAllCo tv1 k_co co1) - | isReflCo k_co = mkInvForAllTy tv1 <$> go co1 + | isGReflCo k_co = mkInvForAllTy tv1 <$> go co1 + -- kind_co always has kind @Type@, thus @isGReflCo@ | otherwise = go_forall empty_subst co where empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co) @@ -1889,9 +1977,6 @@ coercionKind co = tys = go co go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co go (InstCo aco arg) = go_app aco [arg] - go (CoherenceCo g h) - = let Pair ty1 ty2 = go g in - Pair (mkCastTy ty1 h) ty2 go (KindCo co) = typeKind <$> go co go (SubCo co) = go co go (AxiomRuleCo ax cos) = expectJust "coercionKind" $ @@ -1909,9 +1994,10 @@ coercionKind co = where Pair _ k2 = go k_co tv2 = setTyVarKind tv1 (substTy subst k2) - subst' | isReflCo k_co = extendTCvInScope subst tv1 - | otherwise = extendTvSubst (extendTCvInScope subst tv2) tv1 $ - TyVarTy tv2 `mkCastTy` mkSymCo k_co + subst' | isGReflCo k_co = extendTCvInScope subst tv1 + -- kind_co always has kind @Type@, thus @isGReflCo@ + | otherwise = extendTvSubst (extendTCvInScope subst tv2) tv1 $ + TyVarTy tv2 `mkCastTy` mkSymCo k_co go_forall subst other_co = substTy subst `pLiftSnd` go other_co @@ -1945,7 +2031,8 @@ coercionKindRole co = (coercionKind co, coercionRole co) coercionRole :: Coercion -> Role coercionRole = go where - go (Refl r _) = r + go (Refl _) = Nominal + go (GRefl r _ _) = r go (TyConAppCo r _ _) = r go (AppCo co1 _) = go co1 go (ForAllCo _ _ co) = go co @@ -1959,7 +2046,6 @@ coercionRole = go go (NthCo r _d _co) = r go (LRCo {}) = Nominal go (InstCo co _) = go co - go (CoherenceCo co1 _) = go co1 go (KindCo {}) = Nominal go (SubCo _) = Representational go (AxiomRuleCo ax _) = coaxrRole ax @@ -1992,10 +2078,14 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 | Just ty2' <- coreView ty2 = go ty1 ty2' go (CastTy ty1 co) ty2 - = go ty1 ty2 `mkCoherenceLeftCo` co + = let co' = go ty1 ty2 + r = coercionRole co' + in mkCoherenceLeftCo r ty1 co co' go ty1 (CastTy ty2 co) - = go ty1 ty2 `mkCoherenceRightCo` co + = let co' = go ty1 ty2 + r = coercionRole co' + in mkCoherenceRightCo r ty2 co co' go ty1@(TyVarTy tv1) _tyvarty = ASSERT( case _tyvarty of diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot index df4a24e5b2..6e6acd752a 100644 --- a/compiler/types/Coercion.hs-boot +++ b/compiler/types/Coercion.hs-boot @@ -28,12 +28,14 @@ mkTransCo :: Coercion -> Coercion -> Coercion mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion mkLRCo :: LeftOrRight -> Coercion -> Coercion mkInstCo :: Coercion -> Coercion -> Coercion -mkCoherenceCo :: Coercion -> Coercion -> Coercion +mkGReflCo :: Role -> Type -> MCoercionN -> Coercion +mkNomReflCo :: Type -> Coercion mkKindCo :: Coercion -> Coercion mkSubCo :: Coercion -> Coercion mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion +isGReflCo :: Coercion -> Bool isReflCo :: Coercion -> Bool isReflexiveCo :: Coercion -> Bool decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion) diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs index 306e1b1034..046edfaa42 100644 --- a/compiler/types/FamInstEnv.hs +++ b/compiler/types/FamInstEnv.hs @@ -1341,15 +1341,15 @@ normaliseType env role ty = initNormM env role (tyCoVarsOfType ty) $ normalise_type ty normalise_type :: Type -- old type - -> NormM (Coercion, Type) -- (coercion,new type), where - -- co :: old-type ~ new_type + -> NormM (Coercion, Type) -- (coercion, new type), where + -- co :: old-type ~ new_type -- Normalise the input type, by eliminating *all* type-function redexes -- but *not* newtypes (which are visible to the programmer) -- Returns with Refl if nothing happens -- Does nothing to newtypes -- The returned coercion *must* be *homogeneous* -- See Note [Normalising types] --- Try to not to disturb type synonyms if possible +-- Try not to disturb type synonyms if possible normalise_type ty = go ty @@ -1376,7 +1376,8 @@ normalise_type ty = do { (nco, nty) <- go ty ; lc <- getLC ; let co' = substRightCo lc co - ; return (castCoercionKind nco co co', mkCastTy nty co') } + ; return (castCoercionKind nco Nominal ty nty co co' + , mkCastTy nty co') } go (CoercionTy co) = do { lc <- getLC ; r <- getRole @@ -1623,7 +1624,11 @@ allTyVarsInTy = go go (CastTy ty co) = go ty `unionVarSet` go_co co go (CoercionTy co) = go_co co - go_co (Refl _ ty) = go ty + go_mco MRefl = emptyVarSet + go_mco (MCo co) = go_co co + + go_co (Refl ty) = go ty + go_co (GRefl _ ty mco) = go ty `unionVarSet` go_mco mco go_co (TyConAppCo _ _ args) = go_cos args go_co (AppCo co arg) = go_co co `unionVarSet` go_co arg go_co (ForAllCo tv h co) @@ -1638,7 +1643,6 @@ allTyVarsInTy = go go_co (NthCo _ _ co) = go_co co go_co (LRCo _ co) = go_co co go_co (InstCo co arg) = go_co co `unionVarSet` go_co arg - go_co (CoherenceCo c1 c2) = go_co c1 `unionVarSet` go_co c2 go_co (KindCo co) = go_co co go_co (SubCo co) = go_co co go_co (AxiomRuleCo _ cs) = go_cos cs diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs index db4bc8c668..70ae469795 100644 --- a/compiler/types/OptCoercion.hs +++ b/compiler/types/OptCoercion.hs @@ -74,7 +74,7 @@ We thus want some coercion proving this: (t1[tv |-> s1]) ~ (t2[tv |-> s2 |> sym h]) If we substitute the *type* tv for the *coercion* -(g2 `mkCoherenceRightCo` sym h) in g, we'll get this result exactly. +(g2 ; t2 ~ t2 |> sym h) in g, we'll get this result exactly. This is bizarre, though, because we're substituting a type variable with a coercion. However, this operation already exists: it's called *lifting*, and defined in Coercion. @@ -170,12 +170,30 @@ opt_co4_wrap env sym rep r co result -} -opt_co4 env _ rep r (Refl _r ty) +opt_co4 env _ rep r (Refl ty) + = ASSERT2( r == Nominal, text "Expected role:" <+> ppr r $$ + text "Found role:" <+> ppr Nominal $$ + text "Type:" <+> ppr ty ) + liftCoSubst (chooseRole rep r) env ty + +opt_co4 env _ rep r (GRefl _r ty MRefl) = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$ text "Found role:" <+> ppr _r $$ text "Type:" <+> ppr ty ) liftCoSubst (chooseRole rep r) env ty +opt_co4 env sym rep r (GRefl _r ty (MCo co)) + = ASSERT2( r == _r, text "Expected role:" <+> ppr r $$ + text "Found role:" <+> ppr _r $$ + text "Type:" <+> ppr ty ) + if isGReflCo co || isGReflCo co' + then liftCoSubst r' env ty + else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty) + where + r' = chooseRole rep r + ty' = substTy (lcSubstLeft env) ty + co' = opt_co4 env False False Nominal co + opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co -- surprisingly, we don't have to do anything to the env here. This is -- because any "lifting" substitutions in the env are tied to ForAllCos, @@ -225,7 +243,7 @@ opt_co4 env sym rep r (CoVarCo cv) = opt_co4_wrap (zapLiftingContext env) sym rep r co | ty1 `eqType` ty2 -- See Note [Optimise CoVarCo to Refl] - = Refl (chooseRole rep r) ty1 + = mkReflCo (chooseRole rep r) ty1 | otherwise = ASSERT( isCoVar cv1 ) @@ -273,11 +291,13 @@ opt_co4 env sym rep r (TransCo co1 co2) co2' = opt_co4_wrap env sym rep r co2 in_scope = lcInScopeSet env -opt_co4 env _sym rep r (NthCo _r n (Refl _r2 ty)) - | Just (_tc, args) <- ASSERT( r == _r ) +opt_co4 env _sym rep r (NthCo _r n co) + | Just (ty, _) <- isReflCo_maybe co + , Just (_tc, args) <- ASSERT( r == _r ) splitTyConApp_maybe ty = liftCoSubst (chooseRole rep r) env (args `getNth` n) - | n == 0 + | Just (ty, _) <- isReflCo_maybe co + , n == 0 , Just (tv, _) <- splitForAllTy_maybe ty = liftCoSubst (chooseRole rep r) env (tyVarKind tv) @@ -330,7 +350,7 @@ opt_co4 env sym rep r (InstCo co1 arg) -- forall over type... | Just (tv, kind_co, co_body) <- splitForAllCo_maybe co1 = opt_co4_wrap (extendLiftingContext env tv - (arg' `mkCoherenceRightCo` mkSymCo kind_co)) + (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) arg')) sym rep r co_body -- See if it is a forall after optimization @@ -339,7 +359,7 @@ opt_co4 env sym rep r (InstCo co1 arg) -- forall over type... | Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1' = opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv' - (arg' `mkCoherenceRightCo` mkSymCo kind_co')) + (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co') arg')) False False r' co_body' | otherwise = InstCo co1' arg' @@ -347,22 +367,7 @@ opt_co4 env sym rep r (InstCo co1 arg) co1' = opt_co4_wrap env sym rep r co1 r' = chooseRole rep r arg' = opt_co4_wrap env sym False Nominal arg - -opt_co4 env sym rep r (CoherenceCo co1 co2) - | TransCo col1 cor1 <- co1 - = opt_co4_wrap env sym rep r (mkTransCo (mkCoherenceCo col1 co2) cor1) - - | TransCo col1' cor1' <- co1' - = if sym then opt_trans in_scope col1' - (optCoercion' (zapTCvSubst (lcTCvSubst env)) - (mkCoherenceRightCo cor1' co2')) - else opt_trans in_scope (mkCoherenceCo col1' co2') cor1' - - | otherwise - = wrapSym sym $ mkCoherenceCo (opt_co4_wrap env False rep r co1) co2' - where co1' = opt_co4_wrap env sym rep r co1 - co2' = opt_co4_wrap env False False Nominal co2 - in_scope = lcInScopeSet env + Pair _ t2 = coercionKind arg' opt_co4 env sym _rep r (KindCo co) = ASSERT( r == Nominal ) @@ -476,12 +481,14 @@ opt_transList is = zipWith (opt_trans is) opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo opt_trans is co1 co2 | isReflCo co1 = co2 + -- optimize when co1 is a Refl Co | otherwise = opt_trans1 is co1 co2 opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo -- First arg is not the identity opt_trans1 is co1 co2 | isReflCo co2 = co1 + -- optimize when co2 is a Refl Co | otherwise = opt_trans2 is co1 co2 opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo @@ -507,6 +514,11 @@ opt_trans2 _ co1 co2 -- Optimize coercions with a top-level use of transitivity. opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo +opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2)) + = ASSERT( r1 == r2 ) + fireTransRule "GRefl" in_co1 in_co2 $ + mkGReflRightCo r1 t1 (opt_trans is co1 co2) + -- Push transitivity through matching destructors opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2) | d1 == d2 @@ -659,18 +671,12 @@ opt_trans_rule is co1 co2 co2_is_axiom_maybe = isAxiom_maybe co2 role = coercionRole co1 -- should be the same as coercionRole co2! -opt_trans_rule is co1 co2 - | Just (lco, lh) <- isCohRight_maybe co1 - , Just (rco, rh) <- isCohLeft_maybe co2 - , (coercionType lh) `eqType` (coercionType rh) - = opt_trans_rule is lco rco - opt_trans_rule _ co1 co2 -- Identity rule | (Pair ty1 _, r) <- coercionKindRole co1 , Pair _ ty2 <- coercionKind co2 , ty1 `eqType` ty2 = fireTransRule "RedTypeDirRefl" co1 co2 $ - Refl r ty2 + mkReflCo r ty2 opt_trans_rule _ _ _ = Nothing @@ -696,19 +702,21 @@ opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs = ASSERT( co1bs `equalLength` co2bs ) fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $ let Pair _ rt1a = coercionKind co1a - Pair lt2a _ = coercionKind co2a + (Pair lt2a _, rt2a) = coercionKindRole co2a Pair _ rt1bs = traverse coercionKind co1bs Pair lt2bs _ = traverse coercionKind co2bs + rt2bs = map coercionRole co2bs kcoa = mkKindCo $ buildCoercion lt2a rt1a kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs - co2a' = mkCoherenceLeftCo co2a kcoa - co2bs' = zipWith mkCoherenceLeftCo co2bs kcobs + co2a' = mkCoherenceLeftCo rt2a lt2a kcoa co2a + co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs + co2bs'' = zipWith mkTransCo co2bs' co2bs in mkAppCos (opt_trans is co1a co2a') - (zipWith (opt_trans is) co1bs co2bs') + (zipWith (opt_trans is) co1bs co2bs'') fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion fireTransRule _rule _co1 _co2 res @@ -820,8 +828,7 @@ This can be done with mkKindCo and buildCoercion. The latter assumes two types are identical modulo casts and builds a coercion between them. Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the -output coercions. These are well-kinded. (We cast the right-hand coercion -because mkCoherenceLeftCo is smaller than mkCoherenceRightCo.) +output coercions. These are well-kinded. Also, note that all of this is done after accumulated any nested AppCo parameters. This step is to avoid quadratic behavior in calling coercionKind. @@ -910,18 +917,6 @@ matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co = Nothing ------------- --- destruct a CoherenceCo -isCohLeft_maybe :: Coercion -> Maybe (Coercion, Coercion) -isCohLeft_maybe (CoherenceCo co1 co2) = Just (co1, co2) -isCohLeft_maybe _ = Nothing - --- destruct a (sym (co1 |> co2)). --- if isCohRight_maybe co = Just (co1, co2), then (sym co1) `mkCohRightCo` co2 = co -isCohRight_maybe :: Coercion -> Maybe (Coercion, Coercion) -isCohRight_maybe (SymCo (CoherenceCo co1 co2)) = Just (mkSymCo co1, co2) -isCohRight_maybe _ = Nothing - -------------- compatible_co :: Coercion -> Coercion -> Bool -- Check whether (co1 . co2) will be well-kinded compatible_co co1 co2 @@ -940,15 +935,15 @@ Suppose we have but g is *not* a ForAllCo. We want to eta-expand it. So, we do this: - g' = all a1:(ForAllKindCo g).(InstCo g (a1 `mkCoherenceRightCo` ForAllKindCo g)) + g' = all a1:(ForAllKindCo g).(InstCo g (a1 ~ a1 |> ForAllKindCo g)) Call the kind coercion h1 and the body coercion h2. We can see that - h2 : t1 ~ t2[a2 |-> (a1 |> h2)] + h2 : t1 ~ t2[a2 |-> (a1 |> h1)] According to the typing rule for ForAllCo, we get that - g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h2)][a1 |-> a1 |> sym h2]) + g' : all a1:k1.t1 ~ all a1:k2.(t2[a2 |-> (a1 |> h1)][a1 |-> a1 |> sym h1]) or @@ -967,7 +962,7 @@ etaForAllCo_maybe co , isForAllTy ty2 , let kind_co = mkNthCo Nominal 0 co = Just ( tv1, kind_co - , mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_co) ) + , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co)) | otherwise = Nothing diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 0ec5888cef..6427917fe5 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -34,7 +34,7 @@ module TyCoRep ( UnivCoProvenance(..), CoercionHole(..), coHoleCoVar, setCoHoleCoVar, CoercionN, CoercionR, CoercionP, KindCoercion, - MCoercion(..), MCoercionR, + MCoercion(..), MCoercionR, MCoercionN, -- * Functions over types mkTyConTy, mkTyVarTy, mkTyVarTys, @@ -861,8 +861,8 @@ data Coercion -- - _ stands for a parameter that is not a Role or Coercion. -- These ones mirror the shape of types - = -- Refl :: "e" -> _ -> e - Refl Role Type -- See Note [Refl invariant] + = -- Refl :: _ -> N + Refl Type -- See Note [Refl invariant] -- Invariant: applications of (Refl T) to a bunch of identity coercions -- always show up as Refl. -- For example (Refl T) (Refl a) (Refl b) shows up as (Refl (T a b)). @@ -873,7 +873,13 @@ data Coercion -- ConAppCo coercions (like all coercions other than Refl) -- are NEVER the identity. - -- Use (Refl Representational _), not (SubCo (Refl Nominal _)) + -- Use (GRefl Representational ty MRefl), not (SubCo (Refl ty)) + + -- GRefl :: "e" -> _ -> Maybe N -> e + -- See Note [Generalized reflexive coercion] + | GRefl Role Type MCoercionN -- See Note [Refl invariant] + -- Use (Refl ty), not (GRefl Nominal ty MRefl) + -- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _)) -- These ones simply lift the correspondingly-named -- Type constructors into Coercions @@ -933,11 +939,6 @@ data Coercion -- :: e -> N -> e -- See Note [InstCo roles] - -- Coherence applies a coercion to the left-hand type of another coercion - -- See Note [Coherence] - | CoherenceCo Coercion KindCoercion - -- :: e -> N -> e - -- Extract a kind coercion from a (heterogeneous) type coercion -- NB: all kind coercions are Nominal | KindCo Coercion @@ -962,7 +963,9 @@ data MCoercion -- A trivial Reflexivity coercion | MCo Coercion -- Other coercions + deriving Data.Data type MCoercionR = MCoercion +type MCoercionN = MCoercion instance Outputable MCoercion where ppr MRefl = text "MRefl" @@ -974,7 +977,7 @@ Note [Refl invariant] Invariant 1: Coercions have the following invariant - Refl is always lifted as far as possible. + Refl (similar for GRefl r ty MRefl) is always lifted as far as possible. You might think that a consequencs is: Every identity coercions has Refl at the root @@ -985,6 +988,42 @@ But that's not quite true because of coercion variables. Consider etc. So the consequence is only true of coercions that have no coercion variables. +Note [Generalized reflexive coercion] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +GRefl is a generalized reflexive coercion (see Trac #15192). It wraps a kind +coercion, which might be reflexive (MRefl) or any coercion (MCo co). The typing +rules for GRefl: + + ty : k1 + ------------------------------------ + GRefl r ty MRefl: ty ~r ty + + ty : k1 co :: k1 ~ k2 + ------------------------------------ + GRefl r ty (MCo co) : ty ~r ty |> co + +Consider we have + + g1 :: s ~r t + s :: k1 + g2 :: k1 ~ k2 + +and we want to construct a coercions co which has type + + (s |> g2) ~r t + +We can define + + co = Sym (GRefl r s g2) ; g1 + +It is easy to see that + + Refl == GRefl Nominal ty MRefl :: ty ~n ty + +A nominal reflexive coercion is quite common, so we keep the special form Refl to +save allocation. + Note [Coercion axioms applied to coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The reason coercion axioms can be applied to coercions and not just @@ -1076,19 +1115,6 @@ add Names to, e.g., VarSets, and there generally is just an impedance mismatch in a bunch of places. So we use tv1. When we need tv2, we can use setTyVarKind. -Note [Coherence] -~~~~~~~~~~~~~~~~ -The Coherence typing rule is thus: - - g1 : s ~ t s : k1 g2 : k1 ~ k2 - ------------------------------------ - CoherenceCo g1 g2 : (s |> g2) ~ t - -While this looks (and is) unsymmetric, a combination of other coercion -combinators can make the symmetric version. - -For role information, see Note [Roles and kind coercions]. - Note [Predicate coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have @@ -1600,10 +1626,17 @@ tyCoVarsOfCoList :: Coercion -> [TyCoVar] -- See Note [Free variables of types] tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co +tyCoFVsOfMCo :: MCoercion -> FV +tyCoFVsOfMCo MRefl = emptyFV +tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co + tyCoFVsOfCo :: Coercion -> FV -- Extracts type and coercion variables from a coercion -- See Note [Free variables of types] -tyCoFVsOfCo (Refl _ ty) fv_cand in_scope acc = tyCoFVsOfType ty fv_cand in_scope acc +tyCoFVsOfCo (Refl ty) fv_cand in_scope acc + = tyCoFVsOfType ty fv_cand in_scope acc +tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc + = (tyCoFVsOfType ty `unionFV` tyCoFVsOfMCo mco) fv_cand in_scope acc tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc @@ -1625,7 +1658,6 @@ tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV tyCoFVsOfCo (NthCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc -tyCoFVsOfCo (CoherenceCo c1 c2) fv_cand in_scope acc = (tyCoFVsOfCo c1 `unionFV` tyCoFVsOfCo c2) fv_cand in_scope acc tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc 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 @@ -1670,9 +1702,14 @@ coVarsOfType (CoercionTy co) = coVarsOfCo co coVarsOfTypes :: [Type] -> TyCoVarSet coVarsOfTypes tys = mapUnionVarSet coVarsOfType tys +coVarsOfMCo :: MCoercion -> CoVarSet +coVarsOfMCo MRefl = emptyVarSet +coVarsOfMCo (MCo co) = coVarsOfCo co + coVarsOfCo :: Coercion -> CoVarSet -- Extract *coercion* variables only. Tiresome to repeat the code, but easy. -coVarsOfCo (Refl _ ty) = coVarsOfType ty +coVarsOfCo (Refl ty) = coVarsOfType ty +coVarsOfCo (GRefl _ ty co) = coVarsOfType ty `unionVarSet` coVarsOfMCo co coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args coVarsOfCo (AppCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg coVarsOfCo (ForAllCo tv kind_co co) @@ -1688,7 +1725,6 @@ coVarsOfCo (TransCo co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 coVarsOfCo (NthCo _ _ co) = coVarsOfCo co coVarsOfCo (LRCo _ co) = coVarsOfCo co coVarsOfCo (InstCo co arg) = coVarsOfCo co `unionVarSet` coVarsOfCo arg -coVarsOfCo (CoherenceCo c1 c2) = coVarsOfCos [c1, c2] coVarsOfCo (KindCo co) = coVarsOfCo co coVarsOfCo (SubCo co) = coVarsOfCo co coVarsOfCo (AxiomRuleCo _ cs) = coVarsOfCos cs @@ -1776,10 +1812,15 @@ noFreeVarsOfType (LitTy _) = True noFreeVarsOfType (CastTy ty co) = noFreeVarsOfType ty && noFreeVarsOfCo co noFreeVarsOfType (CoercionTy co) = noFreeVarsOfCo co +noFreeVarsOfMCo :: MCoercion -> Bool +noFreeVarsOfMCo MRefl = True +noFreeVarsOfMCo (MCo co) = noFreeVarsOfCo co + -- | Returns True if this coercion has no free variables. Should be the same as -- isEmptyVarSet . tyCoVarsOfCo, but faster in the non-forall case. noFreeVarsOfCo :: Coercion -> Bool -noFreeVarsOfCo (Refl _ ty) = noFreeVarsOfType ty +noFreeVarsOfCo (Refl ty) = noFreeVarsOfType ty +noFreeVarsOfCo (GRefl _ ty co) = noFreeVarsOfType ty && noFreeVarsOfMCo co noFreeVarsOfCo (TyConAppCo _ _ args) = all noFreeVarsOfCo args noFreeVarsOfCo (AppCo c1 c2) = noFreeVarsOfCo c1 && noFreeVarsOfCo c2 noFreeVarsOfCo co@(ForAllCo {}) = isEmptyVarSet (tyCoVarsOfCo co) @@ -1795,7 +1836,6 @@ noFreeVarsOfCo (TransCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 noFreeVarsOfCo (NthCo _ _ co) = noFreeVarsOfCo co noFreeVarsOfCo (LRCo _ co) = noFreeVarsOfCo co noFreeVarsOfCo (InstCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 -noFreeVarsOfCo (CoherenceCo co1 co2) = noFreeVarsOfCo co1 && noFreeVarsOfCo co2 noFreeVarsOfCo (KindCo co) = noFreeVarsOfCo co noFreeVarsOfCo (SubCo co) = noFreeVarsOfCo co noFreeVarsOfCo (AxiomRuleCo _ cs) = all noFreeVarsOfCo cs @@ -2456,8 +2496,13 @@ subst_co subst co go_ty :: Type -> Type go_ty = subst_ty subst + go_mco :: MCoercion -> MCoercion + go_mco MRefl = MRefl + go_mco (MCo co) = MCo (go co) + go :: Coercion -> Coercion - go (Refl r ty) = mkReflCo r $! go_ty ty + go (Refl ty) = mkNomReflCo $! (go_ty ty) + go (GRefl r ty mco) = (mkGReflCo r $! (go_ty ty)) $! (go_mco mco) go (TyConAppCo r tc args)= let args' = map go args in args' `seqList` mkTyConAppCo r tc args' go (AppCo co arg) = (mkAppCo $! go co) $! go arg @@ -2474,7 +2519,6 @@ subst_co subst co go (NthCo r d co) = mkNthCo r d $! (go co) go (LRCo lr co) = mkLRCo lr $! (go co) go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg - go (CoherenceCo co1 co2) = (mkCoherenceCo $! (go co1)) $! (go co2) go (KindCo co) = mkKindCo $! (go co) go (SubCo co) = mkSubCo $! (go co) go (AxiomRuleCo c cs) = let cs1 = map go cs @@ -3057,7 +3101,11 @@ tidyCo :: TidyEnv -> Coercion -> Coercion tidyCo env@(_, subst) co = go co where - go (Refl r ty) = Refl r (tidyType env ty) + go_mco MRefl = MRefl + go_mco (MCo co) = MCo (go co) + + go (Refl ty) = Refl (tidyType env ty) + go (GRefl r ty mco) = GRefl r (tidyType env ty) $! go_mco mco go (TyConAppCo r tc cos) = let args = map go cos in args `seqList` TyConAppCo r tc args go (AppCo co1 co2) = (AppCo $! go co1) $! go co2 @@ -3079,7 +3127,6 @@ tidyCo env@(_, subst) co go (NthCo r d co) = NthCo r d $! go co go (LRCo lr co) = LRCo lr $! go co go (InstCo co ty) = (InstCo $! go co) $! go ty - go (CoherenceCo co1 co2) = (CoherenceCo $! go co1) $! go co2 go (KindCo co) = KindCo $! go co go (SubCo co) = SubCo $! go co go (AxiomRuleCo ax cos) = let cos1 = tidyCos env cos @@ -3124,7 +3171,9 @@ typeSize (CastTy ty co) = typeSize ty + coercionSize co typeSize (CoercionTy co) = coercionSize co coercionSize :: Coercion -> Int -coercionSize (Refl _ ty) = typeSize ty +coercionSize (Refl ty) = typeSize ty +coercionSize (GRefl _ ty MRefl) = typeSize ty +coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args) coercionSize (AppCo co arg) = coercionSize co + coercionSize arg coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h @@ -3138,7 +3187,6 @@ coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2 coercionSize (NthCo _ _ co) = 1 + coercionSize co coercionSize (LRCo _ co) = 1 + coercionSize co coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg -coercionSize (CoherenceCo c1 c2) = 1 + coercionSize c1 + coercionSize c2 coercionSize (KindCo co) = 1 + coercionSize co coercionSize (SubCo co) = 1 + coercionSize co coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs) diff --git a/compiler/types/TyCoRep.hs-boot b/compiler/types/TyCoRep.hs-boot index 3753e70b84..9f886dc458 100644 --- a/compiler/types/TyCoRep.hs-boot +++ b/compiler/types/TyCoRep.hs-boot @@ -12,10 +12,13 @@ data UnivCoProvenance data TCvSubst data TyLit data TyBinder +data MCoercion type PredType = Type type Kind = Type type ThetaType = [PredType] +type CoercionN = Coercion +type MCoercionN = MCoercion pprKind :: Kind -> SDoc pprType :: Type -> SDoc diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index f501930cc7..45b1b74382 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -403,8 +403,13 @@ expandTypeSynonyms ty go subst (CastTy ty co) = mkCastTy (go subst ty) (go_co subst co) go subst (CoercionTy co) = mkCoercionTy (go_co subst co) - go_co subst (Refl r ty) - = mkReflCo r (go subst ty) + go_mco _ MRefl = MRefl + go_mco subst (MCo co) = MCo (go_co subst co) + + go_co subst (Refl ty) + = mkNomReflCo (go subst ty) + go_co subst (GRefl r ty mco) + = mkGReflCo r (go subst ty) (go_mco subst mco) -- NB: coercions are always expanded upon creation go_co subst (TyConAppCo r tc args) = mkTyConAppCo r tc (map (go_co subst) args) @@ -431,8 +436,6 @@ expandTypeSynonyms ty = mkLRCo lr (go_co subst co) go_co subst (InstCo co arg) = mkInstCo (go_co subst co) (go_co subst arg) - go_co subst (CoherenceCo co1 co2) - = mkCoherenceCo (go_co subst co1) (go_co subst co2) go_co subst (KindCo co) = mkKindCo (go_co subst co) go_co subst (SubCo co) @@ -541,7 +544,11 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar env co = go co where - go (Refl r ty) = Refl r <$> mapType mapper env ty + go_mco MRefl = return MRefl + go_mco (MCo co) = MCo <$> (go co) + + go (Refl ty) = Refl <$> mapType mapper env ty + go (GRefl r ty mco) = mkgreflco r <$> mapType mapper env ty <*> (go_mco mco) go (TyConAppCo r tc args) = mktyconappco r tc <$> mapM go args go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2 @@ -565,7 +572,6 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar go (NthCo r i co) = mknthco r i <$> go co go (LRCo lr co) = mklrco lr <$> go co go (InstCo co arg) = mkinstco <$> go co <*> go arg - go (CoherenceCo c1 c2) = mkcoherenceco <$> go c1 <*> go c2 go (KindCo co) = mkkindco <$> go co go (SubCo co) = mksubco <$> go co @@ -575,16 +581,16 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar go_prov p@(PluginProv _) = return p ( mktyconappco, mkappco, mkaxiominstco, mkunivco - , mksymco, mktransco, mknthco, mklrco, mkinstco, mkcoherenceco - , mkkindco, mksubco, mkforallco) + , mksymco, mktransco, mknthco, mklrco, mkinstco + , mkkindco, mksubco, mkforallco, mkgreflco) | smart = ( mkTyConAppCo, mkAppCo, mkAxiomInstCo, mkUnivCo - , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo, mkCoherenceCo - , mkKindCo, mkSubCo, mkForAllCo ) + , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo + , mkKindCo, mkSubCo, mkForAllCo, mkGReflCo ) | otherwise = ( TyConAppCo, AppCo, AxiomInstCo, UnivCo - , SymCo, TransCo, NthCo, LRCo, InstCo, CoherenceCo - , KindCo, SubCo, ForAllCo ) + , SymCo, TransCo, NthCo, LRCo, InstCo + , KindCo, SubCo, ForAllCo, GRefl ) {- ************************************************************************ @@ -2293,7 +2299,8 @@ nonDetCmpTypeX env orig_t1 orig_t2 = nonDetCmpTypesX :: RnEnv2 -> [Type] -> [Type] -> Ordering nonDetCmpTypesX _ [] [] = EQ nonDetCmpTypesX env (t1:tys1) (t2:tys2) = nonDetCmpTypeX env t1 t2 - `thenCmp` nonDetCmpTypesX env tys1 tys2 + `thenCmp` + nonDetCmpTypesX env tys1 tys2 nonDetCmpTypesX _ [] _ = LT nonDetCmpTypesX _ _ [] = GT @@ -2463,8 +2470,15 @@ occCheckExpand vs_to_avoid ty -- See Note [Occurrence checking: look inside kinds] ------------------ - go_co cxt (Refl r ty) = do { ty' <- go cxt ty - ; return (mkReflCo r ty') } + go_mco _ MRefl = return MRefl + go_mco ctx (MCo co) = MCo <$> go_co ctx co + + ------------------ + go_co cxt (Refl ty) = do { ty' <- go cxt ty + ; return (mkNomReflCo ty') } + go_co cxt (GRefl r ty mco) = do { mco' <- go_mco cxt mco + ; ty' <- go cxt ty + ; return (mkGReflCo r ty' mco') } -- Note: Coercions do not contain type synonyms go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args ; return (mkTyConAppCo r tc args') } @@ -2504,9 +2518,6 @@ occCheckExpand vs_to_avoid ty go_co cxt (InstCo co arg) = do { co' <- go_co cxt co ; arg' <- go_co cxt arg ; return (mkInstCo co' arg') } - go_co cxt (CoherenceCo co1 co2) = do { co1' <- go_co cxt co1 - ; co2' <- go_co cxt co2 - ; return (mkCoherenceCo co1' co2') } go_co cxt (KindCo co) = do { co' <- go_co cxt co ; return (mkKindCo co') } go_co cxt (SubCo co) = do { co' <- go_co cxt co @@ -2547,7 +2558,8 @@ tyConsOfType ty go (CastTy ty co) = go ty `unionUniqSets` go_co co go (CoercionTy co) = go_co co - go_co (Refl _ ty) = go ty + go_co (Refl ty) = go ty + go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co @@ -2561,11 +2573,13 @@ tyConsOfType ty go_co (NthCo _ _ co) = go_co co go_co (LRCo _ co) = go_co co go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg - go_co (CoherenceCo co1 co2) = go_co co1 `unionUniqSets` go_co co2 go_co (KindCo co) = go_co co go_co (SubCo co) = go_co co go_co (AxiomRuleCo _ cs) = go_cos cs + go_mco MRefl = emptyUniqSet + go_mco (MCo co) = go_co co + go_prov UnsafeCoerceProv = emptyUniqSet go_prov (PhantomProv co) = go_co co go_prov (ProofIrrelProv co) = go_co co diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs index edd82ba6fa..a8474524ab 100644 --- a/compiler/types/Unify.hs +++ b/compiler/types/Unify.hs @@ -1319,7 +1319,7 @@ data MatchEnv = ME { me_tmpls :: TyVarSet , me_env :: RnEnv2 } -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'. In particular, if --- @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@, +-- @liftCoMatch vars ty co == Just s@, then @liftCoSubst s ty == co@, -- where @==@ there means that the result of 'liftCoSubst' has the same -- type as the original co; but may be different under the hood. -- That is, it matches a type against a coercion of the same @@ -1392,9 +1392,6 @@ ty_co_match menv subst ty co lkco rkco ty_co_match menv subst ty' co (substed_co_l `mkTransCo` lkco) (substed_co_r `mkTransCo` rkco) - | CoherenceCo co1 co2 <- co - = ty_co_match menv subst ty co1 (lkco `mkTransCo` mkSymCo co2) rkco - | SymCo co' <- co = swapLiftCoEnv <$> ty_co_match menv (swapLiftCoEnv subst) ty co' rkco lkco @@ -1409,7 +1406,7 @@ ty_co_match menv subst (TyVarTy tv1) co lkco rkco = if any (inRnEnvR rn_env) (tyCoVarsOfCoList co) then Nothing -- occurs check failed else Just $ extendVarEnv subst tv1' $ - castCoercionKind co (mkSymCo lkco) (mkSymCo rkco) + castCoercionKindI co (mkSymCo lkco) (mkSymCo rkco) | otherwise = Nothing @@ -1457,6 +1454,21 @@ ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1) ty_co_match _ subst (CoercionTy {}) _ _ _ = Just subst -- don't inspect coercions +ty_co_match menv subst ty (GRefl r t (MCo co)) lkco rkco + = ty_co_match menv subst ty (GRefl r t MRefl) lkco (rkco `mkTransCo` mkSymCo co) + +ty_co_match menv subst ty co1 lkco rkco + | Just (CastTy t co, r) <- isReflCo_maybe co1 + -- In @pushRefl@, pushing reflexive coercion inside CastTy will give us + -- t |> co ~ t ; <t> ; t ~ t |> co + -- But transitive coercions are not helpful. Therefore we deal + -- with it here: we do recursion on the smaller reflexive coercion, + -- while propagating the correct kind coercions. + = let kco' = mkSymCo co + in ty_co_match menv subst ty (mkReflCo r t) (lkco `mkTransCo` kco') + (rkco `mkTransCo` kco') + + ty_co_match menv subst ty co lkco rkco | Just co' <- pushRefl co = ty_co_match menv subst ty co' lkco rkco | otherwise = Nothing @@ -1501,17 +1513,18 @@ ty_co_match_args menv subst (ty:tys) (arg:args) (lkco:lkcos) (rkco:rkcos) ty_co_match_args _ _ _ _ _ _ = Nothing pushRefl :: Coercion -> Maybe Coercion -pushRefl (Refl Nominal (AppTy ty1 ty2)) - = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2)) -pushRefl (Refl r (FunTy ty1 ty2)) - | Just rep1 <- getRuntimeRep_maybe ty1 - , Just rep2 <- getRuntimeRep_maybe ty2 - = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2 - , mkReflCo r ty1, mkReflCo r ty2 ]) -pushRefl (Refl r (TyConApp tc tys)) - = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys)) -pushRefl (Refl r (ForAllTy (TvBndr tv _) ty)) - = Just (mkHomoForAllCos_NoRefl [tv] (Refl r ty)) +pushRefl co = + case (isReflCo_maybe co) of + Just (AppTy ty1 ty2, Nominal) + -> Just (AppCo (mkReflCo Nominal ty1) (mkNomReflCo ty2)) + Just (FunTy ty1 ty2, r) + | Just rep1 <- getRuntimeRep_maybe ty1 + , Just rep2 <- getRuntimeRep_maybe ty2 + -> Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2 + , mkReflCo r ty1, mkReflCo r ty2 ]) + Just (TyConApp tc tys, r) + -> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys)) + Just (ForAllTy (TvBndr tv _) ty, r) + -> Just (mkHomoForAllCos_NoRefl [tv] (mkReflCo r ty)) -- NB: NoRefl variant. Otherwise, we get a loop! -pushRefl (Refl r (CastTy ty co)) = Just (castCoercionKind (Refl r ty) co co) -pushRefl _ = Nothing + _ -> Nothing diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T index dfb8613d98..6632231999 100644 --- a/testsuite/tests/perf/compiler/all.T +++ b/testsuite/tests/perf/compiler/all.T @@ -891,7 +891,7 @@ test('T9872c', test('T9872d', [ only_ways(['normal']), compiler_stats_num_field('bytes allocated', - [(wordsize(64), 572537984, 5), + [(wordsize(64), 578498120, 5), # 2014-12-18 796071864 Initally created # 2014-12-18 739189056 Reduce type families even more eagerly # 2015-01-07 687562440 TrieMap leaf compression @@ -906,6 +906,7 @@ test('T9872d', # 2017-03-03 462817352 Share Typeable KindReps # 2018-03-25 526485920 Flattener patch does more work (#12919) # 2018-04-11 572537984 simplCast improvement collateral (#11735) + # 2018-07-04 578498120 introduce GRefl (#15192) (wordsize(32), 232954000, 5) # some date 328810212 |