Finally, validate-clean

Except for polykinds/T14846, where there is an extra
error message.  I actually tnink it's correct, but have
not checked yet.

14 files changed, 204 insertions, 179 deletions

diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 11a0e20828..abdce588a3 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -1451,7 +1451,6 @@ tcExtendTyVarEnvForRhs (Just sig) thing_inside
 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
 tcExtendTyVarEnvFromSig sig_inst thing_inside
   | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
-     -- Note [Use tcExtendTyVar not scopeTyVars in tcRhs]
   = tcExtendNameTyVarEnv wcs $
     tcExtendNameTyVarEnv skol_prs $
     thing_inside
@@ -1591,29 +1590,6 @@ Example for (E2), we generate
 The beta is untoucable, but floats out of the constraint and can
 be solved absolutely fine.
 
-Note [Use tcExtendTyVar not scopeTyVars in tcRhs]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Normally, any place that corresponds to Λ or ∀ in Core should be flagged
-with a call to scopeTyVars, which arranges for an implication constraint
-to be made, bumps the TcLevel, and (crucially) prevents a unification
-variable created outside the scope of a local skolem to unify with that
-skolem.
-
-We do not need to do this here, however.
-
-- Note that this happens only in the case of a partial signature.
-  Complete signatures go via tcPolyCheck, not tcPolyInfer.
-
-- The TcLevel is incremented in tcPolyInfer, right outside the call
-  to tcMonoBinds. We thus don't have to worry about outer metatvs unifying
-  with local skolems.
-
-- The other potential concern is that we need SkolemInfo associated with
-  the skolems. This, too, is OK, though: the constraints pass through
-  simplifyInfer (which doesn't report errors), at the end of which
-  the skolems will get quantified and put into an implication constraint.
-  Thus, by the time any errors are reported, the SkolemInfo will be
-  in place.
 
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs
index fe29c3d1d0..c2d58b31c2 100644
--- a/compiler/typecheck/TcClassDcl.hs
+++ b/compiler/typecheck/TcClassDcl.hs
@@ -198,9 +198,6 @@ tcClassDecl2 (L _ (ClassDecl {tcdLName = class_name, tcdSigs = sigs,
 
         ; let tc_item = tcDefMeth clas clas_tyvars this_dict
                                   default_binds sig_fn prag_fn
-                   -- tcExtendTyVarEnv here (instead of scopeTyVars) is OK:
-                   -- the tcDefMeth calls checkConstraints to bump the TcLevel
-                   -- and make the implication constraint
         ; dm_binds <- tcExtendTyVarEnv clas_tyvars $
                       mapM tc_item op_items
 
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 05c7958441..562e084aaf 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -759,9 +759,6 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
   = setSrcSpan (getLoc (hsSigType deriv_pred)) $
     -- Use loc of the 'deriving' item
     do  { (mb_deriv_strat', deriv_tvs, (cls, cls_tys, cls_arg_kinds))
-                   -- Why not scopeTyVars? Because these are *TyVar*s, not TcTyVars.
-                   -- Their kinds are fully settled. No need to worry about skolem
-                   -- escape.
                 <- tcExtendTyVarEnv tvs $
                 -- Deriving preds may (now) mention
                 -- the type variables for the type constructor, hence tcExtendTyVarenv
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index 425a6a8fff..d32272bfc5 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -467,18 +467,10 @@ tcExtendKindEnv extra_env thing_inside
 
 -----------------------
 -- Scoped type and kind variables
--- Before using this function, consider using TcHsType.scopeTyVars, which
--- bumps the TcLevel and thus prevents any of these TyVars from appearing
--- in kinds of tyvars in an outer scope.
--- Indeed, you should always use scopeTyVars unless some other code nearby
--- bumps the TcLevel.
 tcExtendTyVarEnv :: [TyVar] -> TcM r -> TcM r
 tcExtendTyVarEnv tvs thing_inside
   = tcExtendNameTyVarEnv (mkTyVarNamePairs tvs) thing_inside
 
--- Before using this function, consider using TcHsType.scopeTyVars2, which
--- bumps the TcLevel and thus prevents any of these TyVars from appearing
--- in kinds of tyvars in an outer scope.
 tcExtendNameTyVarEnv :: [(Name,TcTyVar)] -> TcM r -> TcM r
 tcExtendNameTyVarEnv binds thing_inside
   -- this should be used only for explicitly mentioned scoped variables.
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 6261b6a440..8a8c3d3b33 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -31,7 +31,7 @@ module TcHsType (
         tcDataKindSig,
 
           -- tyvars
-        scopeTyVars, zonkAndScopedSort,
+        zonkAndScopedSort,
 
         -- Kind-checking types
         -- No kind generalisation, no checkValidType
@@ -47,7 +47,7 @@ module TcHsType (
         typeLevelMode, kindLevelMode,
 
         kindGeneralize, checkExpectedKindX,
-        instantiateTyN, 
+        instantiateTyN,
         reportFloatingKvs,
 
         -- Sort-checking kinds
@@ -232,7 +232,7 @@ tc_hs_sig_type_and_gen skol_info hs_sig_type ctxt_kind
   = do { (tc_lvl, (wanted, (spec_tkvs, ty)))
               <- pushTcLevelM                                   $
                  solveLocalEqualitiesX "tc_hs_sig_type_and_gen" $
-                 bindImplicitTKBndrs_Skol sig_vars               $
+                 bindImplicitTKBndrs_Skol sig_vars              $
                  do { kind <- newExpectedKind ctxt_kind
 
                     ; tc_lhs_type typeLevelMode hs_ty kind }
@@ -1482,6 +1482,33 @@ newWildTyVar _name
        ; traceTc "newWildTyVar" (ppr tyvar)
        ; return tyvar }
 
+{- *********************************************************************
+*                                                                      *
+             Kind inference for type declarations
+*                                                                      *
+********************************************************************* -}
+
+{- Note [The initial kind of a type constructor]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+kcLHsQTyVars is responsible for getting the initial kind of
+a type constructor.
+
+It has two cases:
+
+ * The TyCon has a CUSK.  In that case, find the full, final,
+   poly-kinded kind of the TyCon.  It's very like a term-level
+   binding where we have a complete type signature for the
+   function.
+
+ * It does not have a CUSK.  Find a monomorphic kind, with
+   unification variables in it; they will be generalised later.
+   It's very like a term-level binding where we do not have
+   a type signature (or, more accurately, where we have a
+   partial type signature), so we infer the type and generalise.
+-}
+
+
+------------------------------
 -- | Kind-check a 'LHsQTyVars'. If the decl under consideration has a complete,
 -- user-supplied kind signature (CUSK), generalise the result.
 -- Used in 'getInitialKind' (for tycon kinds and other kinds)
@@ -1496,12 +1523,25 @@ kcLHsQTyVars :: Name              -- ^ of the thing being checked
              -> LHsQTyVars GhcRn
              -> TcM Kind          -- ^ The result kind
              -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
-kcLHsQTyVars name flav cusk
+kcLHsQTyVars name flav cusk tvs thing_inside
+  | cusk      = kcLHsQTyVars_Cusk    name flav tvs thing_inside
+  | otherwise = kcLHsQTyVars_NonCusk name flav tvs thing_inside
+
+
+kcLHsQTyVars_Cusk, kcLHsQTyVars_NonCusk
+    :: Name              -- ^ of the thing being checked
+    -> TyConFlavour      -- ^ What sort of 'TyCon' is being checked
+    -> LHsQTyVars GhcRn
+    -> TcM Kind          -- ^ The result kind
+    -> TcM TcTyCon       -- ^ A suitably-kinded TcTyCon
+
+------------------------------
+kcLHsQTyVars_Cusk name flav
   user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
                                            , hsq_dependent = dep_names }
                       , hsq_explicit = hs_tvs }) thing_inside
-  | cusk
-    -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
+  -- CUSK case
+  -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
   = addTyConFlavCtxt name flav $
     do { (scoped_kvs, (tc_tvs, res_kind))
            <- pushTcLevelM_                               $
@@ -1573,8 +1613,19 @@ kcLHsQTyVars name flav cusk
               , text "all_tv_prs" <+> ppr all_tv_prs ]
 
        ; return tycon }
+  where
+    ctxt_kind | tcFlavourIsOpen flav = TheKind liftedTypeKind
+              | otherwise            = AnyKind
 
-  | otherwise     -- Not CUSK
+kcLHsQTyVars_Cusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
+
+------------------------------
+kcLHsQTyVars_NonCusk name flav
+  user_tyvars@(HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = kv_ns
+                                           , hsq_dependent = dep_names }
+                      , hsq_explicit = hs_tvs }) thing_inside
+  -- Non_CUSK case
+  -- See note [Required, Specified, and Inferred for types] in TcTyClsDecls
   = do { (scoped_kvs, (tc_tvs, res_kind))
            -- Why bindImplicitTKBndrs_Q_Tv which uses newTyVarTyVar?
            -- See Note [Inferring kinds for type declarations] in TcTyClsDecls
@@ -1614,7 +1665,7 @@ kcLHsQTyVars name flav cusk
        | otherwise
        = mkAnonTyConBinder tv
 
-kcLHsQTyVars _ _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
+kcLHsQTyVars_NonCusk _ _ (XLHsQTyVars _) _ = panic "kcLHsQTyVars"
 
 
 {- Note [Kind-checking tyvar binders for associated types]
@@ -1849,28 +1900,6 @@ tcHsQTyVarBndr _ _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
 
 
 
---------------------------
--- Bringing tyvars into scope
---------------------------
-
--- | Bring tyvars into scope, wrapping the thing_inside in an implication
--- constraint. The implication constraint is necessary to provide SkolemInfo
--- for the tyvars and to ensure that no unification variables made outside
--- the scope of these tyvars (i.e. lower TcLevel) unify with the locally-scoped
--- tyvars (i.e. higher TcLevel).
---
--- INVARIANT: The thing_inside must check only types, never terms.
---
--- Use this (not tcExtendTyVarEnv) wherever you expect a Λ or ∀ in Core.
--- Use tcExtendTyVarEnv otherwise.
-scopeTyVars :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
-scopeTyVars skol_info tvs thing_inside
-  = fmap snd $ -- discard the TcEvBinds, which will always be empty
-    checkConstraints skol_info tvs [{- no EvVars -}] $
-    tcExtendTyVarEnv tvs $
-    thing_inside
-
-
 {- *********************************************************************
 *                                                                      *
              Kind generalisation
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 914114f508..de891608cb 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -547,29 +547,6 @@ lot of kinding and type checking code with ordinary algebraic data types (and
 GADTs).
 -}
 
-tcFamInstDeclChecks :: Maybe ClsInstInfo
-                      -> Located Name -> TcM TyCon
-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?
-       ; 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)
-
-       ; return fam_tc }
-
 tcTyFamInstDecl :: Maybe ClsInstInfo
                 -> LTyFamInstDecl GhcRn -> TcM FamInst
   -- "type instance"
@@ -626,27 +603,19 @@ tcDataFamInstDecl mb_clsinfo
        ; let exp_bndrs = mb_bndrs `orElse` []
              data_ctxt = DataKindCtxt fam_name
 
-       ; (imp_tvs, (exp_tvs, (pats, stupid_theta, res_kind)))
-               <- pushTcLevelM_                                $
-                  solveEqualities                              $
-                  bindImplicitTKBndrs_Q_Skol imp_vars          $
-                  bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
-                  do { (pats, res_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats
-                     ; stupid_theta <- tcHsContext ctxt
-                     ; mapM_ (wrapLocM kcConDecl) cons
-
-                     ; exp_res_kind <- case m_ksig of
-                          Nothing   -> return liftedTypeKind
-                          Just hs_k -> tcLHsKindSig data_ctxt hs_k
-                     ; _ <- checkExpectedKindX pp_hs_pats bogus_ty
-                                               res_kind exp_res_kind
-                            -- ToDo: what about a non-triv result?
+       ; (qtvs, pats, (stupid_theta, res_kind))
+            <- tcFamTyPatsAndGen fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats $
+               \ res_kind -> do { stupid_theta <- tcHsContext ctxt
+                                ; mapM_ (wrapLocM kcConDecl) cons
 
-                     ; return (pats, stupid_theta, res_kind) }
+                                ; exp_res_kind <- case m_ksig of
+                                     Nothing   -> return liftedTypeKind
+                                     Just hs_k -> tcLHsKindSig data_ctxt hs_k
+                                ; _ <- checkExpectedKindX pp_hs_pats bogus_ty
+                                                          res_kind exp_res_kind
+                                       -- ToDo: what about a non-triv result?
 
-       ; let scoped_tvs = imp_tvs ++ exp_tvs
-       ; dvs  <- candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs)
-       ; qtvs <- quantifyTyVars emptyVarSet dvs
+                                ; return (stupid_theta, res_kind) }
 
        -- Zonk the patterns etc into the Type world
        ; (ze, qtvs)   <- zonkTyBndrs qtvs
@@ -684,7 +653,7 @@ tcDataFamInstDecl mb_clsinfo
        ; traceTc "tcDataFamInstDecl" (ppr fam_tc $$ ppr pats $$ ppr imp_vars $$ ppr exp_bndrs
                                       $$ ppr cons)
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
-           do { data_cons <- tcExtendTyVarEnv scoped_tvs $
+           do { data_cons <- tcExtendTyVarEnv qtvs $
                              -- For H98 decls, the tyvars scope
                              -- over the data constructors
                              tcConDecls rec_rep_tc ty_binders orig_res_ty cons
@@ -766,6 +735,30 @@ tcDataFamInstDecl _ (L _ (DataFamInstDecl (HsIB _ (XFamEqn _))))
   = panic "tcDataFamInstDecl"
 
 
+---------------------
+tcFamInstDeclChecks :: Maybe ClsInstInfo
+                      -> Located Name -> TcM TyCon
+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?
+       ; 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)
+
+       ; return fam_tc }
+
 {- Note [Associated type instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We allow this:
@@ -1314,8 +1307,6 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys
                                 , ib_pragmas    = sigs
                                 , ib_extensions = exts
                                 , ib_derived    = is_derived })
-      -- tcExtendTyVarEnv (not scopeTyVars) is OK because the TcLevel is pushed
-      -- in checkInstConstraints
   = tcExtendNameTyVarEnv (lexical_tvs `zip` tyvars) $
        -- The lexical_tvs scope over the 'where' part
     do { traceTc "tcInstMeth" (ppr sigs $$ ppr binds)
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index 7ac0dd4356..19ec6de622 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -410,7 +410,7 @@ tc_pat penv (ViewPat _ expr pat) overall_pat_ty thing_inside
 tc_pat penv (SigPat _ pat sig_ty) pat_ty thing_inside
   = do  { (inner_ty, tv_binds, wcs, wrap) <- tcPatSig (inPatBind penv)
                                                             sig_ty pat_ty
-                -- Using tcExtendNameTyVarEnv is appropriate here (not scopeTyVars2)
+                -- Using tcExtendNameTyVarEnv is appropriate here
                 -- because we're not really bringing fresh tyvars into scope.
                 -- We're *naming* existing tyvars. Note that it is OK for a tyvar
                 -- from an outer scope to mention one of these tyvars in its kind.
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index c7b1ede246..dde8cbac9e 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -16,7 +16,7 @@ module TcTyClsDecls (
         -- Functions used by TcInstDcls to check
         -- data/type family instance declarations
         kcConDecl, tcConDecls, dataDeclChecks, checkValidTyCon,
-        tcFamTyPats, tcTyFamInstEqn,
+        tcFamTyPatsAndGen, tcTyFamInstEqn,
         tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
         wrongKindOfFamily,
         ClsInstInfo, checkConsistentFamInst
@@ -1405,9 +1405,9 @@ tcDefaultAssocDecl _ (d1:_:_)
   = failWithTc (text "More than one default declaration for"
                 <+> ppr (feqn_tycon (unLoc d1)))
 
-tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = (dL->L _ tc_name)
+tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
                                              , feqn_pats = hs_tvs
-                                             , feqn_rhs = rhs })]
+                                             , feqn_rhs = hs_rhs_ty })]
   | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
            , hsq_explicit = exp_vars } <- hs_tvs
   = -- See Note [Type-checking default assoc decls]
