diff options
| -rw-r--r-- | compiler/GHC/Core/Coercion/Opt.hs | 56 | ||||
| -rw-r--r-- | compiler/GHC/Core/Lint.hs | 65 |
2 files changed, 64 insertions, 57 deletions
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs index a77de66405..98506c444e 100644 --- a/compiler/GHC/Core/Coercion/Opt.hs +++ b/compiler/GHC/Core/Coercion/Opt.hs @@ -4,7 +4,6 @@ module GHC.Core.Coercion.Opt ( optCoercion - , checkAxInstCo , OptCoercionOpts (..) ) where @@ -991,28 +990,6 @@ of any examples, but if any come to light we may need to reconsider this behaviour. -Note [Conflict checking with AxiomInstCo] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider the following type family and axiom: - -type family Equal (a :: k) (b :: k) :: Bool -type instance where - Equal a a = True - Equal a b = False --- -Equal :: forall k::*. k -> k -> Bool -axEqual :: { forall k::*. forall a::k. Equal k a a ~ True - ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False } - -We wish to disallow (axEqual[1] <*> <Int> <Int). (Recall that the index is -0-based, so this is the second branch of the axiom.) The problem is that, on -the surface, it seems that (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ -False) and that all is OK. But, all is not OK: we want to use the first branch -of the axiom in this case, not the second. The problem is that the parameters -of the first branch can unify with the supplied coercions, thus meaning that -the first branch should be taken. See also Note [Apartness] in -"GHC.Core.FamInstEnv". - Note [Why call checkAxInstCo during optimisation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ NB: The following is no longer relevant, because we no longer push transitivity @@ -1109,39 +1086,6 @@ The problem described here was first found in dependent/should_compile/dynamic-p -} --- | Check to make sure that an AxInstCo is internally consistent. --- Returns the conflicting branch, if it exists --- See Note [Conflict checking with AxiomInstCo] -checkAxInstCo :: Coercion -> Maybe CoAxBranch --- defined here to avoid dependencies in GHC.Core.Coercion --- If you edit this function, you may need to update the GHC formalism --- See Note [GHC Formalism] in GHC.Core.Lint -checkAxInstCo (AxiomInstCo ax ind cos) - = let branch = coAxiomNthBranch ax ind - tvs = coAxBranchTyVars branch - cvs = coAxBranchCoVars branch - incomps = coAxBranchIncomps branch - (tys, cotys) = splitAtList tvs (map coercionLKind cos) - co_args = map stripCoercionTy cotys - subst = zipTvSubst tvs tys `composeTCvSubst` - zipCvSubst cvs co_args - target = Type.substTys subst (coAxBranchLHS branch) - in_scope = mkInScopeSet $ - unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps) - flattened_target = flattenTys in_scope target in - check_no_conflict flattened_target incomps - where - check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch - check_no_conflict _ [] = Nothing - check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest) - -- See Note [Apartness] in GHC.Core.FamInstEnv - | SurelyApart <- tcUnifyTysFG alwaysBindFun flat lhs_incomp - = check_no_conflict flat rest - | otherwise - = Just b -checkAxInstCo _ = Nothing - - ----------- wrapSym :: SymFlag -> Coercion -> Coercion wrapSym sym co | sym = mkSymCo co diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index 483d7168f7..7bb1eb43aa 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -56,7 +56,6 @@ import GHC.Core.TyCon as TyCon import GHC.Core.Coercion.Axiom import GHC.Core.FamInstEnv( compatibleBranches ) import GHC.Core.Unify -import GHC.Core.Coercion.Opt ( checkAxInstCo ) import GHC.Core.Opt.Arity ( typeArity, exprIsDeadEnd ) import GHC.Core.Opt.Monad @@ -2531,6 +2530,70 @@ lintCoercion (HoleCo h) = do { addErrL $ text "Unfilled coercion hole:" <+> ppr h ; lintCoercion (CoVarCo (coHoleCoVar h)) } + +{- +Note [Conflict checking with AxiomInstCo] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider the following type family and axiom: + +type family Equal (a :: k) (b :: k) :: Bool +type instance where + Equal a a = True + Equal a b = False +-- +Equal :: forall k::*. k -> k -> Bool +axEqual :: { forall k::*. forall a::k. Equal k a a ~ True + ; forall k::*. forall a::k. forall b::k. Equal k a b ~ False } + +The coercion (axEqual[1] <*> <Int> <Int) is ill-typed, and Lint should reject it. +(Recall that the index is 0-based, so this is the second branch of the axiom.) +The problem is that, on the surface, it seems that + + (axEqual[1] <*> <Int> <Int>) :: (Equal * Int Int ~ False) + +and that all is OK. But, all is not OK: we want to use the first branch of the +axiom in this case, not the second. The problem is that the parameters of the +first branch can unify with the supplied coercions, thus meaning that the first +branch should be taken. See also Note [Apartness] in "GHC.Core.FamInstEnv". + +For more details, see the section "Branched axiom conflict checking" in +docs/core-spec, which defines the corresponding no_conflict function used by the +Co_AxiomInstCo rule in the section "Coercion typing". +-} + +-- | Check to make sure that an AxInstCo is internally consistent. +-- Returns the conflicting branch, if it exists +-- See Note [Conflict checking with AxiomInstCo] +checkAxInstCo :: Coercion -> Maybe CoAxBranch +-- defined here to avoid dependencies in GHC.Core.Coercion +-- If you edit this function, you may need to update the GHC formalism +-- See Note [GHC Formalism] in GHC.Core.Lint +checkAxInstCo (AxiomInstCo ax ind cos) + = let branch = coAxiomNthBranch ax ind + tvs = coAxBranchTyVars branch + cvs = coAxBranchCoVars branch + incomps = coAxBranchIncomps branch + (tys, cotys) = splitAtList tvs (map coercionLKind cos) + co_args = map stripCoercionTy cotys + subst = zipTvSubst tvs tys `composeTCvSubst` + zipCvSubst cvs co_args + target = Type.substTys subst (coAxBranchLHS branch) + in_scope = mkInScopeSet $ + unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps) + flattened_target = flattenTys in_scope target in + check_no_conflict flattened_target incomps + where + check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch + check_no_conflict _ [] = Nothing + check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest) + -- See Note [Apartness] in GHC.Core.FamInstEnv + | SurelyApart <- tcUnifyTysFG alwaysBindFun flat lhs_incomp + = check_no_conflict flat rest + | otherwise + = Just b +checkAxInstCo _ = Nothing + + {- ************************************************************************ * * |