diff options
Diffstat (limited to 'compiler/GHC/Core/FamInstEnv.hs')
| -rw-r--r-- | compiler/GHC/Core/FamInstEnv.hs | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs index c5445fceae..a6c7604008 100644 --- a/compiler/GHC/Core/FamInstEnv.hs +++ b/compiler/GHC/Core/FamInstEnv.hs @@ -428,7 +428,8 @@ Here is how we do it: apart(target, pattern) = not (unify(flatten(target), pattern)) where flatten (implemented in flattenTys, below) converts all type-family -applications into fresh variables. (See Note [Flattening] in GHC.Core.Unify.) +applications into fresh variables. (See +Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.) Note [Compatibility] ~~~~~~~~~~~~~~~~~~~~ @@ -1141,6 +1142,7 @@ reduceTyFamApp_maybe envs role tc tys | Just ax <- isBuiltInSynFamTyCon_maybe tc , Just (coax,ts,ty) <- sfMatchFam ax tys + , role == coaxrRole coax = let co = mkAxiomRuleCo coax (zipWith mkReflCo (coaxrAsmpRoles coax) ts) in Just (co, ty) @@ -1175,7 +1177,8 @@ findBranch branches target_tys , cab_incomps = incomps }) = branch in_scope = mkInScopeSet (unionVarSets $ map (tyCoVarsOfTypes . coAxBranchLHS) incomps) - -- See Note [Flattening] in GHC.Core.Unify + -- See Note [Flattening type-family applications when matching instances] + -- in GHC.Core.Unify flattened_target = flattenTys in_scope target_tys in case tcMatchTys tpl_lhs target_tys of Just subst -- matching worked. now, check for apartness. @@ -1192,11 +1195,11 @@ findBranch branches target_tys -- (POPL '14). This should be used when determining if an equation -- ('CoAxBranch') of a closed type family can be used to reduce a certain target -- type family application. -apartnessCheck :: [Type] -- ^ /flattened/ target arguments. Make sure - -- they're flattened! See Note [Flattening] - -- in GHC.Core.Unify - -- (NB: This "flat" is a different - -- "flat" than is used in GHC.Tc.Solver.Flatten.) +apartnessCheck :: [Type] + -- ^ /flattened/ target arguments. Make sure they're flattened! See + -- Note [Flattening type-family applications when matching instances] + -- in GHC.Core.Unify. (NB: This "flat" is a different + -- "flat" than is used in GHC.Tc.Solver.Flatten.) -> CoAxBranch -- ^ the candidate equation we wish to use -- Precondition: this matches the target -> Bool -- ^ True <=> equation can fire @@ -1316,7 +1319,7 @@ topNormaliseType_maybe env ty tyFamStepper :: NormaliseStepper (Coercion, MCoercionN) tyFamStepper rec_nts tc tys -- Try to step a type/data family = case topReduceTyFamApp_maybe env tc tys of - Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, MCo res_co) + Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, res_co) _ -> NS_Done --------------- @@ -1362,14 +1365,14 @@ normalise_tc_app tc tys assemble_result :: Role -- r, ambient role in NormM monad -> Type -- nty, result type, possibly of changed kind -> Coercion -- orig_ty ~r nty, possibly heterogeneous - -> CoercionN -- typeKind(orig_ty) ~N typeKind(nty) + -> MCoercionN -- typeKind(orig_ty) ~N typeKind(nty) -> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted) -- where nty_casted has same kind as orig_ty assemble_result r nty orig_to_nty kind_co = ( final_co, nty_old_kind ) where - nty_old_kind = nty `mkCastTy` mkSymCo kind_co - final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty + nty_old_kind = nty `mkCastTyMCo` mkSymMCo kind_co + final_co = mkCoherenceRightMCo r nty (mkSymMCo kind_co) orig_to_nty --------------- -- | Try to simplify a type-family application, by *one* step @@ -1378,7 +1381,7 @@ normalise_tc_app tc tys -- res_co :: typeKind(F tys) ~ typeKind(rhs) -- Type families and data families; always Representational role topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type] - -> Maybe (Coercion, Type, Coercion) + -> Maybe (Coercion, Type, MCoercion) topReduceTyFamApp_maybe envs fam_tc arg_tys | isFamilyTyCon fam_tc -- type families and data families , Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys @@ -1391,7 +1394,7 @@ topReduceTyFamApp_maybe envs fam_tc arg_tys normalise_tc_args fam_tc arg_tys normalise_tc_args :: TyCon -> [Type] -- tc tys - -> NormM (Coercion, [Type], CoercionN) + -> NormM (Coercion, [Type], MCoercionN) -- (co, new_tys), where -- co :: tc tys ~ tc new_tys; might not be homogeneous -- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys) @@ -1474,14 +1477,14 @@ normalise_type ty ; role <- getRole ; let nty = mkAppTys nfun nargs nco = mkAppCos fun_co args_cos - nty_casted = nty `mkCastTy` mkSymCo res_co - final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco + nty_casted = nty `mkCastTyMCo` mkSymMCo res_co + final_co = mkCoherenceRightMCo role nty (mkSymMCo res_co) nco ; return (final_co, nty_casted) } } normalise_args :: Kind -- of the function -> [Role] -- roles at which to normalise args -> [Type] -- args - -> NormM ([Coercion], [Type], Coercion) + -> NormM ([Coercion], [Type], MCoercion) -- returns (cos, xis, res_co), where each xi is the normalised -- version of the corresponding type, each co is orig_arg ~ xi, -- and the res_co :: kind(f orig_args) ~ kind(f xis) @@ -1491,7 +1494,7 @@ normalise_args :: Kind -- of the function normalise_args fun_ki roles args = do { normed_args <- zipWithM normalise1 roles args ; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args - ; return (map mkSymCo cos, xis, mkSymCo res_co) } + ; return (map mkSymCo cos, xis, mkSymMCo res_co) } where (ki_binders, inner_ki) = splitPiTys fun_ki fvs = tyCoVarsOfTypes args |