@@ -1436,11 +1436,17 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = (dL->L _ tc_name)
           -- at an associated type. But this would be wrong, because an associated
           -- type default LHS can mention *different* type variables than the
           -- enclosing class. So it's treated more as a freestanding beast.
-       ; (_tvs', pats', rhs_ty) <- tcFamTyPatsAndGen fam_tc Nothing
-                                                     imp_vars exp_vars pats rhs
+       ; (qtvs, pats, rhs_ty) <- tcFamTyPatsAndGen fam_tc Nothing
+                                                   imp_vars exp_vars pats
+                                                   (tcCheckLHsType hs_rhs_ty)
+
+       ; (ze, _qtvs) <- zonkTyBndrs qtvs
+       ; pats        <- zonkTcTypesToTypesX ze pats
+       ; rhs_ty      <- zonkTcTypeToTypeX   ze rhs_ty
 
          -- See Note [Type-checking default assoc decls]
-       ; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
+       ; traceTc "tcDefalut" (vcat [ppr (tyConTyVars fam_tc), ppr _qtvs, ppr pats])
+       ; case tcMatchTys pats (mkTyVarTys (tyConTyVars fam_tc)) of
            Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
            Nothing    -> failWithTc (defaultAssocKindErr fam_tc)
            -- We check for well-formedness and validity later,
