Improve consistency checking for associated type-family instances

The "consistency" in this case is beteween the instance head
and the associated type instance head, which is made trickier
by the presence of kind variables that are not explicitly mentioned
in the class head.

See Note [Checking consistent instantiation] in TcInstDcls

This fixes Trac #7282.

2 files changed, 153 insertions, 121 deletions

diff --git a/compiler/typecheck/TcInstDcls.lhs b/compiler/typecheck/TcInstDcls.lhs
index e3e53ce9df..b721a4b93b 100644
--- a/compiler/typecheck/TcInstDcls.lhs
+++ b/compiler/typecheck/TcInstDcls.lhs
@@ -41,6 +41,7 @@ import TcDeriv
 import TcEnv
 import TcHsType
 import TcUnify
+import Unify      ( tcMatchTyX )
 import MkCore     ( nO_METHOD_BINDING_ERROR_ID )
 import CoreSyn    ( DFunArg(..) )
 import Type
@@ -558,6 +559,29 @@ tcClsInstDecl (ClsInstDecl { cid_poly_ty = poly_ty, cid_binds = binds
               inst_info = InstInfo { iSpec  = ispec, iBinds = VanillaInst binds uprags False }
 
         ; return ( [inst_info], tyfam_insts0 ++ concat tyfam_insts1 ++ datafam_insts) }
+
+--------------
+tcAssocTyDecl :: Class                   -- Class of associated type
+              -> VarEnv Type             -- Instantiation of class TyVars
+              -> LTyFamInstDecl Name     
+              -> TcM (FamInst Unbranched)
+tcAssocTyDecl clas mini_env ldecl@(L loc decl)
+  = setSrcSpan loc $
+    tcAddTyFamInstCtxt decl $
+    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (tyFamInstDeclLName decl)
+       ; fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) fam_tc ldecl
+       ; return $ toUnbranchedFamInst fam_inst }
+
+--------------
+tcAssocDataDecl :: Class                 -- ^ Class of associated type
+                -> VarEnv Type           -- ^ Instantiation of class TyVars
+                -> LDataFamInstDecl Name -- ^ RHS
+                -> TcM (FamInst Unbranched)
+tcAssocDataDecl clas mini_env ldecl@(L loc decl)
+  = setSrcSpan loc $
+    tcAddDataFamInstCtxt decl $
+    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (dfid_tycon decl)
+       ; tcDataFamInstDecl (Just (clas, mini_env)) fam_tc ldecl }
 \end{code}
 
 %************************************************************************
@@ -571,29 +595,6 @@ class instance heads, but can contain data constructors and hence they share a
 lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 
-Note [Associated type consistency check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-According to the invariant stated in FamInstEnv, all FamInsts are created
-with *fresh* variables. This is all well and good for matching instances --
-when we don't want a spurious variable collision -- but bad for type checking
-the instance declarations. Consider this example:
-
-  class Cls a where
-    type Typ a
-
-  instance Cls (Maybe b) where
-    type Typ (Maybe b) = Int
-
-When we're checking the class instance, we build the mini_env [a |-> Maybe b].
-Then, we wish to check that the pattern used in the type instance matches.
-If we build the FamInst for the associated type instance before doing this
-check, the check always fails. This is because the FamInst will be built with
-a *fresh* b, which won't be the same as the old, stale b.
-
-Bottom line: we must perform this check before creating the FamInst, even
-though it's a little awkward to do so. (The FamInst packages everything
-nicely, and we have to push around all pieces independently.)
-
 \begin{code}
 tcFamInstDeclCombined :: TopLevelFlag -> Located Name -> TcM TyCon
 tcFamInstDeclCombined top_lvl fam_tc_lname
@@ -627,8 +628,7 @@ tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = grou
        ; co_ax_branches <- tcSynFamInstDecl fam_tc decl
 
          -- (2) check for validity and inaccessibility
-       ; mapM_   check_valid_mk_branch co_ax_branches
-       ; foldlM_ check_inaccessible_branches [] co_ax_branches
+       ; foldlM_ check_valid_branch [] co_ax_branches
 
          -- (3) construct coercion axiom
        ; rep_tc_name <- newFamInstAxiomName loc
