diff options
Diffstat (limited to 'compiler/GHC/Tc')
| -rw-r--r-- | compiler/GHC/Tc/Gen/Bind.hs | 3 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Foreign.hs | 55 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Instance/Family.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Module.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Plugin.hs | 5 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 145 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/InertSet.hs | 6 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 88 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Solver/Rewrite.hs | 403 |
9 files changed, 347 insertions, 365 deletions
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 8a83b5540f..01dcd48952 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -44,6 +44,7 @@ import GHC.Tc.Types.Evidence import GHC.Tc.Gen.HsType import GHC.Tc.Gen.Pat import GHC.Tc.Utils.TcMType +import GHC.Core.Reduction ( Reduction(..) ) import GHC.Core.Multiplicity import GHC.Core.FamInstEnv( normaliseType ) import GHC.Tc.Instance.Family( tcGetFamInstEnvs ) @@ -829,7 +830,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty -- a duplicate ambiguity error. There is a similar -- checkNoErrs for complete type signatures too. do { fam_envs <- tcGetFamInstEnvs - ; let (_co, mono_ty') = normaliseType fam_envs Nominal mono_ty + ; let mono_ty' = reductionReducedType $ normaliseType fam_envs Nominal mono_ty -- Unification may not have normalised the type, -- so do it here to make it as uncomplicated as possible. -- Example: f :: [F Int] -> Bool diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs index 4204071b7d..b1c38a7166 100644 --- a/compiler/GHC/Tc/Gen/Foreign.hs +++ b/compiler/GHC/Tc/Gen/Foreign.hs @@ -48,6 +48,7 @@ import GHC.Tc.Utils.Env import GHC.Tc.Instance.Family import GHC.Core.FamInstEnv import GHC.Core.Coercion +import GHC.Core.Reduction import GHC.Core.Type import GHC.Core.Multiplicity import GHC.Types.ForeignCall @@ -70,7 +71,11 @@ import GHC.Data.Bag import GHC.Driver.Hooks import qualified GHC.LanguageExtensions as LangExt -import Control.Monad +import Control.Monad ( zipWithM ) +import Control.Monad.Trans.Writer.CPS + ( WriterT, runWriterT, tell ) +import Control.Monad.Trans.Class + ( lift ) -- Defines a binding isForeignImport :: forall name. UnXRec name => LForeignDecl name -> Bool @@ -107,15 +112,15 @@ an AppTy will be marshalable. -- we are only allowed to look through newtypes if the constructor is -- in scope. We return a bag of all the newtype constructors thus found. -- Always returns a Representational coercion -normaliseFfiType :: Type -> TcM (Coercion, Type, Bag GlobalRdrElt) +normaliseFfiType :: Type -> TcM (Reduction, Bag GlobalRdrElt) normaliseFfiType ty = do fam_envs <- tcGetFamInstEnvs normaliseFfiType' fam_envs ty -normaliseFfiType' :: FamInstEnvs -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt) -normaliseFfiType' env ty0 = go Representational initRecTc ty0 +normaliseFfiType' :: FamInstEnvs -> Type -> TcM (Reduction, Bag GlobalRdrElt) +normaliseFfiType' env ty0 = runWriterT $ go Representational initRecTc ty0 where - go :: Role -> RecTcChecker -> Type -> TcM (Coercion, Type, Bag GlobalRdrElt) + go :: Role -> RecTcChecker -> Type -> WriterT (Bag GlobalRdrElt) TcM Reduction go role rec_nts ty | Just ty' <- tcView ty -- Expand synonyms = go role rec_nts ty' @@ -125,15 +130,14 @@ normaliseFfiType' env ty0 = go Representational initRecTc ty0 | (bndrs, inner_ty) <- splitForAllTyCoVarBinders ty , not (null bndrs) - = do (coi, nty1, gres1) <- go role rec_nts inner_ty - return ( mkHomoForAllCos (binderVars bndrs) coi - , mkForAllTys bndrs nty1, gres1 ) + = do redn <- go role rec_nts inner_ty + return $ mkHomoForAllRedn bndrs redn | otherwise -- see Note [Don't recur in normaliseFfiType'] - = return (mkReflCo role ty, ty, emptyBag) + = return $ mkReflRedn role ty go_tc_app :: Role -> RecTcChecker -> TyCon -> [Type] - -> TcM (Coercion, Type, Bag GlobalRdrElt) + -> WriterT (Bag GlobalRdrElt) TcM Reduction go_tc_app role rec_nts tc tys -- We don't want to look through the IO newtype, even if it is -- in scope, so we have a special case for it: @@ -148,32 +152,34 @@ normaliseFfiType' env ty0 = go Representational initRecTc ty0 -- Here, we don't reject the type for being recursive. -- If this is a recursive newtype then it will normally -- be rejected later as not being a valid FFI type. - = do { rdr_env <- getGlobalRdrEnv + = do { rdr_env <- lift $ getGlobalRdrEnv ; case checkNewtypeFFI rdr_env tc of Nothing -> nothing - Just gre -> do { (co', ty', gres) <- go role rec_nts' nt_rhs - ; return (mkTransCo nt_co co', ty', gre `consBag` gres) } } + Just gre -> + do { redn <- go role rec_nts' nt_rhs + ; tell (unitBag gre) + ; return $ nt_co `mkTransRedn` redn } } | isFamilyTyCon tc -- Expand open tycons - , (co, ty) <- normaliseTcApp env role tc tys + , Reduction co ty <- normaliseTcApp env role tc tys , not (isReflexiveCo co) - = do (co', ty', gres) <- go role rec_nts ty - return (mkTransCo co co', ty', gres) + = do redn <- go role rec_nts ty + return $ co `mkTransRedn` redn | otherwise = nothing -- see Note [Don't recur in normaliseFfiType'] where tc_key = getUnique tc children_only - = do xs <- zipWithM (\ty r -> go r rec_nts ty) tys (tyConRolesX role tc) - let (cos, tys', gres) = unzip3 xs - return ( mkTyConAppCo role tc cos - , mkTyConApp tc tys', unionManyBags gres) + = do { args <- unzipRedns <$> + zipWithM ( \ ty r -> go r rec_nts ty ) + tys (tyConRolesX role tc) + ; return $ mkTyConAppRedn role tc args } nt_co = mkUnbranchedAxInstCo role (newTyConCo tc) tys [] nt_rhs = newTyConInstRhs tc tys ty = mkTyConApp tc tys - nothing = return (mkReflCo role ty, ty, emptyBag) + nothing = return $ mkReflRedn role ty checkNewtypeFFI :: GlobalRdrEnv -> TyCon -> Maybe GlobalRdrElt checkNewtypeFFI rdr_env tc @@ -236,7 +242,7 @@ tcFImport (L dloc fo@(ForeignImport { fd_name = L nloc nm, fd_sig_ty = hs_ty , fd_fi = imp_decl })) = setSrcSpanA dloc $ addErrCtxt (foreignDeclCtxt fo) $ do { sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty - ; (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty + ; (Reduction norm_co norm_sig_ty, gres) <- normaliseFfiType sig_ty ; let -- Drop the foralls before inspecting the -- structure of the foreign type. @@ -389,7 +395,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty rhs <- tcCheckPolyExpr (nlHsVar nm) sig_ty - (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty + (Reduction norm_co norm_sig_ty, gres) <- normaliseFfiType sig_ty spec' <- tcCheckFEType norm_sig_ty spec @@ -406,7 +412,8 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe return ( mkVarBind id rhs , ForeignExport { fd_name = L loc id , fd_sig_ty = undefined - , fd_e_ext = norm_co, fd_fe = spec' } + , fd_e_ext = norm_co + , fd_fe = spec' } , gres) tcFExport d = pprPanic "tcFExport" (ppr d) diff --git a/compiler/GHC/Tc/Instance/Family.hs b/compiler/GHC/Tc/Instance/Family.hs index 4818fd9ad9..a7cdb3d507 100644 --- a/compiler/GHC/Tc/Instance/Family.hs +++ b/compiler/GHC/Tc/Instance/Family.hs @@ -534,7 +534,7 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args -- It does not look through type families. -- It does not normalise arguments to a tycon. -- --- If the result is Just (rep_ty, (co, gres), rep_ty), then +-- If the result is Just ((gres, co), rep_ty), then -- co : ty ~R rep_ty -- gres are the GREs for the data constructors that -- had to be in scope diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 696e8dc8a3..f458605c14 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -119,6 +119,7 @@ import GHC.Core.DataCon import GHC.Core.Type import GHC.Core.Class import GHC.Core.Coercion.Axiom +import GHC.Core.Reduction ( Reduction(..) ) import GHC.Core.Unify( RoughMatchTc(..) ) import GHC.Core.FamInstEnv ( FamInst, pprFamInst, famInstsRepTyCons @@ -2589,7 +2590,7 @@ tcRnExpr hsc_env mode rdr_expr fam_envs <- tcGetFamInstEnvs ; -- normaliseType returns a coercion which we discard, so the Role is -- irrelevant - return (snd (normaliseType fam_envs Nominal ty)) + return (reductionReducedType (normaliseType fam_envs Nominal ty)) } where -- Optionally instantiate the type of the expression @@ -2676,7 +2677,7 @@ tcRnType hsc_env flexi normalise rdr_type -- normaliseType: expand type-family applications -- expandTypeSynonyms: expand type synonyms (#18828) ; fam_envs <- tcGetFamInstEnvs - ; let ty' | normalise = expandTypeSynonyms $ snd $ + ; let ty' | normalise = expandTypeSynonyms $ reductionReducedType $ normaliseType fam_envs Nominal ty | otherwise = ty diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs index 0674f69903..78a0ebd16a 100644 --- a/compiler/GHC/Tc/Plugin.hs +++ b/compiler/GHC/Tc/Plugin.hs @@ -67,13 +67,14 @@ import GHC.Tc.Utils.Monad ( TcGblEnv, TcLclEnv, TcPluginM import GHC.Tc.Types.Constraint ( Ct, CtLoc, CtEvidence(..), ctLocOrigin ) import GHC.Tc.Utils.TcMType ( TcTyVar, TcType ) import GHC.Tc.Utils.Env ( TcTyThing ) -import GHC.Tc.Types.Evidence ( TcCoercion, CoercionHole, EvTerm(..) +import GHC.Tc.Types.Evidence ( CoercionHole, EvTerm(..) , EvExpr, EvBind, mkGivenEvBind ) import GHC.Types.Var ( EvVar ) import GHC.Unit.Module import GHC.Types.Name import GHC.Types.TyThing +import GHC.Core.Reduction ( Reduction ) import GHC.Core.TyCon import GHC.Core.DataCon import GHC.Core.Class @@ -142,7 +143,7 @@ getFamInstEnvs :: TcPluginM (FamInstEnv, FamInstEnv) getFamInstEnvs = unsafeTcPluginTcM TcM.tcGetFamInstEnvs matchFam :: TyCon -> [Type] - -> TcPluginM (Maybe (TcCoercion, TcType)) + -> TcPluginM (Maybe Reduction) matchFam tycon args = unsafeTcPluginTcM $ TcS.matchFamTcM tycon args newUnique :: TcPluginM Unique diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 162ef60cbc..e8c4ee82e2 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -29,6 +29,7 @@ import GHC.Core.Multiplicity import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness checking import GHC.Core.Coercion import GHC.Core.Coercion.Axiom +import GHC.Core.Reduction import GHC.Core import GHC.Types.Id( mkTemplateLocals ) import GHC.Core.FamInstEnv ( FamInstEnvs ) @@ -209,15 +210,15 @@ canClass :: CtEvidence canClass ev cls tys pend_sc fds = -- all classes do *nominal* matching assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $ - do { (xis, cos) <- rewriteArgsNom ev cls_tc tys - ; let co = mkTcTyConAppCo Nominal cls_tc cos - xi = mkClassPred cls xis + do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc tys + ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns mk_ct new_ev = CDictCan { cc_ev = new_ev , cc_tyargs = xis , cc_class = cls , cc_pend_sc = pend_sc , cc_fundeps = fds } - ; mb <- rewriteEvidence ev xi co + ; mb <- rewriteEvidence ev redn + ; traceTcS "canClass" (vcat [ ppr ev , ppr xi, ppr mb ]) ; return (fmap mk_ct mb) } @@ -709,8 +710,8 @@ canIrred :: CtEvidence -> TcS (StopOrContinue Ct) canIrred ev = do { let pred = ctEvPred ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) - ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred - ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> + ; redn <- rewrite ev pred + ; rewriteEvidence ev redn `andWhenContinue` \ new_ev -> do { -- Re-classify, in case rewriting has improved its shape -- Code is like the canNC, except @@ -824,8 +825,8 @@ canForAll :: CtEvidence -> Bool -> TcS (StopOrContinue Ct) canForAll ev pend_sc = do { -- First rewrite it to apply the current substitution let pred = ctEvPred ev - ; (xi,co) <- rewrite ev pred -- co :: xi ~ pred - ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev -> + ; redn <- rewrite ev pred + ; rewriteEvidence ev redn `andWhenContinue` \ new_ev -> do { -- Now decompose into its pieces and solve it -- (It takes a lot less code to rewrite before decomposing.) @@ -1058,9 +1059,9 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _ -- No similarity in type structure detected. Rewrite and try again. can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 - = do { (xi1, co1) <- rewrite ev ps_ty1 - ; (xi2, co2) <- rewrite ev ps_ty2 - ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 + = do { redn1@(Reduction _ xi1) <- rewrite ev ps_ty1 + ; redn2@(Reduction _ xi2) <- rewrite ev ps_ty2 + ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2 ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 } ---------------------------- @@ -1459,9 +1460,9 @@ can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2 -> TcType -- ^ ty2 -> TcType -- ^ ty2, with type synonyms -> TcS (StopOrContinue Ct) -can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2 +can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2 = do { traceTcS "can_eq_newtype_nc" $ - vcat [ ppr ev, ppr swapped, ppr co, ppr gres, ppr ty1', ppr ty2 ] + vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ] -- check for blowing our stack: -- See Note [Newtypes can blow the stack] @@ -1477,8 +1478,11 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co), ty1') ty2 ps_ty2 -- module, don't warn about it being unused. -- See Note [Tracking unused binding and imports] in GHC.Tc.Utils. - ; new_ev <- rewriteEqEvidence ev swapped ty1' ps_ty2 - (mkTcSymCo co) (mkTcReflCo Representational ps_ty2) + ; let redn1 = mkReduction co1 ty1' + + ; new_ev <- rewriteEqEvidence ev swapped + redn1 + (mkReflRedn Representational ps_ty2) ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 } where gre_list = bagToList gres @@ -1553,9 +1557,9 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2 = do { traceTcS "Decomposing cast" (vcat [ ppr ev , ppr ty1 <+> text "|>" <+> ppr co1 , ppr ps_ty2 ]) - ; new_ev <- rewriteEqEvidence ev swapped ty1 ps_ty2 - (mkTcGReflRightCo role ty1 co1) - (mkTcReflCo role ps_ty2) + ; new_ev <- rewriteEqEvidence ev swapped + (mkGReflLeftRedn role ty1 co1) + (mkReflRedn role ps_ty2) ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 } where role = eqRelRole eq_rel @@ -1912,14 +1916,14 @@ canEqFailure :: CtEvidence -> EqRel canEqFailure ev NomEq ty1 ty2 = canEqHardFailure ev ty1 ty2 canEqFailure ev ReprEq ty1 ty2 - = do { (xi1, co1) <- rewrite ev ty1 - ; (xi2, co2) <- rewrite ev ty2 + = do { redn1 <- rewrite ev ty1 + ; redn2 <- rewrite ev ty2 -- We must rewrite the types before putting them in the -- inert set, so that we are sure to kick them out when -- new equalities become available ; traceTcS "canEqFailure with ReprEq" $ - vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ] - ; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2 + vcat [ ppr ev, ppr redn1, ppr redn2 ] + ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2 ; continueWith (mkIrredCt ReprEqReason new_ev) } -- | Call when canonicalizing an equality fails with utterly no hope. @@ -1928,9 +1932,9 @@ canEqHardFailure :: CtEvidence -- See Note [Make sure that insolubles are fully rewritten] canEqHardFailure ev ty1 ty2 = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2) - ; (s1, co1) <- rewrite ev ty1 - ; (s2, co2) <- rewrite ev ty2 - ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 + ; redn1 <- rewrite ev ty1 + ; redn2 <- rewrite ev ty2 + ; new_ev <- rewriteEqEvidence ev NotSwapped redn1 redn2 ; continueWith (mkIrredCt ShapeMismatchReason new_ev) } {- @@ -2067,7 +2071,7 @@ Ticket #12526 is another good example of this in action. -} --------------------- -canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs +canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs -> EqRel -> SwapFlag -> CanEqLHS -- lhs (or, if swapped, rhs) -> TcType -- lhs: pretty lhs, already rewritten @@ -2097,16 +2101,15 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 ; let -- kind_co :: (ki2 :: *) ~N (ki1 :: *) (whether swapped or not) -- co1 :: kind(tv1) ~N ki1 - rhs' = xi2 `mkCastTy` kind_co -- :: ki1 ps_rhs' = ps_xi2 `mkCastTy` kind_co -- :: ki1 - rhs_co = mkTcGReflLeftCo role xi2 kind_co - -- rhs_co :: (xi2 |> kind_co) ~ xi2 - lhs_co = mkTcReflCo role xi1 + lhs_redn = mkReflRedn role xi1 + rhs_redn@(Reduction _ rhs') + = mkGReflRightRedn role xi2 kind_co ; traceTcS "Hetero equality gives rise to kind equality" (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ]) - ; type_ev <- rewriteEqEvidence ev swapped xi1 rhs' lhs_co rhs_co + ; type_ev <- rewriteEqEvidence ev swapped lhs_redn rhs_redn -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 rhs' ps_rhs' } @@ -2305,8 +2308,8 @@ canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco -- want to rewrite the LHS to (as per e.g. swapOverTyVars) canEqCanLHSFinish :: CtEvidence -> EqRel -> SwapFlag - -> CanEqLHS -- lhs (or, if swapped, rhs) - -> TcType -- rhs, pretty rhs + -> CanEqLHS -- lhs (or, if swapped, rhs) + -> TcType -- rhs (or, if swapped, lhs) -> TcS (StopOrContinue Ct) canEqCanLHSFinish ev eq_rel swapped lhs rhs -- RHS is fully rewritten, but with type synonyms @@ -2315,7 +2318,9 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs -- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2 = do { dflags <- getDynFlags - ; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs rewrite_co1 rewrite_co2 + ; new_ev <- rewriteEqEvidence ev swapped + (mkReflRedn role lhs_ty) + (mkReflRedn role rhs) -- by now, (TyEq:K) is already satisfied ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs) @@ -2356,7 +2361,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs do { traceTcS "canEqCanLHSFinish can't make a canonical" (ppr lhs $$ ppr rhs) ; continueWith (mkIrredCt reason new_ev) } - ; Just (lhs_tv, co, new_rhs) -> + ; Just (lhs_tv, rhs_redn@(Reduction _ new_rhs)) -> do { traceTcS "canEqCanLHSFinish breaking a cycle" $ ppr lhs $$ ppr rhs ; traceTcS "new RHS:" (ppr new_rhs) @@ -2370,8 +2375,8 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs else do { -- See Detail (6) of Note [Type variable cycles] new_new_ev <- rewriteEqEvidence new_ev NotSwapped - lhs_ty new_rhs - (mkTcNomReflCo lhs_ty) co + (mkReflRedn Nominal lhs_ty) + rhs_redn ; continueWith (CEqCan { cc_ev = new_new_ev , cc_lhs = lhs @@ -2382,9 +2387,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs lhs_ty = canEqLHSType lhs - rewrite_co1 = mkTcReflCo role lhs_ty - rewrite_co2 = mkTcReflCo role rhs - -- This is about (TyEq:N) bad_newtype | ReprEq <- eq_rel , Just tc <- tyConAppTyCon_maybe rhs @@ -2410,13 +2412,10 @@ rewriteCastedEquality :: CtEvidence -- :: lhs ~ (rhs |> mco), or (rhs |> mco -> TcS CtEvidence -- :: (lhs |> sym mco) ~ rhs -- result is independent of SwapFlag rewriteCastedEquality ev eq_rel swapped lhs rhs mco - = rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co + = rewriteEqEvidence ev swapped lhs_redn rhs_redn where - new_lhs = lhs `mkCastTyMCo` sym_mco - lhs_co = mkTcGReflLeftMCo role lhs sym_mco - - new_rhs = rhs - rhs_co = mkTcGReflRightMCo role rhs mco + lhs_redn = mkGReflRightMRedn role lhs sym_mco + rhs_redn = mkGReflLeftMRedn role rhs mco sym_mco = mkTcSymMCo mco role = eqRelRole eq_rel @@ -2945,9 +2944,8 @@ andWhenContinue tcs1 tcs2 ContinueWith ct -> tcs2 ct } infixr 0 `andWhenContinue` -- allow chaining with ($) -rewriteEvidence :: CtEvidence -- old evidence - -> TcPredType -- new predicate - -> TcCoercion -- Of type :: new predicate ~ <type of old evidence> +rewriteEvidence :: CtEvidence -- ^ old evidence + -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate -> TcS (StopOrContinue CtEvidence) -- Returns Just new_ev iff either (i) 'co' is reflexivity -- or (ii) 'co' is not reflexivity, and 'new_pred' not cached @@ -2983,7 +2981,7 @@ as well as in old_pred; that is important for good error messages. -} -rewriteEvidence old_ev@(CtDerived {}) new_pred _co +rewriteEvidence old_ev@(CtDerived {}) (Reduction _co new_pred) = -- If derived, don't even look at the coercion. -- This is very important, DO NOT re-order the equations for -- rewriteEvidence to put the isTcReflCo test first! @@ -2993,30 +2991,28 @@ rewriteEvidence old_ev@(CtDerived {}) new_pred _co -- (Getting this wrong caused #7384.) continueWith (old_ev { ctev_pred = new_pred }) -rewriteEvidence old_ev new_pred co +rewriteEvidence old_ev (Reduction co new_pred) | isTcReflCo co -- See Note [Rewriting with Refl] = continueWith (old_ev { ctev_pred = new_pred }) -rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) new_pred co +rewriteEvidence ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) (Reduction co new_pred) = do { new_ev <- newGivenEvVar loc (new_pred, new_tm) ; continueWith new_ev } where -- mkEvCast optimises ReflCo - new_tm = mkEvCast (evId old_evar) (tcDowngradeRole Representational - (ctEvRole ev) - (mkTcSymCo co)) + new_tm = mkEvCast (evId old_evar) + (tcDowngradeRole Representational (ctEvRole ev) co) rewriteEvidence ev@(CtWanted { ctev_dest = dest , ctev_nosh = si - , ctev_loc = loc }) new_pred co + , ctev_loc = loc }) (Reduction co new_pred) = do { mb_new_ev <- newWanted_SI si loc new_pred -- The "_SI" variant ensures that we make a new Wanted - -- with the same shadow-info as the existing one -- with the same shadow-info as the existing one (#16735) ; massert (tcCoercionRole co == ctEvRole ev) ; setWantedEvTerm dest (mkEvCast (getEvExpr mb_new_ev) - (tcDowngradeRole Representational (ctEvRole ev) co)) + (tcDowngradeRole Representational (ctEvRole ev) (mkSymCo co))) ; case mb_new_ev of Fresh new_ev -> continueWith new_ev Cached _ -> stopWith ev "Cached wanted" } @@ -3025,26 +3021,25 @@ rewriteEvidence ev@(CtWanted { ctev_dest = dest rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swapped) -- or orhs ~ olhs (swapped) -> SwapFlag - -> TcType -> TcType -- New predicate nlhs ~ nrhs - -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs - -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs + -> Reduction -- lhs_co :: olhs ~ nlhs + -> Reduction -- rhs_co :: orhs ~ nrhs -> TcS CtEvidence -- Of type nlhs ~ nrhs --- For (rewriteEqEvidence (Given g olhs orhs) False nlhs nrhs lhs_co rhs_co) --- we generate +-- With reductions (Reduction lhs_co nlhs) (Reduction rhs_co nrhs), +-- rewriteEqEvidence yields, for a given equality (Given g olhs orhs): -- If not swapped --- g1 : nlhs ~ nrhs = lhs_co ; g ; sym rhs_co --- If 'swapped' --- g1 : nlhs ~ nrhs = lhs_co ; Sym g ; sym rhs_co +-- g1 : nlhs ~ nrhs = sym lhs_co ; g ; rhs_co +-- If swapped +-- g1 : nlhs ~ nrhs = sym lhs_co ; Sym g ; rhs_co -- --- For (Wanted w) we do the dual thing. +-- For a wanted equality (Wanted w), we do the dual thing: -- New w1 : nlhs ~ nrhs -- If not swapped --- w : olhs ~ orhs = sym lhs_co ; w1 ; rhs_co +-- w : olhs ~ orhs = lhs_co ; w1 ; sym rhs_co -- If swapped --- w : orhs ~ olhs = sym rhs_co ; sym w1 ; lhs_co +-- w : orhs ~ olhs = rhs_co ; sym w1 ; sym lhs_co -- --- It's all a form of rewwriteEvidence, specialised for equalities -rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co +-- It's all a form of rewriteEvidence, specialised for equalities +rewriteEqEvidence old_ev swapped (Reduction lhs_co nlhs) (Reduction rhs_co nrhs) | CtDerived {} <- old_ev -- Don't force the evidence for a Derived = return (old_ev { ctev_pred = new_pred }) @@ -3054,9 +3049,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co = return (old_ev { ctev_pred = new_pred }) | CtGiven { ctev_evar = old_evar } <- old_ev - = do { let new_tm = evCoercion (lhs_co + = do { let new_tm = evCoercion ( mkTcSymCo lhs_co `mkTcTransCo` maybeTcSymCo swapped (mkTcCoVarCo old_evar) - `mkTcTransCo` mkTcSymCo rhs_co) + `mkTcTransCo` rhs_co) ; newGivenEvVar loc' (new_pred, new_tm) } | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev @@ -3065,9 +3060,9 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co -- The "_SI" variant ensures that we make a new Wanted -- with the same shadow-info as the existing one (#16735) ; let co = maybeTcSymCo swapped $ - mkSymCo lhs_co + lhs_co `mkTransCo` hole_co - `mkTransCo` rhs_co + `mkTransCo` mkTcSymCo rhs_co ; setWantedEq dest co ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co]) ; return new_ev } diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index c5252fb09a..5f41ca4ffd 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -36,12 +36,12 @@ import GHC.Prelude import GHC.Tc.Solver.Types import GHC.Tc.Types.Constraint -import GHC.Tc.Types.Evidence import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType import GHC.Types.Var import GHC.Types.Var.Env +import GHC.Core.Reduction import GHC.Core.Predicate import GHC.Core.TyCo.FVs import qualified GHC.Core.TyCo.Rep as Rep @@ -243,12 +243,12 @@ data InertSet -- used to undo the cycle-breaking needed to handle -- Note [Type variable cycles] in GHC.Tc.Solver.Canonical - , inert_famapp_cache :: FunEqMap (TcCoercion, TcType) + , inert_famapp_cache :: FunEqMap Reduction -- Just a hash-cons cache for use when reducing family applications -- only -- -- If F tys :-> (co, rhs, flav), - -- then co :: rhs ~N F tys + -- then co :: F tys ~N rhs -- all evidence is from instances or Givens; no coercion holes here -- (We have no way of "kicking out" from the cache, so putting -- wanteds here means we can end up solving a Wanted with itself. Bad) diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 4b0523b7f2..750b21f9c5 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -138,6 +138,7 @@ import GHC.Driver.Session import GHC.Core.Type import qualified GHC.Core.TyCo.Rep as Rep -- this needs to be used only very locally import GHC.Core.Coercion +import GHC.Core.Reduction import GHC.Tc.Solver.Types import GHC.Tc.Solver.InertSet @@ -175,7 +176,6 @@ import Data.IORef import GHC.Exts (oneShot) import Data.List ( mapAccumL, partition ) import Data.List.NonEmpty ( NonEmpty(..) ) -import Control.Arrow ( first ) #if defined(DEBUG) import GHC.Data.Graph.Directed @@ -1072,9 +1072,8 @@ removeInertCt is ct = CIrredCan {} -> panic "removeInertCt: CIrredEvCan" CNonCanonical {} -> panic "removeInertCt: CNonCanonical" --- | Looks up a family application in the inerts; returned coercion --- is oriented input ~ output -lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavourRole)) +-- | Looks up a family application in the inerts. +lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) lookupFamAppInert fam_tc tys = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getTcSInerts ; return (lookup_inerts inert_funeqs) } @@ -1082,7 +1081,8 @@ lookupFamAppInert fam_tc tys lookup_inerts inert_funeqs | Just (EqualCtList (CEqCan { cc_ev = ctev, cc_rhs = rhs } :| _)) <- findFunEq inert_funeqs fam_tc tys - = Just (ctEvCoercion ctev, rhs, ctEvFlavourRole ctev) + = Just (mkReduction (ctEvCoercion ctev) rhs + ,ctEvFlavourRole ctev) | otherwise = Nothing lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence) @@ -1111,20 +1111,19 @@ lookupSolvedDict (IS { inert_solved_dicts = solved }) loc cls tys _ -> Nothing --------------------------- -lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType)) +lookupFamAppCache :: TyCon -> [Type] -> TcS (Maybe Reduction) lookupFamAppCache fam_tc tys = do { IS { inert_famapp_cache = famapp_cache } <- getTcSInerts ; case findFunEq famapp_cache fam_tc tys of - result@(Just (co, ty)) -> + result@(Just redn) -> do { traceTcS "famapp_cache hit" (vcat [ ppr (mkTyConApp fam_tc tys) - , ppr ty - , ppr co ]) + , ppr redn ]) ; return result } Nothing -> return Nothing } -extendFamAppCache :: TyCon -> [Type] -> (TcCoercion, TcType) -> TcS () +extendFamAppCache :: TyCon -> [Type] -> Reduction -> TcS () -- NB: co :: rhs ~ F tys, to match expectations of rewriter -extendFamAppCache tc xi_args stuff@(_, ty) +extendFamAppCache tc xi_args stuff@(Reduction _ ty) = do { dflags <- getDynFlags ; when (gopt Opt_FamAppCache dflags) $ do { traceTcS "extendFamAppCache" (vcat [ ppr tc <+> ppr xi_args @@ -1141,8 +1140,9 @@ dropFromFamAppCache varset ; let filtered = filterTcAppMap check famapp_cache ; setTcSInerts $ inerts { inert_famapp_cache = filtered } } where - check :: (TcCoercion, TcType) -> Bool - check (co, _) = not (anyFreeVarsOfCo (`elemVarSet` varset) co) + check :: Reduction -> Bool + check redn + = not (anyFreeVarsOfCo (`elemVarSet` varset) $ reductionCoercion redn) {- ********************************************************************* * * @@ -2190,11 +2190,10 @@ checkReductionDepth loc ty wrapErrTcS $ solverDepthErrorTcS loc ty } -matchFam :: TyCon -> [Type] -> TcS (Maybe (CoercionN, TcType)) --- Given (F tys) return (ty, co), where co :: ty ~N F tys -matchFam tycon args = fmap (fmap (first mkTcSymCo)) $ wrapTcS $ matchFamTcM tycon args +matchFam :: TyCon -> [Type] -> TcS (Maybe ReductionN) +matchFam tycon args = wrapTcS $ matchFamTcM tycon args -matchFamTcM :: TyCon -> [Type] -> TcM (Maybe (CoercionN, TcType)) +matchFamTcM :: TyCon -> [Type] -> TcM (Maybe ReductionN) -- Given (F tys) return (ty, co), where co :: F tys ~N ty matchFamTcM tycon args = do { fam_envs <- FamInst.tcGetFamInstEnvs @@ -2205,10 +2204,11 @@ matchFamTcM tycon args , ppr_res match_fam_result ] ; return match_fam_result } where - ppr_res Nothing = text "Match failed" - ppr_res (Just (co,ty)) = hang (text "Match succeeded:") - 2 (vcat [ text "Rewrites to:" <+> ppr ty - , text "Coercion:" <+> ppr co ]) + ppr_res Nothing = text "Match failed" + ppr_res (Just (Reduction co ty)) + = hang (text "Match succeeded:") + 2 (vcat [ text "Rewrites to:" <+> ppr ty + , text "Coercion:" <+> ppr co ]) {- ************************************************************************ @@ -2227,9 +2227,8 @@ breakTyVarCycle_maybe :: CtEvidence -> CheckTyEqResult -- result of checkTypeEq -> CanEqLHS -> TcType -- RHS - -> TcS (Maybe (TcTyVar, CoercionN, TcType)) + -> TcS (Maybe (TcTyVar, ReductionN)) -- new RHS that doesn't have any type families - -- co :: new type ~N old type -- TcTyVar is the LHS tv; convenient for the caller breakTyVarCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _ -- see Detail (7) of Note @@ -2243,8 +2242,8 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs -- See Detail (8) of the Note. = do { should_break <- final_check - ; if should_break then do { (co, new_rhs) <- go rhs - ; return (Just (lhs_tv, co, new_rhs)) } + ; if should_break then do { redn <- go rhs + ; return (Just (lhs_tv, redn)) } else return Nothing } where flavour = ctEvFlavour ev @@ -2262,7 +2261,7 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs = return False -- This could be considerably more efficient. See Detail (5) of Note. - go :: TcType -> TcS (CoercionN, TcType) + go :: TcType -> TcS ReductionN go ty | Just ty' <- rewriterView ty = go ty' go (Rep.TyConApp tc tys) | isTypeFamilyTyCon tc -- worried about whether this type family is not actually @@ -2270,41 +2269,32 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs = do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys fun_app = mkTyConApp tc fun_args fun_app_kind = tcTypeKind fun_app - ; (co, new_ty) <- emit_work fun_app_kind fun_app - ; (extra_args_cos, extra_args') <- mapAndUnzipM go extra_args - ; return (mkAppCos co extra_args_cos, mkAppTys new_ty extra_args') } + ; fun_redn <- emit_work fun_app_kind fun_app + ; arg_redns <- unzipRedns <$> mapM go extra_args + ; return $ mkAppRedns fun_redn arg_redns } -- Worried that this substitution will change kinds? -- See Detail (3) of Note | otherwise - = do { (cos, tys) <- mapAndUnzipM go tys - ; return (mkTyConAppCo Nominal tc cos, mkTyConApp tc tys) } + = do { arg_redns <- unzipRedns <$> mapM go tys + ; return $ mkTyConAppRedn Nominal tc arg_redns } go (Rep.AppTy ty1 ty2) - = do { (co1, ty1') <- go ty1 - ; (co2, ty2') <- go ty2 - ; return (mkAppCo co1 co2, mkAppTy ty1' ty2') } + = mkAppRedn <$> go ty1 <*> go ty2 go (Rep.FunTy vis w arg res) - = do { (co_w, w') <- go w - ; (co_arg, arg') <- go arg - ; (co_res, res') <- go res - ; return (mkFunCo Nominal co_w co_arg co_res, mkFunTy vis w' arg' res') } + = mkFunRedn Nominal vis <$> go w <*> go arg <*> go res go (Rep.CastTy ty cast_co) - = do { (co, ty') <- go ty - -- co :: ty' ~N ty - -- return_co :: (ty' |> cast_co) ~ (ty |> cast_co) - ; return (castCoercionKind1 co Nominal ty' ty cast_co, mkCastTy ty' cast_co) } - + = mkCastRedn1 Nominal ty cast_co <$> go ty go ty@(Rep.TyVarTy {}) = skip ty go ty@(Rep.LitTy {}) = skip ty go ty@(Rep.ForAllTy {}) = skip ty -- See Detail (1) of Note go ty@(Rep.CoercionTy {}) = skip ty -- See Detail (2) of Note - skip ty = return (mkNomReflCo ty, ty) + skip ty = return $ mkReflRedn Nominal ty - emit_work :: TcKind -- of the function application - -> TcType -- original function application - -> TcS (CoercionN, TcType) -- rewritten type (the fresh tyvar) + emit_work :: TcKind -- of the function application + -> TcType -- original function application + -> TcS ReductionN -- rewritten type (the fresh tyvar) emit_work fun_app_kind fun_app = case flavour of Given -> do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind) @@ -2318,14 +2308,14 @@ breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs ; updInertTcS $ \is -> is { inert_cycle_breakers = (new_tv, fun_app) : inert_cycle_breakers is } - ; return (mkNomReflCo new_ty, new_ty) } + ; return $ mkReflRedn Nominal new_ty } -- Why reflexive? See Detail (4) of the Note _derived_or_wd -> do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind) ; let new_ty = mkTyVarTy new_tv ; co <- emitNewWantedEq new_loc Nominal new_ty fun_app - ; return (co, new_ty) } + ; return $ mkReduction (mkSymCo co) new_ty } -- See Detail (7) of the Note new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 13f6c4ce1b..cf95fd8b3a 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -20,6 +20,7 @@ import GHC.Tc.Types.Evidence import GHC.Core.TyCon import GHC.Core.TyCo.Rep -- performs delicate algorithm on types import GHC.Core.Coercion +import GHC.Core.Reduction import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Var.Env @@ -29,7 +30,6 @@ import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Tc.Solver.Monad as TcS import GHC.Tc.Solver.Types - import GHC.Utils.Misc import GHC.Data.Maybe import GHC.Exts (oneShot) @@ -37,8 +37,6 @@ import Control.Monad import GHC.Utils.Monad ( zipWith3M ) import Data.List.NonEmpty ( NonEmpty(..) ) -import Control.Arrow ( first ) - {- ************************************************************************ * * @@ -221,28 +219,29 @@ changes the flavour from Derived just for this purpose. -- If (xi, co) <- rewrite mode ev ty, then co :: xi ~r ty -- where r is the role in @ev@. rewrite :: CtEvidence -> TcType - -> TcS (Xi, TcCoercion) + -> TcS Reduction rewrite ev ty = do { traceTcS "rewrite {" (ppr ty) - ; (ty', co) <- runRewriteCtEv ev (rewrite_one ty) - ; traceTcS "rewrite }" (ppr ty') - ; return (ty', co) } + ; redn <- runRewriteCtEv ev (rewrite_one ty) + ; traceTcS "rewrite }" (ppr $ reductionReducedType redn) + ; return redn } -- specialized to rewriting kinds: never Derived, always Nominal -- See Note [No derived kind equalities] -- See Note [Rewriting] -rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS (Xi, TcCoercionN) +rewriteKind :: CtLoc -> CtFlavour -> TcType -> TcS ReductionN rewriteKind loc flav ty = do { traceTcS "rewriteKind {" (ppr flav <+> ppr ty) ; let flav' = case flav of Derived -> Wanted WDeriv -- the WDeriv/WOnly choice matters not _ -> flav - ; (ty', co) <- runRewrite loc flav' NomEq (rewrite_one ty) - ; traceTcS "rewriteKind }" (ppr ty' $$ ppr co) -- co is never a panic - ; return (ty', co) } + ; redn <- runRewrite loc flav' NomEq (rewrite_one ty) + ; traceTcS "rewriteKind }" (ppr redn) -- the coercion inside the reduction is never a panic + ; return redn } -- See Note [Rewriting] -rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion]) +rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] + -> TcS Reductions -- Externally-callable, hence runRewrite -- Rewrite a vector of types all at once; in fact they are -- always the arguments of type family or class, so @@ -255,11 +254,11 @@ rewriteArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion]) -- because rewriting may use a Derived equality ([D] a ~ ty) rewriteArgsNom ev tc tys = do { traceTcS "rewrite_args {" (vcat (map ppr tys)) - ; (tys', cos, kind_co) + ; ArgsReductions redns@(Reductions _ tys') kind_co <- runRewriteCtEv ev (rewrite_args_tc tc Nothing tys) ; massert (isReflMCo kind_co) ; traceTcS "rewrite }" (vcat (map ppr tys')) - ; return (tys', cos) } + ; return redns } -- | Rewrite a type w.r.t. nominal equality. This is useful to rewrite -- a type w.r.t. any givens. It does not do type-family reduction. This @@ -267,13 +266,13 @@ rewriteArgsNom ev tc tys -- only givens. rewriteType :: CtLoc -> TcType -> TcS TcType rewriteType loc ty - = do { (xi, _) <- runRewrite loc Given NomEq $ + = do { redn <- runRewrite loc Given NomEq $ rewrite_one ty -- use Given flavor so that it is rewritten -- only w.r.t. Givens, never Wanteds/Deriveds -- (Shouldn't matter, if only Givens are present -- anyway) - ; return xi } + ; return $ reductionReducedType redn } {- ********************************************************************* * * @@ -283,15 +282,15 @@ rewriteType loc ty {- Note [Rewriting] ~~~~~~~~~~~~~~~~~~~~ - rewrite ty ==> (xi, co) + rewrite ty ==> Reduction co xi where xi has no reducible type functions has no skolems that are mapped in the inert set has no filled-in metavariables - co :: xi ~ ty + co :: ty ~ xi (coercions in reductions are always left-to-right) Key invariants: - (F0) co :: xi ~ zonk(ty') where zonk(ty') ~ zonk(ty) + (F0) co :: zonk(ty') ~ xi where zonk(ty') ~ zonk(ty) (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty)) @@ -302,18 +301,17 @@ Rewriting also: * applies the substitution embodied in the inert set Because rewriting zonks and the returned coercion ("co" above) is also -zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead, +zonked, it's possible that (co :: ty ~ xi) isn't quite true. So, instead, we can rely on this fact: - (F0) co :: xi ~ zonk(ty'), where zonk(ty') ~ zonk(ty) + (F0) co :: zonk(ty') ~ xi, where zonk(ty') ~ zonk(ty) -Note that the left-hand type of co is *always* precisely xi. The right-hand +Note that the right-hand type of co is *always* precisely xi. The left-hand type may or may not be ty, however: if ty has unzonked filled-in metavariables, -then the right-hand type of co will be the zonk-equal to ty. -It is for this reason that we -occasionally have to explicitly zonk, when (co :: xi ~ ty) is important -even before we zonk the whole program. For example, see the RTRNotFollowed -case in rewriteTyVar. +then the left-hand type of co will be the zonk-equal to ty. +It is for this reason that we occasionally have to explicitly zonk, +when (co :: ty ~ xi) is important even before we zonk the whole program. +For example, see the RTRNotFollowed case in rewriteTyVar. Why have these invariants on rewriting? Because we sometimes use tcTypeKind during canonicalisation, and we want this kind to be zonked (e.g., see @@ -322,7 +320,7 @@ GHC.Tc.Solver.Canonical.canEqCanLHS). Rewriting is always homogeneous. That is, the kind of the result of rewriting is always the same as the kind of the input, modulo zonking. More formally: - (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty)) + (F2) zonk(tcTypeKind(ty)) `eqType` tcTypeKind(xi) This invariant means that the kind of a rewritten type might not itself be rewritten. @@ -388,17 +386,15 @@ rewrite_args_tc :: TyCon -- T -> Maybe [Role] -- Nothing: ambient role is Nominal; all args are Nominal -- Otherwise: no assumptions; use roles provided - -> [Type] -- Arg types [t1,..,tn] - -> RewriteM ( [Xi] -- List of rewritten args [x1,..,xn] - -- 1-1 corresp with [t1,..,tn] - , [Coercion] -- List of arg coercions [co1,..,con] - -- 1-1 corresp with [t1,..,tn] - -- coi :: xi ~r ti - , MCoercionN) -- Result coercion, rco - -- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con)) + -> [Type] + -> RewriteM ArgsReductions -- See the commentary on rewrite_args rewrite_args_tc tc = rewrite_args all_bndrs any_named_bndrs inner_ki emptyVarSet -- NB: TyCon kinds are always closed where + -- There are many bang patterns in here. It's been observed that they + -- greatly improve performance of an optimized build. + -- The T9872 test cases are good witnesses of this fact. + (bndrs, named) = ty_con_binders_ty_binders' (tyConBinders tc) -- it's possible that the result kind has arrows (for, e.g., a type family) @@ -414,13 +410,15 @@ rewrite_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are -> Kind -> TcTyCoVarSet -- function kind; kind's free vars -> Maybe [Role] -> [Type] -- these are in 1-to-1 correspondence -- Nothing: use all Nominal - -> RewriteM ([Xi], [Coercion], MCoercionN) --- Coercions :: Xi ~ Type, at roles given --- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys) --- That is, the third coercion relates the kind of some function (whose kind is --- passed as the first parameter) instantiated at xis to the kind of that --- function instantiated at the tys. This is useful in keeping rewriting --- homoegeneous. The list of roles must be at least as long as the list of + -> RewriteM ArgsReductions +-- This function returns ArgsReductions (Reductions cos xis) res_co +-- coercions: co_i :: ty_i ~ xi_i, at roles given +-- types: xi_i +-- coercion: res_co :: tcTypeKind(fun tys) ~N tcTypeKind(fun xis) +-- That is, the result coercion relates the kind of some function (whose kind is +-- passed as the first parameter) instantiated at tys to the kind of that +-- function instantiated at the xis. This is useful in keeping rewriting +-- homogeneous. The list of roles must be at least as long as the list of -- types. rewrite_args orig_binders any_named_bndrs @@ -436,33 +434,28 @@ rewrite_args orig_binders {-# INLINE rewrite_args_fast #-} -- | fast path rewrite_args, in which none of the binders are named and -- therefore we can avoid tracking a lifting context. --- There are many bang patterns in here. It's been observed that they --- greatly improve performance of an optimized build. --- The T9872 test cases are good witnesses of this fact. -rewrite_args_fast :: [Type] - -> RewriteM ([Xi], [Coercion], MCoercionN) +rewrite_args_fast :: [Type] -> RewriteM ArgsReductions rewrite_args_fast orig_tys = fmap finish (iterate orig_tys) where - iterate :: [Type] - -> RewriteM ([Xi], [Coercion]) - iterate (ty:tys) = do - (xi, co) <- rewrite_one ty - (xis, cos) <- iterate tys - pure (xi : xis, co : cos) - iterate [] = pure ([], []) + iterate :: [Type] -> RewriteM Reductions + iterate (ty : tys) = do + Reduction co xi <- rewrite_one ty + Reductions cos xis <- iterate tys + pure $ Reductions (co : cos) (xi : xis) + iterate [] = pure $ Reductions [] [] {-# INLINE finish #-} - finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN) - finish (xis, cos) = (xis, cos, MRefl) + finish :: Reductions -> ArgsReductions + finish redns = ArgsReductions redns MRefl {-# INLINE rewrite_args_slow #-} -- | Slow path, compared to rewrite_args_fast, because this one must track -- a lifting context. rewrite_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet -> [Role] -> [Type] - -> RewriteM ([Xi], [Coercion], MCoercionN) + -> RewriteM ArgsReductions rewrite_args_slow binders inner_ki fvs roles tys -- Arguments used dependently must be rewritten with proper coercions, but -- we're not guaranteed to get a proper coercion when rewriting with the @@ -476,17 +469,17 @@ rewrite_args_slow binders inner_ki fvs roles tys -- Note [No derived kind equalities] = do { rewritten_args <- zipWith3M fl (map isNamedBinder binders ++ repeat True) roles tys - ; return (simplifyArgsWorker binders inner_ki fvs roles rewritten_args) } + ; return $ simplifyArgsWorker binders inner_ki fvs roles rewritten_args } where {-# INLINE fl #-} fl :: Bool -- must we ensure to produce a real coercion here? - -- see comment at top of function - -> Role -> Type -> RewriteM (Xi, Coercion) + -- see comment at top of function + -> Role -> Type -> RewriteM Reduction fl True r ty = noBogusCoercions $ fl1 r ty fl False r ty = fl1 r ty {-# INLINE fl1 #-} - fl1 :: Role -> Type -> RewriteM (Xi, Coercion) + fl1 :: Role -> Type -> RewriteM Reduction fl1 Nominal ty = setEqRel NomEq $ rewrite_one ty @@ -498,16 +491,16 @@ rewrite_args_slow binders inner_ki fvs roles tys fl1 Phantom ty -- See Note [Phantoms in the rewriter] = do { ty <- liftTcS $ zonkTcType ty - ; return (ty, mkReflCo Phantom ty) } + ; return $ mkReflRedn Phantom ty } ------------------ -rewrite_one :: TcType -> RewriteM (Xi, Coercion) +rewrite_one :: TcType -> RewriteM Reduction -- Rewrite a type to get rid of type function applications, returning -- the new type-function-free type, and a collection of new equality -- constraints. See Note [Rewriting] for more detail. -- --- Postcondition: Coercion :: Xi ~ TcType --- The role on the result coercion matches the EqRel in the RewriteEnv +-- Postcondition: +-- the role on the result coercion matches the EqRel in the RewriteEnv rewrite_one ty | Just ty' <- rewriterView ty -- See Note [Rewriting synonyms] @@ -515,7 +508,7 @@ rewrite_one ty rewrite_one xi@(LitTy {}) = do { role <- getRole - ; return (xi, mkReflCo role xi) } + ; return $ mkReflRedn role xi } rewrite_one (TyVarTy tv) = rewriteTyVar tv @@ -534,13 +527,12 @@ rewrite_one (TyConApp tc tys) | otherwise = rewrite_ty_con_app tc tys -rewrite_one ty@(FunTy { ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) - = do { (xi1,co1) <- rewrite_one ty1 - ; (xi2,co2) <- rewrite_one ty2 - ; (xi3,co3) <- setEqRel NomEq $ rewrite_one mult +rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 }) + = do { arg_redn <- rewrite_one ty1 + ; res_redn <- rewrite_one ty2 + ; w_redn <- setEqRel NomEq $ rewrite_one mult ; role <- getRole - ; return (ty { ft_mult = xi3, ft_arg = xi1, ft_res = xi2 } - , mkFunCo role co3 co1 co2) } + ; return $ mkFunRedn role vis w_redn arg_redn res_redn } rewrite_one ty@(ForAllTy {}) -- TODO (RAE): This is inadequate, as it doesn't rewrite the kind of @@ -550,126 +542,116 @@ rewrite_one ty@(ForAllTy {}) -- We allow for-alls when, but only when, no type function -- applications inside the forall involve the bound type variables. = do { let (bndrs, rho) = tcSplitForAllTyVarBinders ty - tvs = binderVars bndrs - ; (rho', co) <- rewrite_one rho - ; return (mkForAllTys bndrs rho', mkHomoForAllCos tvs co) } + ; redn <- rewrite_one rho + ; return $ mkHomoForAllRedn bndrs redn } rewrite_one (CastTy ty g) - = do { (xi, co) <- rewrite_one ty - ; (g', _) <- rewrite_co g + = do { redn <- rewrite_one ty + ; g' <- rewrite_co g ; role <- getRole - ; return (mkCastTy xi g', castCoercionKind1 co role xi ty g') } - -- It makes a /big/ difference to call castCoercionKind1 not - -- the more general castCoercionKind2. - -- See Note [castCoercionKind1] in GHC.Core.Coercion - -rewrite_one (CoercionTy co) = first mkCoercionTy <$> rewrite_co co + ; return $ mkCastRedn1 role ty g' redn } + -- This calls castCoercionKind1. + -- It makes a /big/ difference to call castCoercionKind1 not + -- the more general castCoercionKind2. + -- See Note [castCoercionKind1] in GHC.Core.Coercion + +rewrite_one (CoercionTy co) + = do { co' <- rewrite_co co + ; role <- getRole + ; return $ mkReflCoRedn role co' } -- | "Rewrite" a coercion. Really, just zonk it so we can uphold -- (F1) of Note [Rewriting] -rewrite_co :: Coercion -> RewriteM (Coercion, Coercion) -rewrite_co co - = do { co <- liftTcS $ zonkCo co - ; env_role <- getRole - ; let co' = mkTcReflCo env_role (mkCoercionTy co) - ; return (co, co') } +rewrite_co :: Coercion -> RewriteM Coercion +rewrite_co co = liftTcS $ zonkCo co + +-- | Rewrite a reduction, composing the resulting coercions. +rewrite_reduction :: Reduction -> RewriteM Reduction +rewrite_reduction (Reduction co xi) + = do { redn <- bumpDepth $ rewrite_one xi + ; return $ co `mkTransRedn` redn } -- rewrite (nested) AppTys -rewrite_app_tys :: Type -> [Type] -> RewriteM (Xi, Coercion) +rewrite_app_tys :: Type -> [Type] -> RewriteM Reduction -- commoning up nested applications allows us to look up the function's kind -- only once. Without commoning up like this, we would spend a quadratic amount -- of time looking up functions' types rewrite_app_tys (AppTy ty1 ty2) tys = rewrite_app_tys ty1 (ty2:tys) rewrite_app_tys fun_ty arg_tys - = do { (fun_xi, fun_co) <- rewrite_one fun_ty - ; rewrite_app_ty_args fun_xi fun_co arg_tys } + = do { redn <- rewrite_one fun_ty + ; rewrite_app_ty_args redn arg_tys } -- Given a rewritten function (with the coercion produced by rewriting) and -- a bunch of unrewritten arguments, rewrite the arguments and apply. -- The coercion argument's role matches the role stored in the RewriteM monad. -- -- The bang patterns used here were observed to improve performance. If you --- wish to remove them, be sure to check for regeressions in allocations. -rewrite_app_ty_args :: Xi -> Coercion -> [Type] -> RewriteM (Xi, Coercion) -rewrite_app_ty_args fun_xi fun_co [] +-- wish to remove them, be sure to check for regressions in allocations. +rewrite_app_ty_args :: Reduction -> [Type] -> RewriteM Reduction +rewrite_app_ty_args redn [] -- this will be a common case when called from rewrite_fam_app, so shortcut - = return (fun_xi, fun_co) -rewrite_app_ty_args fun_xi fun_co arg_tys - = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of + = return redn +rewrite_app_ty_args fun_redn@(Reduction fun_co fun_xi) arg_tys + = do { het_redn <- case tcSplitTyConApp_maybe fun_xi of Just (tc, xis) -> do { let tc_roles = tyConRolesRepresentational tc arg_roles = dropList xis tc_roles - ; (arg_xis, arg_cos, kind_co) + ; ArgsReductions (Reductions arg_cos arg_xis) kind_co <- rewrite_vector (tcTypeKind fun_xi) arg_roles arg_tys - -- Here, we have fun_co :: T xi1 xi2 ~ ty - -- and we need to apply fun_co to the arg_cos. The problem is + -- We start with a reduction of the form + -- fun_co :: ty ~ T xi_1 ... xi_n + -- and further arguments a_1, ..., a_m. + -- We rewrite these arguments, and obtain coercions: + -- arg_co_i :: a_i ~ zeta_i + -- Now, we need to apply fun_co to the arg_cos. The problem is -- that using mkAppCo is wrong because that function expects -- its second coercion to be Nominal, and the arg_cos might -- not be. The solution is to use transitivity: - -- T <xi1> <xi2> arg_cos ;; fun_co <arg_tys> + -- fun_co <a_1> ... <a_m> ;; T <xi_1> .. <xi_n> arg_co_1 ... arg_co_m ; eq_rel <- getEqRel ; let app_xi = mkTyConApp tc (xis ++ arg_xis) app_co = case eq_rel of NomEq -> mkAppCos fun_co arg_cos - ReprEq -> mkTcTyConAppCo Representational tc - (zipWith mkReflCo tc_roles xis ++ arg_cos) + ReprEq -> mkAppCos fun_co (map mkNomReflCo arg_tys) `mkTcTransCo` - mkAppCos fun_co (map mkNomReflCo arg_tys) - ; return (app_xi, app_co, kind_co) } + mkTcTyConAppCo Representational tc + (zipWith mkReflCo tc_roles xis ++ arg_cos) + + ; return $ + mkHetReduction + (mkReduction app_co app_xi ) + kind_co } Nothing -> - do { (arg_xis, arg_cos, kind_co) + do { ArgsReductions redns kind_co <- rewrite_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys - ; let arg_xi = mkAppTys fun_xi arg_xis - arg_co = mkAppCos fun_co arg_cos - ; return (arg_xi, arg_co, kind_co) } + ; return $ mkHetReduction (mkAppRedns fun_redn redns) kind_co } ; role <- getRole - ; return (homogenise_result xi co role kind_co) } + ; return (homogeniseHetRedn role het_redn) } -rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion) +rewrite_ty_con_app :: TyCon -> [TcType] -> RewriteM Reduction rewrite_ty_con_app tc tys = do { role <- getRole ; let m_roles | Nominal <- role = Nothing | otherwise = Just $ tyConRolesX role tc - ; (xis, cos, kind_co) <- rewrite_args_tc tc m_roles tys - ; let tyconapp_xi = mkTyConApp tc xis - tyconapp_co = mkTyConAppCo role tc cos - ; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) } - --- Make the result of rewriting homogeneous (Note [Rewriting] (F2)) -homogenise_result :: Xi -- a rewritten type - -> Coercion -- :: xi ~r original ty - -> Role -- r - -> MCoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty) - -> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co) - -- ~r original ty) -homogenise_result xi co _ MRefl = (xi, co) -homogenise_result xi co r mco@(MCo kind_co) - = (xi `mkCastTy` kind_co, (mkSymCo $ GRefl r xi mco) `mkTransCo` co) -{-# INLINE homogenise_result #-} + ; ArgsReductions redns kind_co <- rewrite_args_tc tc m_roles tys + ; let tyconapp_redn + = mkHetReduction + (mkTyConAppRedn role tc redns) + kind_co + ; return $ homogeniseHetRedn role tyconapp_redn } -- Rewrite a vector (list of arguments). rewrite_vector :: Kind -- of the function being applied to these arguments - -> [Role] -- If we're rewrite w.r.t. ReprEq, what roles do the + -> [Role] -- If we're rewriting w.r.t. ReprEq, what roles do the -- args have? -> [Type] -- the args to rewrite - -> RewriteM ([Xi], [Coercion], MCoercionN) + -> RewriteM ArgsReductions rewrite_vector ki roles tys = do { eq_rel <- getEqRel - ; case eq_rel of - NomEq -> rewrite_args bndrs - any_named_bndrs - inner_ki - fvs - Nothing - tys - ReprEq -> rewrite_args bndrs - any_named_bndrs - inner_ki - fvs - (Just roles) - tys + ; let mb_roles = case eq_rel of { NomEq -> Nothing; ReprEq -> Just roles } + ; rewrite_args bndrs any_named_bndrs inner_ki fvs mb_roles tys } where (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki @@ -764,7 +746,7 @@ is inlined in that case, and only FINISH 1 is performed. -} -rewrite_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion) +rewrite_fam_app :: TyCon -> [TcType] -> RewriteM Reduction -- rewrite_fam_app can be over-saturated -- rewrite_exact_fam_app lifts out the application to top level -- Postcondition: Coercion :: Xi ~ F tys @@ -777,14 +759,12 @@ rewrite_fam_app tc tys -- Can be over-saturated -- in which case the remaining arguments should -- be dealt with by AppTys do { let (tys1, tys_rest) = splitAt (tyConArity tc) tys - ; (xi1, co1) <- rewrite_exact_fam_app tc tys1 - -- co1 :: xi1 ~ F tys1 - - ; rewrite_app_ty_args xi1 co1 tys_rest } + ; redn <- rewrite_exact_fam_app tc tys1 + ; rewrite_app_ty_args redn tys_rest } -- the [TcType] exactly saturate the TyCon -- See Note [How to normalise a family application] -rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM (Xi, Coercion) +rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction rewrite_exact_fam_app tc tys = do { checkStackDepth (mkTyConApp tc tys) @@ -793,68 +773,77 @@ rewrite_exact_fam_app tc tys ; case result1 of -- Don't use the cache; -- See Note [rewrite_exact_fam_app performance] - { Just (co, xi) -> finish False (xi, co) + { Just redn -> finish False redn ; Nothing -> -- That didn't work. So reduce the arguments, in STEP 3. do { eq_rel <- getEqRel - -- checking eq_rel == NomEq saves ~0.5% in T9872a - ; (xis, cos, kind_co) <- if eq_rel == NomEq - then rewrite_args_tc tc Nothing tys - else setEqRel NomEq $ - rewrite_args_tc tc Nothing tys - -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys) - - ; let role = eqRelRole eq_rel - args_co = mkTyConAppCo role tc cos - -- args_co :: F xis ~r F tys - - homogenise :: TcType -> TcCoercion -> (TcType, TcCoercion) - -- in (xi', co') = homogenise xi co - -- assume co :: xi ~r F xis, co is homogeneous - -- then xi' :: tcTypeKind(F tys) - -- and co' :: xi' ~r F tys, which is homogeneous - homogenise xi co = homogenise_result xi (co `mkTcTransCo` args_co) role kind_co + -- checking eq_rel == NomEq saves ~0.5% in T9872a + ; ArgsReductions (Reductions cos xis) kind_co <- + if eq_rel == NomEq + then rewrite_args_tc tc Nothing tys + else setEqRel NomEq $ + rewrite_args_tc tc Nothing tys + + -- If we manage to rewrite the type family application after + -- rewriting the arguments, we will need to compose these + -- reductions. + -- + -- We have: + -- + -- arg_co_i :: ty_i ~ xi_i + -- fam_co :: F xi_1 ... xi_n ~ zeta + -- + -- The full reduction is obtained as a composite: + -- + -- full_co :: F ty_1 ... ty_n ~ zeta + -- full_co = F co_1 ... co_n ;; fam_co + ; let + role = eqRelRole eq_rel + args_co = mkTyConAppCo role tc cos + ; let homogenise :: Reduction -> Reduction + homogenise redn + = homogeniseHetRedn role + $ mkHetReduction + (args_co `mkTransRedn` redn) + kind_co -- STEP 4: try the inerts ; result2 <- liftTcS $ lookupFamAppInert tc xis ; flavour <- getFlavour ; case result2 of - { Just (co, xi, fr@(_, inert_eq_rel)) - -- co :: F xis ~ir xi + { Just (redn, fr@(_, inert_eq_rel)) | fr `eqCanRewriteFR` (flavour, eq_rel) -> do { traceRewriteM "rewrite family application with inert" - (ppr tc <+> ppr xis $$ ppr xi) - ; finish True (homogenise xi downgraded_co) } + (ppr tc <+> ppr xis $$ ppr redn) + ; finish True (homogenise downgraded_redn) } -- this will sometimes duplicate an inert in the cache, -- but avoiding doing so had no impact on performance, and -- it seems easier not to weed out that special case where - inert_role = eqRelRole inert_eq_rel - role = eqRelRole eq_rel - downgraded_co = tcDowngradeRole role inert_role (mkTcSymCo co) - -- downgraded_co :: xi ~r F xis + inert_role = eqRelRole inert_eq_rel + role = eqRelRole eq_rel + downgraded_redn = downgradeRedn role inert_role redn ; _ -> -- inert didn't work. Try to reduce again, in STEP 5/6. do { result3 <- try_to_reduce tc xis ; case result3 of - Just (co, xi) -> finish True (homogenise xi co) - Nothing -> -- we have made no progress at all: STEP 7. - return (homogenise reduced (mkTcReflCo role reduced)) + Just redn -> finish True (homogenise redn) + Nothing -> -- we have made no progress at all: STEP 7. + return (homogenise $ mkReflRedn role reduced) where reduced = mkTyConApp tc xis }}}}} where -- call this if the above attempts made progress. -- This recursively rewrites the result and then adds to the cache finish :: Bool -- add to the cache? - -> (Xi, Coercion) -> RewriteM (Xi, Coercion) - finish use_cache (xi, co) + -> Reduction -> RewriteM Reduction + finish use_cache redn = do { -- rewrite the result: FINISH 1 - (fully, fully_co) <- bumpDepth $ rewrite_one xi - ; let final_co = fully_co `mkTcTransCo` co + final_redn <- rewrite_reduction redn ; eq_rel <- getEqRel ; flavour <- getFlavour @@ -863,13 +852,13 @@ rewrite_exact_fam_app tc tys -- the cache only wants Nominal eqs -- and Wanteds can rewrite Deriveds; the cache -- has only Givens - liftTcS $ extendFamAppCache tc tys (final_co, fully) - ; return (fully, final_co) } + liftTcS $ extendFamAppCache tc tys final_redn + ; return final_redn } {-# INLINE finish #-} --- Returned coercion is output ~r input, where r is the role in the RewriteM monad +-- Returned coercion is input ~r output, where r is the role in the RewriteM monad -- See Note [How to normalise a family application] -try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe (TcCoercion, TcType)) +try_to_reduce :: TyCon -> [TcType] -> RewriteM (Maybe Reduction) try_to_reduce tc tys = do { result <- liftTcS $ firstJustsM [ lookupFamAppCache tc tys -- STEP 5 , matchFam tc tys ] -- STEP 6 @@ -877,19 +866,20 @@ try_to_reduce tc tys where -- The result above is always Nominal. We might want a Representational -- coercion; this downgrades (and prints, out of convenience). - downgrade :: Maybe (TcCoercionN, TcType) -> RewriteM (Maybe (TcCoercion, TcType)) + downgrade :: Maybe Reduction -> RewriteM (Maybe Reduction) downgrade Nothing = return Nothing - downgrade result@(Just (co, xi)) + downgrade result@(Just redn) = do { traceRewriteM "Eager T.F. reduction success" $ - vcat [ ppr tc, ppr tys, ppr xi - , ppr co <+> dcolon <+> ppr (coercionKind co) + vcat [ ppr tc + , ppr tys + , ppr redn ] ; eq_rel <- getEqRel -- manually doing it this way avoids allocation in the vastly -- common NomEq case ; case eq_rel of NomEq -> return result - ReprEq -> return (Just (mkSubCo co, xi)) } + ReprEq -> return $ Just (mkSubRedn redn) } {- ************************************************************************ @@ -903,31 +893,27 @@ data RewriteTvResult = RTRNotFollowed -- ^ The inert set doesn't make the tyvar equal to anything else - | RTRFollowed TcType Coercion + | RTRFollowed !Reduction -- ^ The tyvar rewrites to a not-necessarily rewritten other type. - -- co :: new type ~r old type, where the role is determined by - -- the RewriteEnv + -- The role is determined by the RewriteEnv. -- -- With Quick Look, the returned TcType can be a polytype; -- that is, in the constraint solver, a unification variable -- can contain a polytype. See GHC.Tc.Gen.App -- Note [Instantiation variables are short lived] -rewriteTyVar :: TyVar -> RewriteM (Xi, Coercion) +rewriteTyVar :: TyVar -> RewriteM Reduction rewriteTyVar tv = do { mb_yes <- rewrite_tyvar1 tv ; case mb_yes of - RTRFollowed ty1 co1 -- Recur - -> do { (ty2, co2) <- rewrite_one ty1 - -- ; traceRewriteM "rewriteTyVar2" (ppr tv $$ ppr ty2) - ; return (ty2, co2 `mkTransCo` co1) } + RTRFollowed redn -> rewrite_reduction redn RTRNotFollowed -- Done, but make sure the kind is zonked -- Note [Rewriting] invariant (F0) and (F1) -> do { tv' <- liftTcS $ updateTyVarKindM zonkTcType tv ; role <- getRole ; let ty' = mkTyVarTy tv' - ; return (ty', mkTcReflCo role ty') } } + ; return $ mkReflRedn role ty' } } rewrite_tyvar1 :: TcTyVar -> RewriteM RewriteTvResult -- "Rewriting" a type variable means to apply the substitution to it @@ -942,7 +928,8 @@ rewrite_tyvar1 tv Just ty -> do { traceRewriteM "Following filled tyvar" (ppr tv <+> equals <+> ppr ty) ; role <- getRole - ; return (RTRFollowed ty (mkReflCo role ty)) } ; + ; return $ RTRFollowed $ + mkReflRedn role ty } Nothing -> do { traceRewriteM "Unfilled tyvar" (pprTyVar tv) ; fr <- getFlavourRole ; rewrite_tyvar2 tv fr } } @@ -966,16 +953,16 @@ rewrite_tyvar2 tv fr@(_, eq_rel) (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev) - ; let rewrite_co1 = mkSymCo (ctEvCoercion ctev) - rewrite_co = case (ct_eq_rel, eq_rel) of + ; let rewriting_co1 = ctEvCoercion ctev + rewriting_co = case (ct_eq_rel, eq_rel) of (ReprEq, _rel) -> assert (_rel == ReprEq ) -- if this ASSERT fails, then -- eqCanRewriteFR answered incorrectly - rewrite_co1 - (NomEq, NomEq) -> rewrite_co1 - (NomEq, ReprEq) -> mkSubCo rewrite_co1 + rewriting_co1 + (NomEq, NomEq) -> rewriting_co1 + (NomEq, ReprEq) -> mkSubCo rewriting_co1 - ; return (RTRFollowed rhs_ty rewrite_co) } + ; return $ RTRFollowed $ mkReduction rewriting_co rhs_ty } -- NB: ct is Derived then fmode must be also, hence -- we are not going to touch the returned coercion -- so ctEvCoercion is fine. |