@@ -1763,16 +1769,33 @@ tcTyFamInstEqn fam_tc mb_clsinfo
     (dl->L loc (HsIB { hsib_ext = imp_vars
                  , hsib_body = FamEqn { feqn_tycon  = L _ eqn_tc_name
                                       , feqn_bndrs  = mb_expl_bndrs
-                                      , feqn_pats   = lhs_hs_pats
+                                      , feqn_pats   = hs_pats
                                       , feqn_rhs    = rhs_hs_ty }}))
   = ASSERT( getName fam_tc == eqn_tc_name )
     setSrcSpan loc $
-    do { (tvs, pats, rhs_ty) <- tcFamTyPatsAndGen fam_tc mb_clsinfo
-                                     imp_vars (mb_expl_bndrs `orElse` [])
-                                     lhs_hs_pats rhs_hs_ty
+    do {
+       -- First, check the arity of visible arguments
+       -- If we wait until validity checking, we'll get kind errors
+       -- below when an arity error will be much easier to understand.
+       ; let vis_arity = length (tyConVisibleTyVars fam_tc)
+       ; checkTc (hs_pats `lengthIs` vis_arity) $
+         wrongNumberOfParmsErr vis_arity
 
-       ; return (mkCoAxBranch tvs [] pats rhs_ty
-                              (map (const Nominal) tvs)
+       ; (qtvs, pats, rhs_ty) <- tcFamTyPatsAndGen fam_tc mb_clsinfo
+                                      imp_vars (mb_expl_bndrs `orElse` [])
+                                      hs_pats
+                                      (tcCheckLHsType rhs_hs_ty)
+
+       ; (ze, qtvs') <- zonkTyBndrs qtvs
+       ; pats'       <- zonkTcTypesToTypesX ze pats
+       ; rhs_ty'     <- zonkTcTypeToTypeX   ze rhs_ty
+
+       -- Check that type patterns match the class instance head
+       ; checkConsistentFamInst mb_clsinfo fam_tc pats'
+
+       ; traceTc "tcTyFamInstEqn" (ppr fam_tc $$ ppr qtvs' $$ ppr pats' $$ ppr rhs_ty')
+       ; return (mkCoAxBranch qtvs' [] pats' rhs_ty'
+                              (map (const Nominal) qtvs')
                               loc) }
 
 tcTyFamInstEqn _ _ (dL->L _ (XHsImplicitBndrs _)) = panic "tcTyFamInstEqn"
@@ -1804,61 +1827,67 @@ indexed-types/should_compile/T12369 for an example.
 So, the kind-checker must return the new skolems and args (that is, Type
 or (Type -> Type) for the equations above) and the instantiated kind.
 
-Note [Failing early in kcDataDefn]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
-calls tcConDecl, which checks that the return type of a GADT-like constructor
-is actually an instance of the type head. Without the checkNoErrs, potentially
-two bad things could happen:
-
- 1) Duplicate error messages, because tcConDecl will be called again during
-    *type* checking (as opposed to kind checking)
- 2) If we just keep blindly forging forward after both kind checking and type
-    checking, we can get a panic in rejigConRes. See Trac #8368.
--}
+Note [Generalising in tcFamTyPatsAndThen]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have something like
+  type instance forall (a::k) b. F t1 t2 = rhs
+
+Then  imp_vars = [k], exp_bndrs = [a::k, b]
+
+We want to quantify over
+  * k, a, and b  (all user-specified)
+  * and any inferred free kind vars from
+      - the kinds of k, a, b
+      - the types t1, t2
+
+However, unlike a type signature like
+  f :: forall (a::k). blah
 
+we do /not/ care about the Inferred/Specified designation
+or order for the final quantified tyvars.  Type-family
+instances are not invoked directly in Haskell source code,
+so visible type application etc plays no role.
+
+So, the simple thing is
+   - gather candiates from [k, a, b] and pats
+   - quantify over them
+
+Hence the sligtly mysterious call:
+    candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs)
+
+Simple, neat, but a little non-obvious!
+-}
 
 --------------------------
 tcFamTyPatsAndGen :: TyCon -> Maybe ClsInstInfo
                   -> [Name] -> [LHsTyVarBndr GhcRn]  -- Implicit and explicicit binder
                   -> HsTyPats GhcRn                  -- Patterns