@@ -637,25 +637,24 @@ tcTyFamInstDecl mb_clsinfo fam_tc (L loc decl@(TyFamInstDecl { tfid_group = grou
        ; let axiom = mkBranchedCoAxiom rep_tc_name fam_tc co_ax_branches
        ; newFamInst SynFamilyInst group axiom }
     where 
-      check_valid_mk_branch :: CoAxBranch -> TcM ()
-      check_valid_mk_branch (CoAxBranch { cab_tvs = t_tvs, cab_lhs = t_typats
-                                        , cab_rhs = t_rhs, cab_loc = loc })
+      check_valid_branch :: [CoAxBranch]     -- previous
+                         -> CoAxBranch       -- current
+                         -> TcM [CoAxBranch] -- current : previous
+      check_valid_branch prev_branches
+          cur_branch@(CoAxBranch { cab_tvs = t_tvs, cab_lhs = t_typats
+                                 , cab_rhs = t_rhs, cab_loc = loc })
         = setSrcSpan loc $
-          do { -- check the well-formedness of the instance
+          do { -- Check the well-formedness of the instance
                checkValidTyFamInst fam_tc t_tvs t_typats t_rhs
 
-               -- check that type patterns match the class instance head
-             ; tcAssocFamInst mb_clsinfo loc (ptext (sLit "type")) fam_tc t_typats }
+               -- Check that type patterns match the class instance head
+             ; checkConsistentFamInst mb_clsinfo (ptext (sLit "type")) fam_tc t_tvs t_typats
 
+               -- Check whether the branch is dominated by earlier
+               -- ones and hence is inaccessible
+             ; when (t_typats `isDominatedBy` prev_branches) $
+               addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
 
-      check_inaccessible_branches :: [CoAxBranch]     -- previous
-                                  -> CoAxBranch       -- current
-                                  -> TcM [CoAxBranch] -- current : previous
-      check_inaccessible_branches prev_branches
-                                  cur_branch@(CoAxBranch { cab_lhs = tys })
-        = setSrcSpan (coAxBranchSpan cur_branch) $
-          do { when (tys `isDominatedBy` prev_branches) $
-                    addErrTc $ inaccessibleCoAxBranch fam_tc cur_branch
              ; return $ cur_branch : prev_branches }
 
 tcDataFamInstDecl :: Maybe (Class, VarEnv Type)
@@ -667,7 +666,8 @@ tcDataFamInstDecl mb_clsinfo fam_tc
              , dfid_tycon = fam_tc_name
              , dfid_defn = defn@HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                                            , dd_ctxt = ctxt, dd_cons = cons } }))
