Better validity checks, simplification

5 files changed, 285 insertions, 289 deletions

diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs
index 7c632c8d80..16a4e1279d 100644
--- a/compiler/typecheck/TcGenDeriv.hs
+++ b/compiler/typecheck/TcGenDeriv.hs
@@ -1871,8 +1871,7 @@ gen_Newtype_binds loc cls inst_tvs inst_tys rhs_ty
         let axiom = mkSingleCoAxiom Nominal rep_tc_name rep_tvs' rep_cvs'
                                     fam_tc rep_lhs_tys rep_rhs_ty
         -- Check (c) from Note [GND and associated type families] in TcDeriv
-        checkValidCoAxBranch (Just (cls, cls_tvs, lhs_env)) fam_tc
-                             (coAxiomSingleBranch axiom)
+        checkValidCoAxBranch fam_tc (coAxiomSingleBranch axiom)
         newFamInst SynFamilyInst axiom
       where
         cls_tvs     = classTyVars cls
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 5272fd46c8..6261b6a440 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -47,7 +47,7 @@ module TcHsType (
         typeLevelMode, kindLevelMode,
 
         kindGeneralize, checkExpectedKindX,
-        instantiateTyN, instantiateTyUntilN,
+        instantiateTyN, 
         reportFloatingKvs,
 
         -- Sort-checking kinds
@@ -875,7 +875,7 @@ tcInferApps :: TcTyMode
             -> TcType               -- ^ Function
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
-            -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
+            -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
 -- Precondition: typeKind fun_ty = fun_ki
 --    Reason: we will return a type application like (fun_ty arg1 ... argn),
 --            and that type must be well-kinded
@@ -883,39 +883,37 @@ tcInferApps :: TcTyMode
 -- Postcondition: Result kind is zonked.
 tcInferApps mode orig_hs_ty fun_ty fun_ki orig_hs_args
   = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr fun_ki)
-       ; (f_args, args, res_k) <- go 1 [] empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
+       ; (f_args, res_k) <- go 1 empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
        ; traceTc "tcInferApps }" empty
-       ; res_k <- zonkTcType res_k  -- nec'y to uphold (IT4) of Note [The tcType invariant]
-       ; return (f_args, args, res_k) }
+       ; res_k <- zonkTcType res_k  -- Uphold (IT4) of Note [The tcType invariant]
+       ; return (f_args, res_k) }
   where
     empty_subst                      = mkEmptyTCvSubst $ mkInScopeSet $
                                        tyCoVarsOfType fun_ki
     (orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
 
     go :: Int             -- the # of the next argument
-       -> [TcType]        -- already type-checked args, in reverse order
        -> TCvSubst        -- instantiating substitution
        -> TcType          -- function applied to some args
        -> [TyBinder]      -- binders in function kind (both vis. and invis.)
        -> TcKind          -- function kind body (not a Pi-type)
        -> [LHsType GhcRn] -- un-type-checked args
-       -> TcM (TcType, [TcType], TcKind)  -- same as overall return type
+       -> TcM (TcType, TcKind)  -- same as overall return type
 
       -- no user-written args left. We're done!
-    go _ acc_args subst fun ki_binders inner_ki []
+    go _ subst fun ki_binders inner_ki []
       = return ( fun
-               , reverse acc_args
                , nakedSubstTy subst $ mkPiTys ki_binders inner_ki)
                  -- nakedSubstTy: see Note [The well-kinded type invariant]
 
       -- The function's kind has a binder. Is it visible or invisible?
-    go n acc_args subst fun (ki_binder:ki_binders) inner_ki
+    go n subst fun (ki_binder:ki_binders) inner_ki
        all_args@(arg:args)
       | isInvisibleBinder ki_binder
         -- It's invisible. Instantiate.
       = do { traceTc "tcInferApps (invis)" (ppr ki_binder $$ ppr subst)
            ; (subst', arg') <- tcInstTyBinder Nothing subst ki_binder
-           ; go n (arg' : acc_args) subst' (mkNakedAppTy fun arg')
+           ; go n subst' (mkNakedAppTy fun arg')
                 ki_binders inner_ki all_args }
 
       | otherwise
@@ -929,15 +927,15 @@ tcInferApps mode orig_hs_ty fun_ty fun_ki orig_hs_args
                      tc_lhs_type mode arg exp_kind
            ; traceTc "tcInferApps (vis 1)" (ppr exp_kind)
            ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
-           ; go (n+1) (arg' : acc_args) subst'
+           ; go (n+1) subst'
                 (mkNakedAppTy fun arg') -- See Note [The well-kinded type invariant]
                 ki_binders inner_ki args }
 
        -- We've run out of known binders in the functions's kind.
-    go n acc_args subst fun [] inner_ki all_args
+    go n subst fun [] inner_ki all_args
       | not (null new_ki_binders)
          -- But, after substituting, we have more binders.
-      = go n acc_args zapped_subst fun new_ki_binders new_inner_ki all_args
+      = go n zapped_subst fun new_ki_binders new_inner_ki all_args
 
       | otherwise
          -- Even after substituting, still no binders. Use matchExpectedFunKind
@@ -945,7 +943,7 @@ tcInferApps mode orig_hs_ty fun_ty fun_ki orig_hs_args
            ; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_inner_ki
            ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
                  subst'       = zapped_subst `extendTCvInScopeSet` new_in_scope
-           ; go n acc_args subst'
+           ; go n subst'
                 (fun `mkNakedCastTy` co)  -- See Note [The well-kinded type invariant]
                 [mkAnonBinder arg_k]
                 res_k all_args }
@@ -968,7 +966,7 @@ tcTyApps :: TcTyMode
          -> TcM (TcType, TcKind) -- ^ (f args, result kind)   result kind is zonked
 -- Precondition: see precondition for tcInferApps
 tcTyApps mode orig_hs_ty fun_ty fun_ki args
-  = do { (ty', _args, ki') <- tcInferApps mode orig_hs_ty fun_ty fun_ki args
+  = do { (ty', ki') <- tcInferApps mode orig_hs_ty fun_ty fun_ki args
        ; return (ty' `mkNakedCastTy` mkNomReflCo ki', ki') }
           -- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]
 
@@ -981,22 +979,20 @@ checkExpectedKind :: HasDebugCallStack
                   -> TcKind         -- the known kind of that type
                   -> TcKind         -- the expected kind
                   -> TcM TcType
-checkExpectedKind hs_ty ty act exp
-  = fstOf3 <$> checkExpectedKindX Nothing (ppr hs_ty) ty act exp
+checkExpectedKind hs_ty ty act exp = checkExpectedKindX (ppr hs_ty) ty act exp
 
 checkExpectedKindX :: HasDebugCallStack
-                   => Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
-                   -> SDoc                 -- HsType whose kind we're checking
+                   => SDoc                 -- HsType whose kind we're checking
                    -> TcType               -- the type whose kind we're checking
                    -> TcKind               -- the known kind of that type, k
                    -> TcKind               -- the expected kind, exp_kind
-                   -> TcM (TcType, [TcType], TcCoercionN)
+                   -> TcM TcType
     -- (the new args, the coercion)
 -- Instantiate a kind (if necessary) and then call unifyType
 --      (checkExpectedKind ty act_kind exp_kind)
 -- checks that the actual kind act_kind is compatible
 --      with the expected kind exp_kind
-checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
+checkExpectedKindX pp_hs_ty ty act_kind exp_kind
  = do { -- We need to make sure that both kinds have the same number of implicit
         -- foralls out front. If the actual kind has more, instantiate accordingly.
         -- Otherwise, just pass the type & kind through: the errors are caught
@@ -1004,7 +1000,7 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
         let (exp_bndrs, _)            = splitPiTysInvisible exp_kind
             (act_bndrs, act_inner_ki) = splitPiTysInvisible act_kind
             n_to_inst                 = length act_bndrs - length exp_bndrs
-      ; (new_args, act_kind') <- instantiateTyN mb_kind_env n_to_inst act_bndrs act_inner_ki
+      ; (new_args, act_kind') <- instantiateTyN n_to_inst act_bndrs act_inner_ki
 
       ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                   , uo_expected = exp_kind
@@ -1019,33 +1015,31 @@ checkExpectedKindX mb_kind_env pp_hs_ty ty act_kind exp_kind
              , text "exp_kind:" <+> ppr exp_kind ]
 
       ; if act_kind' `tcEqType` exp_kind
-        then return (ty', new_args, mkTcNomReflCo exp_kind)  -- This is very common
+        then return ty'   -- This is very common
         else do { co_k <- uType KindLevel origin act_kind' exp_kind
                 ; traceTc "checkExpectedKind" (vcat [ ppr act_kind
                                                     , ppr exp_kind
                                                     , ppr co_k ])
                 ; let result_ty = ty' `mkNakedCastTy` co_k
                       -- See Note [The tcType invariant]
-                ; return (result_ty, new_args, co_k) } }
+                ; return result_ty } }
 
 -- | Instantiate @n@ invisible arguments to a type. If @n <= 0@, no instantiation
 -- occurs. If @n@ is too big, then all available invisible arguments are instantiated.
 -- (In other words, this function is very forgiving about bad values of @n@.)
 -- Why zonk the result? So that tcTyVar can obey (IT6) of Note [The tcType invariant]
 instantiateTyN :: HasDebugCallStack
-               => Maybe (VarEnv Kind)              -- ^ Predetermined instantiations
-                                                   -- (for assoc. type patterns)
-               -> Int                              -- ^ @n@
+               => Int                              -- ^ @n@
                -> [TyBinder] -> TcKind             -- ^ its kind (zonked)
                -> TcM ([TcType], TcKind)   -- ^ The inst'ed type, new args, kind (zonked)
-instantiateTyN mb_kind_env n bndrs inner_ki
+instantiateTyN n bndrs inner_ki
   | n <= 0            -- It's fine for it to be < 0.  E.g.
   = return ([], ki)   -- Check that (Maybe :: forall {k}. k->*),
                       --       and see the call to instantiateTyN in checkExpectedKind
                       -- A user bug to be reported as such; it is not a compiler crash!
 
   | otherwise
-  = do { (subst, inst_args) <- tcInstTyBinders empty_subst mb_kind_env inst_bndrs
+  = do { (subst, inst_args) <- tcInstTyBinders empty_subst Nothing inst_bndrs
        ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
        ; ki' <- zonkTcType (substTy subst rebuilt_ki)
        ; traceTc "instantiateTyN" (vcat [ ppr ki
@@ -1060,16 +1054,6 @@ instantiateTyN mb_kind_env n bndrs inner_ki
      ki          = mkPiTys bndrs inner_ki
      empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
 
--- | Instantiate a type to have at most @n@ invisible arguments.
-instantiateTyUntilN :: Maybe (VarEnv Kind)   -- ^ Possibly, instantiations for vars
-                    -> Int         -- ^ @n@
-                    -> TcKind      -- ^ its kind
-                    -> TcM ([TcType], TcKind)   -- ^ The new args, final kind
-instantiateTyUntilN mb_kind_env n ki
-  = let (bndrs, inner_ki) = splitPiTysInvisible ki
-        num_to_inst       = length bndrs - n
-    in
-    instantiateTyN mb_kind_env num_to_inst bndrs inner_ki
 
 ---------------------------
 tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
@@ -1159,7 +1143,7 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
       | otherwise
       = do { tc_kind <- zonkTcType (tyConKind tc)
            ; let (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
-           ; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc))
+           ; (tc_args, kind) <- instantiateTyN (length (tyConBinders tc))
                                                tc_kind_bndrs tc_inner_ki
            ; let is_saturated = tc_args `lengthAtLeast` tyConArity tc
                  tc_ty
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index b498c07c34..914114f508 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -547,20 +547,23 @@ lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 -}
 
-tcFamInstDeclCombined :: Maybe ClsInstInfo
+tcFamInstDeclChecks :: Maybe ClsInstInfo
                       -> Located Name -> TcM TyCon
-tcFamInstDeclCombined mb_clsinfo fam_tc_lname
+tcFamInstDeclChecks mb_clsinfo fam_tc_lname
   = do { -- Type family instances require -XTypeFamilies
          -- and can't (currently) be in an hs-boot file
        ; traceTc "tcFamInstDecl" (ppr fam_tc_lname)
        ; type_families <- xoptM LangExt.TypeFamilies
-       ; is_boot <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
+       ; is_boot       <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
        ; checkTc type_families $ badFamInstDecl fam_tc_lname
        ; checkTc (not is_boot) $ badBootFamInstDeclErr
 
        -- Look up the family TyCon and check for validity including
        -- check that toplevel type instances are not for associated types.
        ; fam_tc <- tcLookupLocatedTyCon fam_tc_lname
+
+       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
+
        ; when (isNothing mb_clsinfo &&   -- Not in a class decl
                isTyConAssoc fam_tc)      -- but an associated type
               (addErr $ assocInClassErr fam_tc_lname)
@@ -570,14 +573,14 @@ tcFamInstDeclCombined mb_clsinfo fam_tc_lname
 tcTyFamInstDecl :: Maybe ClsInstInfo
                 -> LTyFamInstDecl GhcRn -> TcM FamInst
   -- "type instance"
+  -- See Note [Associated type instances]
 tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
   = setSrcSpan loc           $
     tcAddTyFamInstCtxt decl  $
     do { let fam_lname = feqn_tycon (hsib_body eqn)
-       ; fam_tc <- tcFamInstDeclCombined mb_clsinfo fam_lname
+       ; fam_tc <- tcFamInstDeclChecks mb_clsinfo fam_lname
 
          -- (0) Check it's an open type family
-       ; checkTc (isFamilyTyCon fam_tc)         (notFamily fam_tc)
        ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
        ; checkTc (isOpenTypeFamilyTyCon fam_tc) (notOpenFamily fam_tc)
 
@@ -586,7 +589,7 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
                                         (L (getLoc fam_lname) eqn)
 
          -- (2) check for validity
-       ; checkValidCoAxBranch mb_clsinfo fam_tc co_ax_branch
+       ; checkValidCoAxBranch fam_tc co_ax_branch
 
          -- (3) construct coercion axiom
        ; rep_tc_name <- newFamInstAxiomName fam_lname [coAxBranchLHS co_ax_branch]
@@ -611,10 +614,9 @@ tcDataFamInstDecl mb_clsinfo
                                         , dd_derivs = derivs } }}}))
   = setSrcSpan loc             $
     tcAddDataFamInstCtxt decl  $
-    do { fam_tc <- tcFamInstDeclCombined mb_clsinfo lfam_name
+    do { fam_tc <- tcFamInstDeclChecks mb_clsinfo lfam_name
 
        -- Check that the family declaration is for the right kind
-       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
        ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
        ; gadt_syntax <- dataDeclChecks fam_name new_or_data ctxt cons
           -- Do /not/ check that the number of patterns = tyConArity fam_tc
@@ -636,7 +638,7 @@ tcDataFamInstDecl mb_clsinfo
                      ; exp_res_kind <- case m_ksig of
                           Nothing   -> return liftedTypeKind
                           Just hs_k -> tcLHsKindSig data_ctxt hs_k
-                     ; _ <- checkExpectedKindX Nothing pp_hs_pats bogus_ty
+                     ; _ <- checkExpectedKindX pp_hs_pats bogus_ty
                                                res_kind exp_res_kind
                             -- ToDo: what about a non-triv result?
 
@@ -676,6 +678,9 @@ tcDataFamInstDecl mb_clsinfo
              orig_res_ty = mkTyConApp fam_tc all_pats
              ty_binders  = full_tcbs `chkAppend` extra_tcbs
 
+       -- Check that type patterns match the class instance head
+       ; checkConsistentFamInst mb_clsinfo fam_tc all_pats
+
        ; traceTc "tcDataFamInstDecl" (ppr fam_tc $$ ppr pats $$ ppr imp_vars $$ ppr exp_bndrs
                                       $$ ppr cons)
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
@@ -713,7 +718,7 @@ tcDataFamInstDecl mb_clsinfo
        -- Remember to check validity; no recursion to worry about here
        -- Check that left-hand sides are ok (mono-types, no type families,
        -- consistent instantiations, etc)
-       ; checkValidCoAxBranch mb_clsinfo fam_tc (coAxiomSingleBranch axiom)
+       ; checkValidCoAxBranch fam_tc (coAxiomSingleBranch axiom)
 
        -- Result kind must be '*' (otherwise, we have too few patterns)
        ; checkTc (tcIsLiftedTypeKind final_res_kind) $
@@ -761,6 +766,24 @@ tcDataFamInstDecl _ (L _ (DataFamInstDecl (HsIB _ (XFamEqn _))))
   = panic "tcDataFamInstDecl"
 
 
+{- 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, because it's an *associated* type.
+-}
+
 {- *********************************************************************
 *                                                                      *
       Type-checking instance declarations, pass 2
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index bea2882669..c7b1ede246 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -18,7 +18,8 @@ module TcTyClsDecls (
         kcConDecl, tcConDecls, dataDeclChecks, checkValidTyCon,
         tcFamTyPats, tcTyFamInstEqn,
         tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
-        wrongKindOfFamily, dataConCtxt
+        wrongKindOfFamily,
+        ClsInstInfo, checkConsistentFamInst
     ) where
 
 #include "HsVersions.h"
@@ -1823,7 +1824,7 @@ tcFamTyPatsAndGen :: TyCon -> Maybe ClsInstInfo
                   -> HsTyPats GhcRn                  -- Patterns
                   -> LHsType GhcRn                   -- RHS type
                   -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
-tcFamTyPatsAndGen fam_tc mb_cls_info imp_vars exp_bndrs hs_pats rhs_hs_ty
+tcFamTyPatsAndGen fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats rhs_hs_ty
   = do { traceTc "tcTyFamInstEqn {" (vcat [ ppr fam_tc <+> ppr hs_pats ])
 
          -- First, check the arity of visible arguments
@@ -1838,10 +1839,13 @@ tcFamTyPatsAndGen fam_tc mb_cls_info imp_vars exp_bndrs hs_pats rhs_hs_ty
                   solveEqualities                              $
                   bindImplicitTKBndrs_Q_Skol imp_vars          $
                   bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
-                  do { (pats, res_kind) <- tcFamTyPats fam_tc mb_cls_info hs_pats
+                  do { (pats, res_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats
                      ; rhs_ty <- tcCheckLHsType rhs_hs_ty res_kind
                      ; return (pats, rhs_ty) }
 
+         -- Check that type patterns match the class instance head
+       ; checkConsistentFamInst mb_clsinfo fam_tc pats
+
        ; let scoped_tvs = imp_tvs ++ exp_tvs
        ; dvs  <- candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs)
        ; qtvs <- quantifyTyVars emptyVarSet dvs
@@ -1868,13 +1872,20 @@ tcFamTyPats fam_tc mb_clsinfo hs_pats
        ; (subst, invis_pats) <- tcInstTyBinders emptyTCvSubst mb_kind_env invis_bndrs
        ; let fun_ty = mkTyConApp fam_tc invis_pats
 
-       ; (_, pats, res_kind) <- tcInferApps typeLevelMode lhs_fun fun_ty
+       ; (fam_app, res_kind) <- tcInferApps typeLevelMode lhs_fun fun_ty
                                             (substTy subst body_kind) hs_pats
 
        ; traceTc "End tcFamTyPats }" $
          vcat [ ppr fam_tc <+> dcolon <+> ppr fun_kind
               , text "res_kind:" <+> ppr res_kind ]
-       ; return (invis_pats ++ pats, res_kind) }
+
+       -- We expect fam_app to look like (F t1 .. tn)
+       -- tcInferApps is capable of returning ((F ty1 |> co) ty2),
+       -- but that can't happen here because we already checked the
+       -- arity of F matches the number of pattern
+       ; case splitTyConApp_maybe fam_app of
+           Just (_, pats) -> return  (pats, res_kind)
+           Nothing        -> pprPanic "tcFamTyPats" bad_lhs }
   where
     fam_name  = tyConName fam_tc
     fam_arity = tyConArity fam_tc
@@ -1883,6 +1894,8 @@ tcFamTyPats fam_tc mb_clsinfo hs_pats
     (invis_bndrs, body_kind) = splitPiTysInvisibleN fam_arity fun_kind
     mb_kind_env = thdOf3 <$> mb_clsinfo
 
+    bad_lhs = hang (text "Ill-typed LHS of family instance")
+                 2 (ppr fam_tc <+> sep (map ppr hs_pats))
 
 {- Note [Constraints in patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3028,8 +3041,6 @@ checkValidClass cls
     cls_arity = length (tyConVisibleTyVars (classTyCon cls))
        -- Ignore invisible variables
     cls_tv_set = mkVarSet tyvars
-    mini_env   = zipVarEnv tyvars (mkTyVarTys tyvars)
-    mb_cls     = Just (cls, tyvars, mini_env)
 
     check_op constrained_class_methods (sel_id, dm)
       = setSrcSpan (getSrcSpan sel_id) $
@@ -3081,7 +3092,8 @@ checkValidClass cls
              -- Check that any default declarations for associated types are valid
            ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
              setSrcSpan loc $
-             checkValidTyFamEqn mb_cls fam_tc fam_tvs (mkTyVarTys fam_tvs) rhs }
+             tcAddFamInstCtxt (text "default type instance") (getName fam_tc) $
+             checkValidTyFamEqn fam_tc fam_tvs (mkTyVarTys fam_tvs) rhs }
         where
           fam_tvs = tyConTyVars fam_tc
 
@@ -3173,8 +3185,199 @@ checkFamFlag tc_name
     err_msg = hang (text "Illegal family declaration for" <+> quotes (ppr tc_name))
                  2 (text "Enable TypeFamilies to allow indexed type families")
 
-{- Note [Class method constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- | Extra information about the parent instance declaration, needed
+-- when type-checking associated types. The 'Class' is the enclosing
+-- class, the [TyVar] are the type variable of the instance decl,
+-- and and the @VarEnv Type@ maps class variables to their instance
+-- types.
+type ClsInstInfo = (Class, [TyVar], VarEnv Type)
+
+type AssocInstArgShape = (Maybe Type, Type)
+  -- AssocInstArgShape is used only for associated family instances
+  --    (mb_exp, actual)
+  -- mb_exp = Just ty  => this arg corresponds to a class variable
+  --        = Nothing  => it doesn't correspond to a class variable
+  -- e.g.  class C b where
+  --          type F a b c
+  --       instance C [x] where
+  --          type F p [x] q
+  -- We get [AssocInstArgShape] = [ (Nothing,  p)
+  --                              , (Just [x], [x])
+  --                              , (Nothing,  q)]
+
+
+checkConsistentFamInst :: Maybe ClsInstInfo
+                       -> TyCon     -- ^ Family tycon
+                       -> [Type]    -- ^ Type patterns from instance
+                       -> TcM ()
+-- See Note [Checking consistent instantiation]
+
+checkConsistentFamInst Nothing _ _ = return ()
+checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys
+  = do { -- Check that the associated type indeed comes from this class
+         -- See [Mismatched class methods and associated type families]
+         -- in TcInstDecls.
+
+         checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc)
+                 (badATErr (className clas) (tyConName fam_tc))
+
+       -- Check type args first (more comprehensible)
+       ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
+
+       -- And now kind args
+       ; checkTcM (all check_arg kind_shapes)
+                  (tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
+
+       ; traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
+                                                , ppr arg_shapes
+                                                , ppr mini_env ]) }
+  where
+    arg_shapes :: [AssocInstArgShape]
+    arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
+                 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
+
+    kind_shapes, type_shapes :: [AssocInstArgShape]
+    (kind_shapes, type_shapes) = partitionInvisibles $
+                                 arg_shapes `zip` tyConArgFlags fam_tc at_tys
+
+    check_arg :: AssocInstArgShape -> Bool
+    check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
+    check_arg (Nothing,     _    ) = True -- Arg position does not correspond
+                                          -- to a class variable
+
+    pp_wrong_at_arg
+      = vcat [ text "Type indexes must match class instance head"
+             , pp_exp_act ]
+
+    pp_exp_act
+      = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
+             , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_tys)
+             , sdocWithDynFlags $ \dflags ->
+               ppWhen (has_poly_args dflags) $
+               vcat [ text "where the `<tv>' arguments are type variables,"
+                    , text "distinct from each other and from the instance variables" ] ]
+
+    -- We need to tidy, since it's possible that expected_args will contain
+    -- inferred kind variables with names identical to those in at_tys. If we
+    -- don't, we'll end up with horrible messages like this one (#13972):
+    --
+    --   Expected: T (a -> Either a b)
+    --     Actual: T (a -> Either a b)
+    (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
+    (tidy_env2, expected_args)
+      = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
+                                | (exp_ty, at_ty) <- arg_shapes ]
+    mk_tv at_ty   = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
+    tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
+
+    has_poly_args dflags = any (isNothing . fst) shapes
+      where
+        shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
+               | otherwise                          = type_shapes
+
+badATErr :: Name -> Name -> SDoc
+badATErr clas op
+  = hsep [text "Class", quotes (ppr clas),
+          text "does not have an associated type", quotes (ppr op)]
+
+
+{- Note [Checking consistent instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See Trac #11450 for background discussion on this check.
+
+  class C a b where
+    type T a x b
+
+With this class decl, if we have an instance decl
+  instance C ty1 ty2 where ...
+then the type instance must look like
+     type T ty1 v ty2 = ...
+with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
+For example:
+
+  instance C [p] Int
+    type T [p] y Int = (p,y,y)
+
+Note that
+
+* We used to allow completely different bound variables in the
+  associated type instance; e.g.
+    instance C [p] Int
+      type T [q] y Int = ...
+  But from GHC 8.2 onwards, we don't.  It's much simpler this way.
+  See Trac #11450.
+
+* When the class variable isn't used on the RHS of the type instance,
+  it's tempting to allow wildcards, thus
+    instance C [p] Int
+      type T [_] y Int = (y,y)
+  But it's awkward to do the test, and it doesn't work if the
+  variable is repeated:
+    instance C (p,p) Int
+      type T (_,_) y Int = (y,y)
+  Even though 'p' is not used on the RHS, we still need to use 'p'
+  on the LHS to establish the repeated pattern.  So to keep it simple
+  we just require equality.
+
+* For variables in associated type families that are not bound by the class
+  itself, we do _not_ check if they are over-specific. In other words,
+  it's perfectly acceptable to have an instance like this:
+
+    instance C [p] Int where
+      type T [p] (Maybe x) Int = x
+
+  While the first and third arguments to T are required to be exactly [p] and
+  Int, respectively, since they are bound by C, the second argument is allowed
+  to be more specific than just a type variable. Furthermore, it is permissible
+  to define multiple equations for T that differ only in the non-class-bound
+  argument:
+
+    instance C [p] Int where
+      type T [p] (Maybe x)    Int = x
+      type T [p] (Either x y) Int = x -> y
+
+  We once considered requiring that non-class-bound variables in associated
+  type family instances be instantiated with distinct type variables. However,
+  that requirement proved too restrictive in practice, as there were examples
+  of extremely simple associated type family instances that this check would
+  reject, and fixing them required tiresome boilerplate in the form of
+  auxiliary type families. For instance, you would have to define the above
+  example as:
+
+    instance C [p] Int where
+      type T [p] x Int = CAux x
+
+    type family CAux x where
+      CAux (Maybe x)    = x
+      CAux (Either x y) = x -> y
+
+  We decided that this restriction wasn't buying us much, so we opted not
+  to pursue that design (see also GHC Trac #13398).
+
+Implementation
+  * 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. (where y can be any type, as
+    it is not scoped over the class type variables.
+
+We make all the instance type variables scope over the
+type instances, of course, which picks 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.
+
+Note [Class method constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Haskell 2010 is supposed to reject
   class C a where
     op :: Eq a => a -> a
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 88107da4b2..d59c4da0f3 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -10,9 +10,9 @@ module TcValidity (
   checkValidTheta, checkValidFamPats,
   checkValidInstance, checkValidInstHead, validDerivPred,
   checkTySynRhs,
-  ClsInstInfo, checkValidCoAxiom, checkValidCoAxBranch,
+  checkValidCoAxiom, checkValidCoAxBranch,
   checkValidTyFamEqn,
-  arityErr, badATErr,
+  arityErr,
   checkValidTelescope,
   allDistinctTyVars
   ) where
@@ -50,8 +50,8 @@ import FamInst     ( makeInjectivityErrors )
 import Name
 import VarEnv
 import VarSet
+import Var         ( VarBndr(..) )
 import Id          ( idType, idName )
-import Var         ( VarBndr(..), mkTyVar )
 import FV
 import ErrUtils
 import DynFlags
@@ -60,7 +60,6 @@ import ListSetOps
 import SrcLoc
 import Outputable
 import Bag         ( emptyBag )
-import Unique      ( mkAlphaTyVarUnique )
 import qualified GHC.LanguageExtensions as LangExt
 
 import Control.Monad
@@ -1621,118 +1620,6 @@ arbitrarily large type, depending on how 'a' is instantiated.
 So we require UndecidableInstances if we have a type family
 in the instance head.  Trac #15172.
 
-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, because it's an *associated* type.
-
-Note [Checking consistent instantiation]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See Trac #11450 for background discussion on this check.
-
-  class C a b where
-    type T a x b
-
-With this class decl, if we have an instance decl
-  instance C ty1 ty2 where ...
-then the type instance must look like
-     type T ty1 v ty2 = ...
-with exactly 'ty1' for 'a', 'ty2' for 'b', and some type 'v' for 'x'.
-For example:
-
-  instance C [p] Int
-    type T [p] y Int = (p,y,y)
-
-Note that
-
-* We used to allow completely different bound variables in the
-  associated type instance; e.g.
-    instance C [p] Int
-      type T [q] y Int = ...
-  But from GHC 8.2 onwards, we don't.  It's much simpler this way.
-  See Trac #11450.
-
-* When the class variable isn't used on the RHS of the type instance,
-  it's tempting to allow wildcards, thus
-    instance C [p] Int
-      type T [_] y Int = (y,y)
-  But it's awkward to do the test, and it doesn't work if the
-  variable is repeated:
-    instance C (p,p) Int
-      type T (_,_) y Int = (y,y)
-  Even though 'p' is not used on the RHS, we still need to use 'p'
-  on the LHS to establish the repeated pattern.  So to keep it simple
-  we just require equality.
-
-* For variables in associated type families that are not bound by the class
-  itself, we do _not_ check if they are over-specific. In other words,
-  it's perfectly acceptable to have an instance like this:
-
-    instance C [p] Int where
-      type T [p] (Maybe x) Int = x
-
-  While the first and third arguments to T are required to be exactly [p] and
-  Int, respectively, since they are bound by C, the second argument is allowed
-  to be more specific than just a type variable. Furthermore, it is permissible
-  to define multiple equations for T that differ only in the non-class-bound
-  argument:
-
-    instance C [p] Int where
-      type T [p] (Maybe x)    Int = x
-      type T [p] (Either x y) Int = x -> y
-
-  We once considered requiring that non-class-bound variables in associated
-  type family instances be instantiated with distinct type variables. However,
-  that requirement proved too restrictive in practice, as there were examples
-  of extremely simple associated type family instances that this check would
-  reject, and fixing them required tiresome boilerplate in the form of
-  auxiliary type families. For instance, you would have to define the above
-  example as:
-
-    instance C [p] Int where
-      type T [p] x Int = CAux x
-
-    type family CAux x where
-      CAux (Maybe x)    = x
-      CAux (Either x y) = x -> y
-
-  We decided that this restriction wasn't buying us much, so we opted not
-  to pursue that design (see also GHC Trac #13398).
-
-Implementation
-  * 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. (where y can be any type, as
-    it is not scoped over the class type variables.
-
-We make all the instance type variables scope over the
-type instances, of course, which picks 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.
-
 Note [Invisible arguments and termination]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When checking the ​Paterson conditions for termination an instance
@@ -1748,101 +1635,6 @@ described in Trac #15177, which contains a number of examples.
 The suspicious bits are the calls to filterOutInvisibleTypes.
 -}
 
--- | Extra information about the parent instance declaration, needed
--- when type-checking associated types. The 'Class' is the enclosing
--- class, the [TyVar] are the type variable of the instance decl,
--- and and the @VarEnv Type@ maps class variables to their instance
--- types.
-type ClsInstInfo = (Class, [TyVar], VarEnv Type)
-
-type AssocInstArgShape = (Maybe Type, Type)
-  -- AssocInstArgShape is used only for associated family instances
-  --    (mb_exp, actual)
-  -- mb_exp = Just ty  => this arg corresponds to a class variable
-  --        = Nothing  => it doesn't correspond to a class variable
-  -- e.g.  class C b where
-  --          type F a b c
-  --       instance C [x] where
-  --          type F p [x] q
-  -- We get [AssocInstArgShape] = [ (Nothing,  p)
-  --                              , (Just [x], [x])
-  --                              , (Nothing,  q)]
-
-checkConsistentFamInst
-               :: Maybe ClsInstInfo
-               -> TyCon              -- ^ Family tycon
-               -> [Type]             -- ^ Type patterns from instance
-               -> TcM ()
--- See Note [Checking consistent instantiation]
-
-checkConsistentFamInst Nothing _ _ = return ()
-checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys
-  = do { -- Check that the associated type indeed comes from this class
-         -- See [Mismatched class methods and associated type families]
-         -- in TcInstDecls.
-
-         checkTc (Just (classTyCon clas) == tyConAssoc_maybe fam_tc)
-                 (badATErr (className clas) (tyConName fam_tc))
-
-       -- Check type args first (more comprehensible)
-       ; checkTc (all check_arg type_shapes)   pp_wrong_at_arg
-
-       -- And now kind args
-       ; checkTcM (all check_arg kind_shapes)
-                  (tidy_env2, pprWithExplicitKindsWhen True pp_wrong_at_arg)
-
-       ; traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
-                                                , ppr arg_shapes
-                                                , ppr mini_env ]) }
-  where
-    arg_shapes :: [AssocInstArgShape]
-    arg_shapes = [ (lookupVarEnv mini_env fam_tc_tv, at_ty)
-                 | (fam_tc_tv, at_ty) <- tyConTyVars fam_tc `zip` at_tys ]
-
-    kind_shapes, type_shapes :: [AssocInstArgShape]
-    (kind_shapes, type_shapes) = partitionInvisibles $
-                                 arg_shapes `zip` tyConArgFlags fam_tc at_tys
-
-    check_arg :: AssocInstArgShape -> Bool
-    check_arg (Just exp_ty, at_ty) = exp_ty `tcEqType` at_ty
-    check_arg (Nothing,     _    ) = True -- Arg position does not correspond
-                                          -- to a class variable
-
-    pp_wrong_at_arg
-      = vcat [ text "Type indexes must match class instance head"
-             , pp_exp_act ]
-
-    pp_exp_act
-      = vcat [ text "Expected:" <+> ppr (mkTyConApp fam_tc expected_args)
-             , text "  Actual:" <+> ppr (mkTyConApp fam_tc at_tys)
-             , sdocWithDynFlags $ \dflags ->
-               ppWhen (has_poly_args dflags) $
-               vcat [ text "where the `<tv>' arguments are type variables,"
-                    , text "distinct from each other and from the instance variables" ] ]
-
-    -- We need to tidy, since it's possible that expected_args will contain
-    -- inferred kind variables with names identical to those in at_tys. If we
-    -- don't, we'll end up with horrible messages like this one (#13972):
-    --
-    --   Expected: T (a -> Either a b)
-    --     Actual: T (a -> Either a b)
-    (tidy_env1, _) = tidyOpenTypes emptyTidyEnv at_tys
-    (tidy_env2, expected_args)
-      = tidyOpenTypes tidy_env1 [ exp_ty `orElse` mk_tv at_ty
-                                | (exp_ty, at_ty) <- arg_shapes ]
-    mk_tv at_ty   = mkTyVarTy (mkTyVar tv_name (typeKind at_ty))
-    tv_name = mkInternalName (mkAlphaTyVarUnique 1) (mkTyVarOcc "<tv>") noSrcSpan
-
-    has_poly_args dflags = any (isNothing . fst) shapes
-      where
-        shapes | gopt Opt_PrintExplicitKinds dflags = arg_shapes
-               | otherwise                          = type_shapes
-
-badATErr :: Name -> Name -> SDoc
-badATErr clas op
-  = hsep [text "Class", quotes (ppr clas),
-          text "does not have an associated type", quotes (ppr op)]
-
 
 {-
 ************************************************************************
@@ -1854,7 +1646,7 @@ badATErr clas op
 
 checkValidCoAxiom :: CoAxiom Branched -> TcM ()
 checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
-  = do { mapM_ (checkValidCoAxBranch Nothing fam_tc) branch_list
+  = do { mapM_ (checkValidCoAxBranch fam_tc) branch_list
        ; foldlM_ check_branch_compat [] branch_list }
   where
     branch_list = fromBranches branches
@@ -1907,26 +1699,24 @@ checkValidCoAxiom ax@(CoAxiom { co_ax_tc = fam_tc, co_ax_branches = branches })
 -- Check that a "type instance" is well-formed (which includes decidability
 -- unless -XUndecidableInstances is given).
 --
-checkValidCoAxBranch :: Maybe ClsInstInfo
-                     -> TyCon -> CoAxBranch -> TcM ()
-checkValidCoAxBranch mb_clsinfo fam_tc
+checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()
+checkValidCoAxBranch fam_tc
                     (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
                                 , cab_lhs = typats
                                 , cab_rhs = rhs, cab_loc = loc })
   = setSrcSpan loc $
-    checkValidTyFamEqn mb_clsinfo fam_tc (tvs++cvs) typats rhs
+    checkValidTyFamEqn fam_tc (tvs++cvs) typats rhs
 
 -- | Do validity checks on a type family equation, including consistency
 -- with any enclosing class instance head, termination, and lack of
 -- polytypes.
-checkValidTyFamEqn :: Maybe ClsInstInfo
-                   -> TyCon   -- ^ of the type family
+checkValidTyFamEqn :: TyCon   -- ^ of the type family
                    -> [Var]   -- ^ Bound variables in the equation
                    -> [Type]  -- ^ Type patterns
                    -> Type    -- ^ Rhs
                    -> TcM ()
-checkValidTyFamEqn mb_clsinfo fam_tc qvs typats rhs
-  = do { checkValidFamPats mb_clsinfo fam_tc qvs typats rhs
+checkValidTyFamEqn fam_tc qvs typats rhs
+  = do { checkValidFamPats fam_tc qvs typats rhs
 
          -- The argument patterns, and RHS, are all boxed tau types
          -- E.g  Reject type family F (a :: k1) :: k2
@@ -1971,23 +1761,20 @@ checkFamInstRhs lhs_tc lhs_tys famInsts
                        --   [a,b,a,a] \\ [a,a] = [b,a]
                        -- So we are counting repetitions
 
-checkValidFamPats :: Maybe ClsInstInfo
-                  -> TyCon -> [Var]
+checkValidFamPats :: TyCon -> [Var]
                   -> [Type]   -- ^ patterns
                   -> Type     -- ^ RHS
                   -> TcM ()
 -- Patterns in a 'type instance' or 'data instance' decl should
--- a) contain no type family applications
+-- a) Shoule contain no type family applications
 --    (vanilla synonyms are fine, though)
 -- b) For associated types, are consistently instantiated
-checkValidFamPats mb_clsinfo fam_tc qvs pats rhs
+checkValidFamPats fam_tc qvs pats rhs
   = do { checkValidTypePats fam_tc pats
 
          -- Check for things used on the right but not bound on the left
        ; checkFamPatBinders fam_tc qvs pats rhs
 
-         -- Check that type patterns match the class instance head
-       ; checkConsistentFamInst mb_clsinfo fam_tc pats
        ; traceTc "checkValidFamPats" (ppr fam_tc <+> ppr pats)
        }