Fix header locations
[ghc.git] / compiler / typecheck / FunDeps.hs
index 3e07f6b..c8f0b1d 100644 (file)
@@ -19,12 +19,16 @@ module FunDeps (
 
 #include "HsVersions.h"
 
+import GhcPrelude
+
 import Name
 import Var
 import Class
 import Type
-import TcType( immSuperClasses )
+import TcType( transSuperClasses )
+import CoAxiom( TypeEqn )
 import Unify
+import FamInst( injTyVarsOfTypes )
 import InstEnv
 import VarSet
 import VarEnv
@@ -32,11 +36,11 @@ import Outputable
 import ErrUtils( Validity(..), allValid )
 import SrcLoc
 import Util
-import FastString
 
 import Pair             ( Pair(..) )
 import Data.List        ( nubBy )
-import Data.Maybe       ( isJust )
+import Data.Maybe
+import Data.Foldable    ( fold )
 
 {-
 ************************************************************************
@@ -50,7 +54,7 @@ Each functional dependency with one variable in the RHS is responsible
 for generating a single equality. For instance:
      class C a b | a -> b
 The constraints ([Wanted] C Int Bool) and [Wanted] C Int alpha
-will generate the folloing FunDepEqn
+will generate the following FunDepEqn
      FDEqn { fd_qtvs = []
            , fd_eqs  = [Pair Bool alpha]
            , fd_pred1 = C Int Bool
@@ -103,10 +107,10 @@ data FunDepEqn loc
                                  --   to fresh unification vars,
                                  -- Non-empty only for FunDepEqns arising from instance decls
 
-          , fd_eqs  :: [Pair Type]  -- Make these pairs of types equal
-          , fd_pred1 :: PredType    -- The FunDepEqn arose from 
-          , fd_pred2 :: PredType    --  combining these two constraints 
-          , fd_loc :: loc  }
+          , fd_eqs   :: [TypeEqn]  -- Make these pairs of types equal
+          , fd_pred1 :: PredType   -- The FunDepEqn arose from
+          , fd_pred2 :: PredType   --  combining these two constraints
+          , fd_loc   :: loc  }
 
 {-
 Given a bunch of predicates that must hold, such as
@@ -147,7 +151,7 @@ instFD (ls,rs) tvs tys
 
 zipAndComputeFDEqs :: (Type -> Type -> Bool) -- Discard this FDEq if true
                    -> [Type] -> [Type]
-                   -> [Pair Type]
+                   -> [TypeEqn]
 -- Create a list of (Type,Type) pairs from two lists of types,
 -- making sure that the types are not already equal
 zipAndComputeFDEqs discard (ty1:tys1) (ty2:tys2)
@@ -166,7 +170,7 @@ improveFromAnother :: loc
 improveFromAnother loc pred1 pred2
   | Just (cls1, tys1) <- getClassPredTys_maybe pred1
   , Just (cls2, tys2) <- getClassPredTys_maybe pred2
-  , tys1 `lengthAtLeast` 2 && cls1 == cls2
+  , cls1 == cls2
   = [ FDEqn { fd_qtvs = [], fd_eqs = eqs, fd_pred1 = pred1, fd_pred2 = pred2, fd_loc = loc }
     | let (cls_tvs, cls_fds) = classTvsFds cls1
     , fd <- cls_fds
@@ -182,10 +186,13 @@ improveFromAnother _ _ _ = []
 -- Improve a class constraint from instance declarations
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+instance Outputable (FunDepEqn a) where
+  ppr = pprEquation
+
 pprEquation :: FunDepEqn a -> SDoc
 pprEquation (FDEqn { fd_qtvs = qtvs, fd_eqs = pairs })
-  = vcat [ptext (sLit "forall") <+> braces (pprWithCommas ppr qtvs),
-          nest 2 (vcat [ ppr t1 <+> ptext (sLit "~") <+> ppr t2 
+  = vcat [text "forall" <+> braces (pprWithCommas ppr qtvs),
+          nest 2 (vcat [ ppr t1 <+> text "~" <+> ppr t2
                        | Pair t1 t2 <- pairs])]
 
 improveFromInstEnv :: InstEnvs
@@ -194,12 +201,9 @@ improveFromInstEnv :: InstEnvs
                    -> [FunDepEqn loc] -- Needs to be a FunDepEqn because
                                       -- of quantified variables
 -- Post: Equations oriented from the template (matching instance) to the workitem!
-improveFromInstEnv _inst_env _ pred
-  | not (isClassPred pred)
-  = panic "improveFromInstEnv: not a class predicate"
 improveFromInstEnv inst_env mk_loc pred
-  | Just (cls, tys) <- getClassPredTys_maybe pred
-  , tys `lengthAtLeast` 2
+  | Just (cls, tys) <- ASSERT2( isClassPred pred, ppr pred )
+                       getClassPredTys_maybe pred
   , let (cls_tvs, cls_fds) = classTvsFds cls
         instances          = classInstances inst_env cls
         rough_tcs          = roughMatchTcs tys
@@ -210,33 +214,37 @@ improveFromInstEnv inst_env mk_loc pred
                                 -- because there often are none!
     , let trimmed_tcs = trimRoughMatchTcs cls_tvs fd rough_tcs
                 -- Trim the rough_tcs based on the head of the fundep.
-                -- Remember that instanceCantMatch treats both argumnents
+                -- Remember that instanceCantMatch treats both arguments
                 -- symmetrically, so it's ok to trim the rough_tcs,
                 -- rather than trimming each inst_tcs in turn
     , ispec <- instances
-    , (meta_tvs, eqs) <- checkClsFD fd cls_tvs ispec
-                                    emptyVarSet tys trimmed_tcs -- NB: orientation
+    , (meta_tvs, eqs) <- improveClsFD cls_tvs fd ispec
+                                      tys trimmed_tcs -- NB: orientation
     , let p_inst = mkClassPred cls (is_tys ispec)
     ]
 improveFromInstEnv _ _ _ = []
 
 
-checkClsFD :: FunDep TyVar -> [TyVar]             -- One functional dependency from the class
-           -> ClsInst                             -- An instance template
-           -> TyVarSet -> [Type] -> [Maybe Name]  -- Arguments of this (C tys) predicate
-                                                  -- TyVarSet are extra tyvars that can be instantiated
-           -> [([TyVar], [Pair Type])]
+improveClsFD :: [TyVar] -> FunDep TyVar    -- One functional dependency from the class
+             -> ClsInst                    -- An instance template
+             -> [Type] -> [Maybe Name]     -- Arguments of this (C tys) predicate
+             -> [([TyCoVar], [TypeEqn])]   -- Empty or singleton
+
+improveClsFD clas_tvs fd
+             (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
+             tys_actual rough_tcs_actual
 
-checkClsFD fd clas_tvs
-           (ClsInst { is_tvs = qtvs, is_tys = tys_inst, is_tcs = rough_tcs_inst })
-           extra_qtvs tys_actual rough_tcs_actual
+-- Compare instance      {a,b}    C sx sp sy sq
+--         with wanted     [W] C tx tp ty tq
+--         for fundep (x,y -> p,q)  from class  (C x p y q)
+-- If (sx,sy) unifies with (tx,ty), take the subst S
 
--- 'qtvs' are the quantified type variables, the ones which an be instantiated
+-- 'qtvs' are the quantified type variables, the ones which can be instantiated
 -- to make the types match.  For example, given
 --      class C a b | a->b where ...
 --      instance C (Maybe x) (Tree x) where ..
 --
--- and an Inst of form (C (Maybe t1) t2),
+-- and a wanted constraint of form (C (Maybe t1) t2),
 -- then we will call checkClsFD with
 --
 --      is_qtvs = {x}, is_tys = [Maybe x,  Tree x]
@@ -244,26 +252,18 @@ checkClsFD fd clas_tvs
 --
 -- We can instantiate x to t1, and then we want to force
 --      (Tree x) [t1/x]  ~   t2
---
--- This function is also used when matching two Insts (rather than an Inst
--- against an instance decl. In that case, qtvs is empty, and we are doing
--- an equality check
---
--- This function is also used by InstEnv.badFunDeps, which needs to *unify*
--- For the one-sided matching case, the qtvs are just from the template,
--- so we get matching
 
   | instanceCantMatch rough_tcs_inst rough_tcs_actual
   = []          -- Filter out ones that can't possibly match,
 
   | otherwise
-  = ASSERT2( length tys_inst == length tys_actual     &&
-             length tys_inst == length clas_tvs
+  = ASSERT2( equalLength tys_inst tys_actual &&
+             equalLength tys_inst clas_tvs
             , ppr tys_inst <+> ppr tys_actual )
 
-    case tcUnifyTys bind_fn ltys1 ltys2 of
+    case tcMatchTyKis ltys1 ltys2 of
         Nothing  -> []
-        Just subst | isJust (tcUnifyTys bind_fn rtys1' rtys2')
+        Just subst | isJust (tcMatchTyKisX subst rtys1 rtys2)
                         -- Don't include any equations that already hold.
                         -- Reason: then we know if any actual improvement has happened,
                         --         in which case we need to iterate the solver
@@ -290,17 +290,16 @@ checkClsFD fd clas_tvs
                         -- executed.  What we're doing instead is recording the partial
                         -- work of the ls1/ls2 unification leaving a smaller unification problem
                   where
-                    rtys1' = map (substTy subst) rtys1
-                    rtys2' = map (substTy subst) rtys2
+                    rtys1' = map (substTyUnchecked subst) rtys1
 
-                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2'
+                    fdeqs = zipAndComputeFDEqs (\_ _ -> False) rtys1' rtys2
                         -- Don't discard anything!
                         -- We could discard equal types but it's an overkill to call
                         -- eqType again, since we know for sure that /at least one/
                         -- equation in there is useful)
 
-                    meta_tvs = [ setVarType tv (substTy subst (varType tv))
-                               | tv <- qtvs, tv `notElemTvSubst` subst ]
+                    meta_tvs = [ setVarType tv (substTyUnchecked subst (varType tv))
+                               | tv <- qtvs, tv `notElemTCvSubst` subst ]
                         -- meta_tvs are the quantified type variables
                         -- that have not been substituted out
                         --
@@ -318,17 +317,12 @@ checkClsFD fd clas_tvs
                         --              whose kind mentions that kind variable!
                         --          Trac #6015, #6068
   where
-    qtv_set = mkVarSet qtvs
-    bind_fn tv | tv `elemVarSet` qtv_set    = BindMe
-               | tv `elemVarSet` extra_qtvs = BindMe
-               | otherwise                  = Skolem
-
     (ltys1, rtys1) = instFD fd clas_tvs tys_inst
     (ltys2, rtys2) = instFD fd clas_tvs tys_actual
 
 {-
-************************************************************************
-*                                                                      *
+%************************************************************************
+%*                                                                      *
         The Coverage condition for instance declarations
 *                                                                      *
 ************************************************************************
@@ -377,51 +371,113 @@ checkInstCoverage be_liberal clas theta inst_taus
   where
     (tyvars, fds) = classTvsFds clas
     fundep_ok fd
-       | if be_liberal then liberal_ok else conservative_ok
-       = IsValid
-       | otherwise
-       = NotValid msg
+       | and (isEmptyVarSet <$> undetermined_tvs) = IsValid
+       | otherwise                                = NotValid msg
        where
          (ls,rs) = instFD fd tyvars inst_taus
-         ls_tvs = tyVarsOfTypes ls
-         rs_tvs = tyVarsOfTypes rs
-
-         conservative_ok = rs_tvs `subVarSet` closeOverKinds ls_tvs
-         liberal_ok      = rs_tvs `subVarSet` closeOverKinds (oclose theta ls_tvs)
-                           -- closeOverKinds: see Note [Closing over kinds in coverage]
-
-         msg = vcat [ sep [ ptext (sLit "The")
-                            <+> ppWhen be_liberal (ptext (sLit "liberal"))
-                            <+> ptext (sLit "coverage condition fails in class")
+         ls_tvs = tyCoVarsOfTypes ls
+         rs_tvs = splitVisVarsOfTypes rs
+
+         undetermined_tvs | be_liberal = liberal_undet_tvs
+                          | otherwise  = conserv_undet_tvs
+
+         closed_ls_tvs = oclose theta ls_tvs
+         liberal_undet_tvs = (`minusVarSet` closed_ls_tvs) <$> rs_tvs
+         conserv_undet_tvs = (`minusVarSet` ls_tvs)        <$> rs_tvs
+
+         undet_set = fold undetermined_tvs
+
+         msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
+                      -- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
+                      -- , text "theta" <+> ppr theta
+                      -- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
+                      -- , text "rs_tvs" <+> ppr rs_tvs
+                      sep [ text "The"
+                            <+> ppWhen be_liberal (text "liberal")
+                            <+> text "coverage condition fails in class"
                             <+> quotes (ppr clas)
-                          , nest 2 $ ptext (sLit "for functional dependency:")
+                          , nest 2 $ text "for functional dependency:"
                             <+> quotes (pprFunDep fd) ]
-                    , sep [ ptext (sLit "Reason: lhs type")<>plural ls <+> pprQuotedList ls
+                    , sep [ text "Reason: lhs type"<>plural ls <+> pprQuotedList ls
                           , nest 2 $
                             (if isSingleton ls
-                             then ptext (sLit "does not")
-                             else ptext (sLit "do not jointly"))
-                            <+> ptext (sLit "determine rhs type")<>plural rs
+                             then text "does not"
+                             else text "do not jointly")
+                            <+> text "determine rhs type"<>plural rs
                             <+> pprQuotedList rs ]
-                    , ppWhen (not be_liberal && liberal_ok) $
-                      ptext (sLit "Using UndecidableInstances might help") ]
-
-{-
-Note [Closing over kinds in coverage]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+                    , text "Un-determined variable" <> pluralVarSet undet_set <> colon
+                            <+> pprVarSet undet_set (pprWithCommas ppr)
+                    , ppWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
+                      ppSuggestExplicitKinds
+                    , ppWhen (not be_liberal &&
+                              and (isEmptyVarSet <$> liberal_undet_tvs)) $
+                      text "Using UndecidableInstances might help" ]
+
+{- Note [Closing over kinds in coverage]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have a fundep  (a::k) -> b
 Then if 'a' is instantiated to (x y), where x:k2->*, y:k2,
 then fixing x really fixes k2 as well, and so k2 should be added to
 the lhs tyvars in the fundep check.
 
 Example (Trac #8391), using liberal coverage
+      data Foo a = ...  -- Foo :: forall k. k -> *
+      class Bar a b | a -> b
+      instance Bar a (Foo a)
+
+    In the instance decl, (a:k) does fix (Foo k a), but only if we notice
+    that (a:k) fixes k.  Trac #10109 is another example.
+
+Here is a more subtle example, from HList-0.4.0.0 (Trac #10564)
+
+  class HasFieldM (l :: k) r (v :: Maybe *)
+        | l r -> v where ...
+  class HasFieldM1 (b :: Maybe [*]) (l :: k) r v
+        | b l r -> v where ...
+  class HMemberM (e1 :: k) (l :: [k]) (r :: Maybe [k])
+        | e1 l -> r
+
+  data Label :: k -> *
+  type family LabelsOf (a :: [*]) ::  *
+
+  instance (HMemberM (Label {k} (l::k)) (LabelsOf xs) b,
+            HasFieldM1 b l (r xs) v)
+         => HasFieldM l (r xs) v where
+
+Is the instance OK? Does {l,r,xs} determine v?  Well:
+
+  * From the instance constraint HMemberM (Label k l) (LabelsOf xs) b,
+    plus the fundep "| el l -> r" in class HMameberM,
+    we get {l,k,xs} -> b
+
+  * Note the 'k'!! We must call closeOverKinds on the seed set
+    ls_tvs = {l,r,xs}, BEFORE doing oclose, else the {l,k,xs}->b
+    fundep won't fire.  This was the reason for #10564.
 
-    type Foo a = a  -- Foo :: forall k. k -> k
-    class Bar a b | a -> b
-    instance Bar a (Foo a)
+  * So starting from seeds {l,r,xs,k} we do oclose to get
+    first {l,r,xs,k,b}, via the HMemberM constraint, and then
+    {l,r,xs,k,b,v}, via the HasFieldM1 constraint.
 
-In the instance decl, (a:k) does fix (Foo k a), but only if we notice
-that (a:k) fixes k.  Trac #10109 is another example.
+  * And that fixes v.
+
+However, we must closeOverKinds whenever augmenting the seed set
+in oclose!  Consider Trac #10109:
+
+  data Succ a   -- Succ :: forall k. k -> *
+  class Add (a :: k1) (b :: k2) (ab :: k3) | a b -> ab
+  instance (Add a b ab) => Add (Succ {k1} (a :: k1))
+                               b
+                               (Succ {k3} (ab :: k3})
+
+We start with seed set {a:k1,b:k2} and closeOverKinds to {a,k1,b,k2}.
+Now use the fundep to extend to {a,k1,b,k2,ab}.  But we need to
+closeOverKinds *again* now to {a,k1,b,k2,ab,k3}, so that we fix all
+the variables free in (Succ {k3} ab).
+
+Bottom line:
+  * closeOverKinds on initial seeds (done automatically
+    by tyCoVarsOfTypes in checkInstCoverage)
+  * and closeOverKinds whenever extending those seeds (in oclose)
 
 Note [The liberal coverage condition]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -440,38 +496,71 @@ also know `t2` and the other way.
 
 oclose is used (only) when checking the coverage condition for
 an instance declaration
+
+Note [Equality superclasses]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+  class (a ~ [b]) => C a b
+
+Remember from Note [The equality types story] in TysPrim, that
+  * (a ~~ b) is a superclass of (a ~ b)
+  * (a ~# b) is a superclass of (a ~~ b)
+
+So when oclose expands superclasses we'll get a (a ~# [b]) superclass.
+But that's an EqPred not a ClassPred, and we jolly well do want to
+account for the mutual functional dependencies implied by (t1 ~# t2).
+Hence the EqPred handling in oclose.  See Trac #10778.
+
+Note [Care with type functions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (Trac #12803)
+  class C x y | x -> y
+  type family F a b
+  type family G c d = r | r -> d
+
+Now consider
+  oclose (C (F a b) (G c d)) {a,b}
+
+Knowing {a,b} fixes (F a b) regardless of the injectivity of F.
+But knowing (G c d) fixes only {d}, because G is only injective
+in its second parameter.
+
+Hence the tyCoVarsOfTypes/injTyVarsOfTypes dance in tv_fds.
 -}
 
-oclose :: [PredType] -> TyVarSet -> TyVarSet
+oclose :: [PredType] -> TyCoVarSet -> TyCoVarSet
 -- See Note [The liberal coverage condition]
 oclose preds fixed_tvs
   | null tv_fds = fixed_tvs -- Fast escape hatch for common case.
-  | otherwise   = transCloVarSet extend fixed_tvs
+  | otherwise   = fixVarSet extend fixed_tvs
   where
     extend fixed_tvs = foldl add fixed_tvs tv_fds
        where
           add fixed_tvs (ls,rs)
-            | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` rs
+            | ls `subVarSet` fixed_tvs = fixed_tvs `unionVarSet` closeOverKinds rs
             | otherwise                = fixed_tvs
+            -- closeOverKinds: see Note [Closing over kinds in coverage]
 
-    tv_fds  :: [(TyVarSet,TyVarSet)]
-    tv_fds  = [ (tyVarsOfTypes xs, tyVarsOfTypes ys)
-              | (xs, ys) <- concatMap determined preds ]
+    tv_fds  :: [(TyCoVarSet,TyCoVarSet)]
+    tv_fds  = [ (tyCoVarsOfTypes ls, injTyVarsOfTypes rs)
+                  -- See Note [Care with type functions]
+              | pred <- preds
+              , pred' <- pred : transSuperClasses pred
+                   -- Look for fundeps in superclasses too
+              , (ls, rs) <- determined pred' ]
 
     determined :: PredType -> [([Type],[Type])]
     determined pred
        = case classifyPredType pred of
             EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
-            ClassPred cls tys -> local_fds ++ concatMap determined superclasses
-              where
-               local_fds = [ instFD fd cls_tvs tys
-                           | fd <- cls_fds ]
-               (cls_tvs, cls_fds) = classTvsFds cls
-               superclasses = immSuperClasses cls tys
+               -- See Note [Equality superclasses]
+            ClassPred cls tys  -> [ instFD fd cls_tvs tys
+                                  | let (cls_tvs, cls_fds) = classTvsFds cls
+                                  , fd <- cls_fds ]
             _ -> []
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
         Check that a new instance decl is OK wrt fundeps
 *                                                                      *
@@ -501,37 +590,62 @@ The instance decls don't overlap, because the third parameter keeps
 them separate.  But we want to make sure that given any constraint
         D s1 s2 s3
 if s1 matches
+
+Note [Bogus consistency check]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In checkFunDeps we check that a new ClsInst is consistent with all the
+ClsInsts in the environment.
+
+The bogus aspect is discussed in Trac #10675. Currenty it if the two
+types are *contradicatory*, using (isNothing . tcUnifyTys).  But all
+the papers say we should check if the two types are *equal* thus
+   not (substTys subst rtys1 `eqTypes` substTys subst rtys2)
+For now I'm leaving the bogus form because that's the way it has
+been for years.
 -}
 
-checkFunDeps :: InstEnvs -> ClsInst
-             -> Maybe [ClsInst] -- Nothing  <=> ok
-                                -- Just dfs <=> conflict with dfs
+checkFunDeps :: InstEnvs -> ClsInst -> [ClsInst]
+-- The Consistency Check.
 -- Check whether adding DFunId would break functional-dependency constraints
 -- Used only for instance decls defined in the module being compiled
-checkFunDeps inst_envs ispec
-  | null bad_fundeps = Nothing
-  | otherwise        = Just bad_fundeps
-  where
-    (ins_tvs, clas, ins_tys) = instanceHead ispec
-    ins_tv_set   = mkVarSet ins_tvs
-    cls_inst_env = classInstances inst_envs clas
-    bad_fundeps  = badFunDeps cls_inst_env clas ins_tv_set ins_tys
-
-badFunDeps :: [ClsInst] -> Class
-           -> TyVarSet -> [Type]        -- Proposed new instance type
-           -> [ClsInst]
-badFunDeps cls_insts clas ins_tv_set ins_tys
+-- Returns a list of the ClsInst in InstEnvs that are inconsistent
+-- with the proposed new ClsInst
+checkFunDeps inst_envs (ClsInst { is_tvs = qtvs1, is_cls = cls
+                                , is_tys = tys1, is_tcs = rough_tcs1 })
+  | null fds
+  = []
+  | otherwise
   = nubBy eq_inst $
-    [ ispec | fd <- fds,        -- fds is often empty, so do this first!
-              let trimmed_tcs = trimRoughMatchTcs clas_tvs fd rough_tcs,
-              ispec <- cls_insts,
-              notNull (checkClsFD fd clas_tvs ispec ins_tv_set ins_tys trimmed_tcs)
-    ]
+    [ ispec | ispec <- cls_insts
+            , fd    <- fds
+            , is_inconsistent fd ispec ]
   where
-    (clas_tvs, fds) = classTvsFds clas
-    rough_tcs = roughMatchTcs ins_tys
+    cls_insts      = classInstances inst_envs cls
+    (cls_tvs, fds) = classTvsFds cls
+    qtv_set1       = mkVarSet qtvs1
+
+    is_inconsistent fd (ClsInst { is_tvs = qtvs2, is_tys = tys2, is_tcs = rough_tcs2 })
+      | instanceCantMatch trimmed_tcs rough_tcs2
+      = False
+      | otherwise
+      = case tcUnifyTyKis bind_fn ltys1 ltys2 of
+          Nothing         -> False
+          Just subst
+            -> isNothing $   -- Bogus legacy test (Trac #10675)
+                             -- See Note [Bogus consistency check]
+               tcUnifyTyKis bind_fn (substTysUnchecked subst rtys1) (substTysUnchecked subst rtys2)
+
+      where
+        trimmed_tcs    = trimRoughMatchTcs cls_tvs fd rough_tcs1
+        (ltys1, rtys1) = instFD fd cls_tvs tys1
+        (ltys2, rtys2) = instFD fd cls_tvs tys2
+        qtv_set2       = mkVarSet qtvs2
+        bind_fn tv | tv `elemVarSet` qtv_set1 = BindMe
+                   | tv `elemVarSet` qtv_set2 = BindMe
+                   | otherwise                = Skolem
+
     eq_inst i1 i2 = instanceDFunId i1 == instanceDFunId i2
-        -- An single instance may appear twice in the un-nubbed conflict list
+        -- A single instance may appear twice in the un-nubbed conflict list
         -- because it may conflict with more than one fundep.  E.g.
         --      class C a b c | a -> b, a -> c
         --      instance C Int Bool Bool
@@ -545,6 +659,8 @@ trimRoughMatchTcs :: [TyVar] -> FunDep TyVar -> [Maybe Name] -> [Maybe Name]
 -- we want to match only on the type ta; so our
 -- rough-match thing must similarly be filtered.
 -- Hence, we Nothing-ise the tb and tc types right here
+--
+-- Result list is same length as input list, just with more Nothings
 trimRoughMatchTcs clas_tvs (ltvs, _) mb_tcs
   = zipWith select clas_tvs mb_tcs
   where