-  = do { -- Check that the family declaration is for the right kind
+  = setSrcSpan loc $
+    do { -- Check that the family declaration is for the right kind
          checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
        ; checkTc (isAlgTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
@@ -675,18 +675,18 @@ tcDataFamInstDecl mb_clsinfo fam_tc
        ; tcFamTyPats fam_tc pats (kcDataDefn defn) $ 
            \tvs' pats' res_kind -> do
 
-         -- Check that left-hand side contains no type family applications
+       { -- Check that left-hand side contains no type family applications
          -- (vanilla synonyms are fine, though, and we checked for
-         -- foralls earlier)
-       { checkValidFamPats fam_tc tvs' pats'
+         --  foralls earlier)
+         checkValidFamPats fam_tc tvs' pats'
+         -- Check that type patterns match class instance head, if any
+       ; checkConsistentFamInst mb_clsinfo (ppr new_or_data) fam_tc tvs' pats'
          
          -- Result kind must be '*' (otherwise, we have too few patterns)
        ; checkTc (isLiftedTypeKind res_kind) $ tooFewParmsErr (tyConArity fam_tc)
 
        ; stupid_theta <- tcHsContext ctxt
        ; h98_syntax <- dataDeclChecks (tyConName fam_tc) new_or_data stupid_theta cons
-         -- Check that type patterns match class instance head, if any
-       ; tcAssocFamInst mb_clsinfo loc (ppr new_or_data) fam_tc pats'
 
          -- Construct representation tycon
        ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
@@ -719,60 +719,129 @@ tcDataFamInstDecl mb_clsinfo fam_tc
          -- Remember to check validity; no recursion to worry about here
        ; checkValidTyCon rep_tc
        ; return fam_inst } }
+\end{code}
 
 
-----------------
--- See Note [Associated type consistency check]
-tcAssocFamInst :: Maybe (Class
-               ,  VarEnv Type)       -- ^ Class of associated type
-                                     -- and instantiation of class TyVars
-               -> SrcSpan            -- ^ Of the family instance
+Note [Associated type instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We allow this:
+  class C a where
+    type T x a
+  instance C Int where
+    type T (S y) Int = y
+    type T Z     Int = Char
+
+Note that 
+  a) The variable 'x' is not bound by the class decl
+  b) 'x' is instantiated to a non-type-variable in the instance
+  c) There are several type instance decls for T in the instance
+
+All this is fine.  Of course, you can't give any *more* instances
+for (T ty Int) elsewhere, becuase it's an *associated* type.
+
+Note [Checking consistent instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+  class C a b where
+    type T a x b
+
+  instance C [p] Int
+    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
+                                --    type TR p y = (p,y,y)
+
+So we 
+  * Form the mini-envt from the class type variables a,b
+    to the instance decl types [p],Int:   [a->[p], b->Int]
+
+  * Look at the tyvars a,x,b of the type family constructor T
+    (it shares tyvars with the class C)
+
+  * Apply the mini-evnt to them, and check that the result is
+    consistent with the instance types [p] y Int
+
+We do *not* assume (at this point) the the bound variables of 
+the assoicated type instance decl are the same as for the parent
+instance decl. So, for example,
+
+  instance C [p] Int
+    type T [q] y Int = ...
+
+would work equally well. Reason: making the *kind* variables line
+up is much harder. Example (Trac #7282):
+  class Foo (xs :: [k]) where
+     type Bar xs :: *
+
+   instance Foo '[] where
+     type Bar '[] = Int
+Here the instance decl really looks like
+   instance Foo k ('[] k) where
+     type Bar k ('[] k) = Int
+but the k's are not scoped, and hence won't match Uniques.
+
+So instead we just match structure, with tcMatchTyX, and check
+that distinct type variales match 1-1 with distinct type variables.
+
+HOWEVER, we *still* make the instance type variables scope over the
+type instances, to pick up non-obvious kinds.  Eg
+   class Foo (a :: k) where
+      type F a
+   instance Foo (b :: k -> k) where
+      type F b = Int
+Here the instance is kind-indexed and really looks like
+      type F (k->k) (b::k->k) = Int
+But if the 'b' didn't scope, we would make F's instance too
+poly-kinded.
+
+\begin{code}
+checkConsistentFamInst 
+               :: Maybe ( Class
+                        , VarEnv Type )  -- ^ Class of associated type
+                                         -- and instantiation of class TyVars
                -> SDoc               -- ^ "flavor" of the instance
                -> TyCon              -- ^ Family tycon
+               -> [TyVar]            -- ^ Type variables of the family instance
                -> [Type]             -- ^ Type patterns from instance
                -> TcM ()
-tcAssocFamInst Nothing _ _ _ _ = return ()
-tcAssocFamInst (Just (clas, mini_env)) loc flav fam_tc at_tys
-  = setSrcSpan loc $
-    tcAddFamInstCtxt flav (tyConName fam_tc) $
-    do {
-       -- Check that the associated type comes from this class
+-- See Note [Checking consistent instantiation]
+
+checkConsistentFamInst Nothing _ _ _ _ = return ()
+checkConsistentFamInst (Just (clas, mini_env)) flav fam_tc at_tvs at_tys
+  = tcAddFamInstCtxt flav (tyConName fam_tc) $
+    do { -- Check that the associated type indeed comes from this class
          checkTc (Just clas == tyConAssoc_maybe fam_tc)
                  (badATErr (className clas) (tyConName fam_tc))
 
-       -- See Note [Checking consistent instantiation] in TcTyClsDecls
-       ; zipWithM_ check_arg (tyConTyVars fam_tc) at_tys }
+         -- See Note [Checking consistent instantiation] in TcTyClsDecls
+         -- Check right to left, so that we spot type variable
+         -- inconsistencies before (more confusing) kind variables
+       ; discardResult $ foldrM check_arg emptyTvSubst $
+                         tyConTyVars fam_tc `zip` at_tys }
   where
-    check_arg fam_tc_tv at_ty
+    at_tv_set = mkVarSet at_tvs
+
+    check_arg :: (TyVar, Type) -> TvSubst -> TcM TvSubst
+    check_arg (fam_tc_tv, at_ty) subst
       | Just inst_ty <- lookupVarEnv mini_env fam_tc_tv
-      = checkTc (inst_ty `eqType` at_ty) 
-                (wrongATArgErr at_ty inst_ty)
+      = case tcMatchTyX at_tv_set subst at_ty inst_ty of
+           Just subst | all_distinct subst -> return subst
+           _ -> failWithTc $ wrongATArgErr at_ty inst_ty
                 -- No need to instantiate here, becuase the axiom
                 -- uses the same type variables as the assocated class
       | otherwise
-      = return ()   -- Allow non-type-variable instantiation
-                    -- See Note [Associated type instances]
-
-tcAssocTyDecl :: Class                   -- Class of associated type
-              -> VarEnv Type             -- Instantiation of class TyVars
-              -> LTyFamInstDecl Name     
-              -> TcM (FamInst Unbranched)
-tcAssocTyDecl clas mini_env ldecl@(L loc decl)
-  = setSrcSpan loc $
-    tcAddTyFamInstCtxt decl $
-    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (tyFamInstDeclLName decl)
-       ; fam_inst <- tcTyFamInstDecl (Just (clas, mini_env)) fam_tc ldecl
-       ; return $ toUnbranchedFamInst fam_inst }
+      = return subst   -- Allow non-type-variable instantiation
+                       -- See Note [Associated type instances]
 
-tcAssocDataDecl :: Class                 -- ^ Class of associated type
-                -> VarEnv Type           -- ^ Instantiation of class TyVars
-                -> LDataFamInstDecl Name -- ^ RHS
-                -> TcM (FamInst Unbranched)
-tcAssocDataDecl clas mini_env ldecl@(L loc decl)
-  = setSrcSpan loc $
-    tcAddDataFamInstCtxt decl $
-    do { fam_tc <- tcFamInstDeclCombined NotTopLevel (dfid_tycon decl)
-       ; tcDataFamInstDecl (Just (clas, mini_env)) fam_tc ldecl }
+    all_distinct :: TvSubst -> Bool
+    -- True if all the variables mapped the substitution 
+    -- map to *distinct* type *variables*
+    all_distinct subst = go [] at_tvs
+       where
+         go _   []       = True
+         go acc (tv:tvs) = case lookupTyVar subst tv of
+                             Nothing -> go acc tvs
+                             Just ty | Just tv' <- tcGetTyVar_maybe ty
+                                     , tv' `notElem` acc
+                                     -> go (tv' : acc) tvs
+                             _other -> False
 \end{code}
 
 
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 594ce013d9..2553e23fd3 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -965,42 +965,6 @@ type variables (a,b), but also over the implicitly mentioned kind varaibles
 none. The role of the kind signature (a :: Maybe k) is to add a constraint
 that 'a' must have that kind, and to bring 'k' into scope.
 
-Note [Associated type instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We allow this:
-  class C a where
-    type T x a
-  instance C Int where
-    type T (S y) Int = y
-    type T Z     Int = Char
-
-Note that 
-  a) The variable 'x' is not bound by the class decl
-  b) 'x' is instantiated to a non-type-variable in the instance
-  c) There are several type instance decls for T in the instance
-
-All this is fine.  Of course, you can't give any *more* instances
-for (T ty Int) elsewhere, becuase it's an *associated* type.
-
-Note [Checking consistent instantiation]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  class C a b where
-    type T a x b
-
-  instance C [p] Int
-    type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
-                                --    type TR p y = (p,y,y)
-
-So we 
-  * Form the mini-envt from the class type variables a,b
-    to the instance decl types [p],Int:   [a->[p], b->Int]
-
-  * Look at the tyvars a,x,b of the type family constructor T
-    (it shares tyvars with the class C)
-
-  * Apply the mini-evnt to them, and check that the result is
-    consistent with the instance types [p] y Int
-
 
 %************************************************************************
 %*                                                                      *
@@ -1458,7 +1422,6 @@ checkValidClass cls
 	; mapM_ (check_op constrained_class_methods) op_stuff
 
         -- Check the associated type defaults are well-formed and instantiated
-        -- See Note [Checking consistent instantiation]
         ; mapM_ check_at_defs at_stuff	}
   where
     (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls