Take account of injectivity when doing fundeps

This fixes Trac #12803. Yikes!

See Note [Care with type functions].

7 files changed, 94 insertions, 33 deletions

diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 7f4d072bfd..d3ba85e6e3 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -991,6 +991,11 @@ mk_sum arity = (tycon, sum_cons)
 
 -- See Note [The equality types story] in TysPrim
 -- (:~~: :: forall k1 k2 (a :: k1) (b :: k2). a -> b -> Constraint)
+--
+-- It's tempting to put functional dependencies on (~~), but it's not
+-- necessary because the functional-dependency coverage check looks
+-- through superclasses, and (~#) is handled in that check.
+
 heqTyCon, coercibleTyCon :: TyCon
 heqClass, coercibleClass :: Class
 heqDataCon, coercibleDataCon :: DataCon
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 09417a7f25..8fe043112f 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -10,7 +10,7 @@ module FamInst (
         newFamInst,
 
         -- * Injectivity
-        makeInjectivityErrors
+        makeInjectivityErrors, injTyVarsOfType, injTyVarsOfTypes
     ) where
 
 import HscTypes
@@ -504,35 +504,39 @@ unusedInjTvsInRHS tycon injList lhs rhs =
       -- set of type variables appearing in the RHS on an injective position.
       -- For all returned variables we assume their associated kind variables
       -- also appear in the RHS.
-      injRhsVars = collectInjVars rhs
-
-      -- Collect all type variables that are either arguments to a type
-      -- constructor or to injective type families.
-      collectInjVars :: Type -> VarSet
-      collectInjVars (TyVarTy v)
-        = unitVarSet v `unionVarSet` collectInjVars (tyVarKind v)
-      collectInjVars (TyConApp tc tys)
-        | isTypeFamilyTyCon tc = collectInjTFVars tys
-                                                 (familyTyConInjectivityInfo tc)
-        | otherwise            = mapUnionVarSet collectInjVars tys
-      collectInjVars (LitTy {})
-        = emptyVarSet
-      collectInjVars (FunTy arg res)
-        = collectInjVars arg `unionVarSet` collectInjVars res
-      collectInjVars (AppTy fun arg)
-        = collectInjVars fun `unionVarSet` collectInjVars arg
-      -- no forall types in the RHS of a type family
-      collectInjVars (ForAllTy {})    =
-          panic "unusedInjTvsInRHS.collectInjVars"
-      collectInjVars (CastTy ty _)   = collectInjVars ty
-      collectInjVars (CoercionTy {}) = emptyVarSet
-
-      collectInjTFVars :: [Type] -> Injectivity -> VarSet
-      collectInjTFVars _ NotInjective
-          = emptyVarSet
-      collectInjTFVars tys (Injective injList)
-          = mapUnionVarSet collectInjVars (filterByList injList tys)
+      injRhsVars = injTyVarsOfType rhs
 
+injTyVarsOfType :: TcTauType -> TcTyVarSet
+-- Collect all type variables that are either arguments to a type
+--   constructor or to /injective/ type families.
+-- Determining the overall type determines thes variables
+--
+-- E.g.   Suppose F is injective in its second arg, but not its first
+--        then injVarOfType (Either a (F [b] (a,c))) = {a,c}
+--        Determining the overall type determines a,c but not b.
+injTyVarsOfType (TyVarTy v)
+  = unitVarSet v `unionVarSet` injTyVarsOfType (tyVarKind v)
+injTyVarsOfType (TyConApp tc tys)
+  | isTypeFamilyTyCon tc
+   = case familyTyConInjectivityInfo tc of
+        NotInjective  -> emptyVarSet
+        Injective inj -> injTyVarsOfTypes (filterByList inj tys)
+  | otherwise
+  = injTyVarsOfTypes tys
+injTyVarsOfType (LitTy {})
+  = emptyVarSet
+injTyVarsOfType (FunTy arg res)
+  = injTyVarsOfType arg `unionVarSet` injTyVarsOfType res
+injTyVarsOfType (AppTy fun arg)
+  = injTyVarsOfType fun `unionVarSet` injTyVarsOfType arg
+-- No forall types in the RHS of a type family
+injTyVarsOfType (CastTy ty _)   = injTyVarsOfType ty
+injTyVarsOfType (CoercionTy {}) = emptyVarSet
+injTyVarsOfType (ForAllTy {})    =
+    panic "unusedInjTvsInRHS.injTyVarsOfType"
+
+injTyVarsOfTypes :: [Type] -> VarSet
+injTyVarsOfTypes tys = mapUnionVarSet injTyVarsOfType tys
 
 -- | Is type headed by a type family application?
 isTFHeaded :: Type -> Bool
diff --git a/compiler/typecheck/FunDeps.hs b/compiler/typecheck/FunDeps.hs
index a42f7b4922..4da6795c00 100644
--- a/compiler/typecheck/FunDeps.hs
+++ b/compiler/typecheck/FunDeps.hs
@@ -25,6 +25,7 @@ import Class
 import Type
 import TcType( transSuperClasses )
 import Unify
+import FamInst( injTyVarsOfTypes )
 import InstEnv
 import VarSet
 import VarEnv
@@ -491,6 +492,36 @@ 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] -> TyCoVarSet -> TyCoVarSet
@@ -507,7 +538,8 @@ oclose preds fixed_tvs
             -- closeOverKinds: see Note [Closing over kinds in coverage]
 
     tv_fds  :: [(TyCoVarSet,TyCoVarSet)]
