summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/GHC/Core/Coercion/Opt.hs56
-rw-r--r--compiler/GHC/Core/Lint.hs65
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
+
+
{-
************************************************************************
* *