Fix Trac #7585.

The coercion optimizer was optimizing coercions inside of branched
axiom applications, sometimes invalidating the branch choice within
the axiom application. Now, we check to make sure we are not
invalidating this invariant before proceeding with the optimization.

1 files changed, 2 insertions, 39 deletions

diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs
index cd041a5d15..cc25ece652 100644
--- a/compiler/coreSyn/CoreLint.lhs
+++ b/compiler/coreSyn/CoreLint.lhs
@@ -51,8 +51,7 @@ import PrelNames
 import Outputable
 import FastString
 import Util
-import Unify
-import InstEnv ( instanceBindFun )
+import OptCoercion ( checkAxInstCo )
 import Control.Monad
 import MonadUtils
 import Data.Maybe
@@ -413,31 +412,6 @@ kind coercions and produce the following substitution which is to be
 applied in the type variables:
   k_ag   ~~>   * -> *
 
-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::BOX. k -> k -> Bool
-axEqual :: { forall k::BOX. forall a::k. Equal k a a ~ True
-           ; forall k::BOX. 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 [Instance checking within groups] in types/FamInstEnv.lhs.
-
-However, if the right-hand side of the previous branch coincides with the right-hand
-side of the selected branch, we wish to accept the AxiomInstCo. See also Note
-[Confluence checking within groups], also in types/FamInstEnv.lhs.
-
 %************************************************************************
 %*									*
 \subsection[lintCoreArgs]{lintCoreArgs}
@@ -951,7 +925,7 @@ lintCoercion co@(AxiomInstCo con ind cos)
                                       (ktvs `zip` cos)
        ; let lhs' = Type.substTys subst_l lhs
              rhs' = Type.substTy subst_r rhs
-       ; case check_no_conflict lhs' (ind - 1) of
+       ; case checkAxInstCo co of
            Just bad_index -> bad_ax $ ptext (sLit "inconsistent with") <+> (ppr bad_index)
            Nothing -> return ()
        ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs') }
@@ -959,17 +933,6 @@ lintCoercion co@(AxiomInstCo con ind cos)
     bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
                         2 (ppr co))
 
-      -- See Note [Conflict checking with AxiomInstCo]
-    check_no_conflict :: [Type] -> Int -> Maybe Int
-    check_no_conflict _ (-1) = Nothing
-    check_no_conflict lhs' j
-      | SurelyApart <- tcApartTys instanceBindFun lhs' lhsj
-      = check_no_conflict lhs' (j-1)
-      | otherwise
-      = Just j
-      where
-        (CoAxBranch { cab_lhs = lhsj }) = coAxiomNthBranch con j
-
     check_ki (subst_l, subst_r) (ktv, co)
       = do { (k, t1, t2) <- lintCoercion co
            ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)