-    tv_fds  = [ (tyCoVarsOfTypes ls, tyCoVarsOfTypes rs)
+    tv_fds  = [ (tyCoVarsOfTypes ls, injTyVarsOfTypes rs)
+                  -- See Note [Care with type functions]
               | pred <- preds
               , pred' <- pred : transSuperClasses pred
                    -- Look for fundeps in superclasses too
@@ -517,13 +549,14 @@ oclose preds fixed_tvs
     determined pred
        = case classifyPredType pred of
             EqPred NomEq t1 t2 -> [([t1],[t2]), ([t2],[t1])]
+               -- 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
 *                                                                      *
diff --git a/compiler/types/Class.hs b/compiler/types/Class.hs
index 169f91d3ba..82a71f5376 100644
--- a/compiler/types/Class.hs
+++ b/compiler/types/Class.hs
@@ -148,7 +148,7 @@ The SrcSpan is for the entire original declaration.
 -}
 
 mkClass :: Name -> [TyVar]
-        -> [([TyVar], [TyVar])]
+        -> [FunDep TyVar]
         -> [PredType] -> [Id]
         -> [ClassATItem]
         -> [ClassOpItem]
diff --git a/testsuite/tests/typecheck/should_fail/T12803.hs b/testsuite/tests/typecheck/should_fail/T12803.hs
new file mode 100644
index 0000000000..f874a2ed42
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12803.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
+             TypeFamilies, FunctionalDependencies #-}
+
+module T10778 where
+
+type family F a :: *
+class C a b | a -> b
+
+instance C p (F q) => C p [q]
+-- This instance should fail the (liberal) coverage condition
diff --git a/testsuite/tests/typecheck/should_fail/T12803.stderr b/testsuite/tests/typecheck/should_fail/T12803.stderr
new file mode 100644
index 0000000000..cb8c4e6768
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12803.stderr
@@ -0,0 +1,8 @@
+
+T12803.hs:9:10: error:
+    • Illegal instance declaration for ‘C p [q]’
+        The liberal coverage condition fails in class ‘C’
+          for functional dependency: ‘a -> b’
+        Reason: lhs type ‘p’ does not determine rhs type ‘[q]’
+        Un-determined variable: q
+    • In the instance declaration for ‘C p [q]’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 4f2dbc43d5..1f3b8ba3a1 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -430,3 +430,4 @@ test('T12124', normal, compile_fail, [''])
 test('T12589', normal, compile_fail, [''])
 test('T12529', normal, compile_fail, [''])
 test('T12729', normal, compile_fail, [''])
+test('T12803', normal, compile_fail, [''])