-                  -> LHsType GhcRn                   -- RHS type
-                  -> TcM ([TyVar], [TcType], TcType) -- (tyvars, pats, rhs)
-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
-         -- If we wait until validity checking, we'll get kind errors
-         -- below when an arity error will be much easier to understand.
-       ; let vis_arity = length (tyConVisibleTyVars fam_tc)
-       ; checkTc (hs_pats `lengthIs` vis_arity) $
-         wrongNumberOfParmsErr vis_arity
+                  -> (TcKind -> TcM a)               -- RHS
+                  -> TcM ([TyVar], [TcType], a)      -- (tyvars, pats, rhs)
+tcFamTyPatsAndGen fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats thing_inside
+  = do { traceTc "tcFamTyPatsAndGen {" (vcat [ ppr fam_tc <+> ppr hs_pats ])
 
+       -- By now, for type families (but not data families) we should
+       -- have checked that the number of patterns matches tyConArity
+
+       -- This code is closely related to the code
+       -- in TcHsType.kcLHsQTyVars_Cusk
        ; (imp_tvs, (exp_tvs, (pats, rhs_ty)))
                <- pushTcLevelM_                                $
                   solveEqualities                              $
                   bindImplicitTKBndrs_Q_Skol imp_vars          $
                   bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
                   do { (pats, res_kind) <- tcFamTyPats fam_tc mb_clsinfo hs_pats
-                     ; rhs_ty <- tcCheckLHsType rhs_hs_ty res_kind
+                     ; rhs_ty <- thing_inside res_kind
                      ; return (pats, rhs_ty) }
 
-         -- Check that type patterns match the class instance head
-       ; checkConsistentFamInst mb_clsinfo fam_tc pats
-
+       -- See Note [Generalising in tcFamTyPatsAndThen]
        ; let scoped_tvs = imp_tvs ++ exp_tvs
        ; dvs  <- candidateQTyVarsOfTypes (pats ++ mkTyVarTys scoped_tvs)
        ; qtvs <- quantifyTyVars emptyVarSet dvs
 
-       ; (ze, qtvs') <- zonkTyBndrs qtvs
-       ; pats'       <- zonkTcTypesToTypesX ze pats
-       ; rhs_ty'     <- zonkTcTypeToTypeX   ze rhs_ty
-
-       ; traceTc "xxx2" (ppr fam_tc $$ ppr qtvs)
-         -- Needs the pats to be zonked
-
-       ; traceTc "tcTyFamInstEqn }" (ppr fam_tc <+> pprTyVars qtvs')
-       ; return (qtvs', pats', rhs_ty') }
+       ; traceTc "tcFamTyPatsAndGen }" (ppr fam_tc <+> pprTyVars qtvs)
+       ; return (qtvs, pats, rhs_ty) }
 
 -----------------
 tcFamTyPats :: TyCon -> Maybe ClsInstInfo
@@ -1885,7 +1914,8 @@ tcFamTyPats fam_tc mb_clsinfo hs_pats
        -- 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 }
+           Nothing        -> WARN( True, bad_lhs fam_app )
+                             return ([], res_kind) }
   where
     fam_name  = tyConName fam_tc
     fam_arity = tyConArity fam_tc
@@ -1894,8 +1924,9 @@ 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))
+    bad_lhs fam_app
+      = hang (text "Ill-typed LHS of family instance")
+           2 (debugPprType fam_app)
 
 {- Note [Constraints in patterns]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 0a47e2fbda..2bd6ae585b 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -3277,9 +3277,10 @@ debug_ppr_ty prec (TyConApp tc tys)
   | otherwise = maybeParen prec appPrec $
                 hang (ppr tc) 2 (sep (map (debug_ppr_ty appPrec) tys))
 
-debug_ppr_ty prec (AppTy t1 t2)
-  = hang (debug_ppr_ty prec t1)
-       2 (debug_ppr_ty appPrec t2)
+debug_ppr_ty _ (AppTy t1 t2)
+  = hang (debug_ppr_ty appPrec t1)  -- Print parens so we see ((a b) c)
+       2 (debug_ppr_ty appPrec t2)  -- so that we can distinguish
+                                    -- TyConApp from AppTy
 
 debug_ppr_ty prec (CastTy ty co)
   = maybeParen prec topPrec $
diff --git a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
index 5640807467..dfe46243ee 100644
--- a/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
+++ b/testsuite/tests/indexed-types/should_fail/SimpleFail9.stderr
@@ -1,5 +1,5 @@
 
-SimpleFail9.hs:14:8: error:
+SimpleFail9.hs:14:3: error:
     • Type indexes must match class instance head
       Expected: S7 (a, Int)
         Actual: S7 (b, Int)
diff --git a/testsuite/tests/indexed-types/should_fail/T10817.stderr b/testsuite/tests/indexed-types/should_fail/T10817.stderr
index 715febdc25..af8acae33a 100644
--- a/testsuite/tests/indexed-types/should_fail/T10817.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T10817.stderr
@@ -1,6 +1,7 @@
 
 T10817.hs:9:3: error:
-    The type family application ‘F a’
-      is no smaller than the instance head ‘F a’
-    (Use UndecidableInstances to permit this)
-    In the class declaration for ‘C’
+    • The type family application ‘F a’
+        is no smaller than the instance head ‘F a’
+      (Use UndecidableInstances to permit this)
+    • In the default type instance declaration for ‘F’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/indexed-types/should_fail/T10899.stderr b/testsuite/tests/indexed-types/should_fail/T10899.stderr
index 925e4348fe..0dd92ef9bf 100644
--- a/testsuite/tests/indexed-types/should_fail/T10899.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T10899.stderr
@@ -1,4 +1,5 @@
 
 T10899.hs:7:3: error:
     • Illegal polymorphic type: forall (m :: * -> *). m a
-    • In the class declaration for ‘C’
+    • In the default type instance declaration for ‘F’
+      In the class declaration for ‘C’
diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr
index 9aa4ab50d9..f9e5132a34 100644
--- a/testsuite/tests/polykinds/T8616.stderr
+++ b/testsuite/tests/polykinds/T8616.stderr
@@ -13,3 +13,12 @@ T8616.hs:8:16: error:
           withSomeSing = undefined :: (Any :: k)
     • Relevant bindings include
         withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1)
+
+T8616.hs:8:30: error:
+    • Expected a type, but ‘Any :: k’ has kind ‘k’
+    • In an expression type signature: (Any :: k)
+      In the expression: undefined :: (Any :: k)
+      In an equation for ‘withSomeSing’:
+          withSomeSing = undefined :: (Any :: k)
+    • Relevant bindings include
+        withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1)
diff --git a/testsuite/tests/printer/Ppr040.hs b/testsuite/tests/printer/Ppr040.hs
index 6fc7b09b15..1af4673c0e 100644
--- a/testsuite/tests/printer/Ppr040.hs
+++ b/testsuite/tests/printer/Ppr040.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TemplateHaskell, RankNTypes, TypeOperators, DataKinds,
+{-# LANGUAGE RankNTypes, TypeOperators, DataKinds,
              PolyKinds, TypeFamilies, GADTs, StarIsType #-}
 
 module RAE_T32a where
@@ -13,14 +13,14 @@ type family (a :: TyArr k1 k2) @@ (b :: k1) :: k2
 data TyPi' (a :: *) (b :: TyArr a *) :: *
 type TyPi (a :: *) (b :: TyArr a *) = TyPi' a b -> *
 type family (a :: TyPi k1 k2) @@@ (b :: k1) :: k2 @@ b
-$(return [])
+-- $(return [])
 
 data MkStar (p :: *) (x :: TyArr' p *)
 type instance MkStar p @@ x = *
-$(return [])
+-- $(return [])
 
 type instance (MkStar p) @@ x = *
-$(return [])
+-- $(return [])
 
 foo :: forall p x . MkStar p @@ x
 foo = undefined
@@ -30,7 +30,7 @@ data Sigma (p :: *) (r :: TyPi p (MkStar p)) :: * where
     forall (p :: *) (r :: TyPi p (MkStar p)) (a :: p) (b :: r @@@ a).
     Sing * p -> Sing (TyPi p (MkStar p)) r -> Sing p a -> Sing (r @@@ a) b
         -> Sigma p r
-$(return [])
+-- $(return [])
 
 data instance Sing Sigma (Sigma p r) x where
   SSigma ::