Fix #12369 by being more flexible with data insts

Previously, a data family's kind had to end in `Type`,
and data instances had to list all the type patterns for the
family. However, both of these restrictions were unnecessary:

- A data family's kind can usefully end in a kind variable `k`.
  See examples on #12369.

- A data instance need not list all patterns, much like how a
  GADT-style data declaration need not list all type parameters,
  when a kind signature is in place. This is useful, for example,
  here:

    data family Sing (a :: k)
    data instance Sing :: Bool -> Type where ...

This patch also improved a few error messages, as some error
plumbing had to be moved around.

See new Note [Arity of data families] in FamInstEnv for more
info.

test case: indexed-types/should_compile/T12369

8 files changed, 355 insertions, 183 deletions

diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 413751c440..86ade903ec 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -34,7 +34,7 @@ module TcHsSyn (
         emptyZonkEnv, mkEmptyZonkEnv,
         zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
         zonkCoToCo, zonkSigType,
-        zonkEvBinds,
+        zonkEvBinds, zonkTcEvBinds
   ) where
 
 #include "HsVersions.h"
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 01c9adba53..77fec02c6f 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -31,10 +31,12 @@ module TcHsType (
         tcHsLiftedType,   tcHsOpenType,
         tcHsLiftedTypeNC, tcHsOpenTypeNC,
         tcLHsType, tcCheckLHsType,
-        tcHsContext, tcLHsPredType, tcInferApps, tcInferArgs,
+        tcHsContext, tcLHsPredType, tcInferApps, tcTyApps,
         solveEqualities, -- useful re-export
 
-        kindGeneralize,
+        typeLevelMode, kindLevelMode,
+
+        kindGeneralize, checkExpectedKindX, instantiateTyUntilN,
 
         -- Sort-checking kinds
         tcLHsKindSig,
@@ -275,7 +277,7 @@ tcHsVectInst ty
     -- Ignoring the binders looks pretty dodgy to me
   = do { (cls, cls_kind) <- tcClass cls_name
        ; (applied_class, _res_kind)
-           <- tcInferApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
+           <- tcTyApps typeLevelMode hs_cls_ty (mkClassPred cls []) cls_kind tys
        ; case tcSplitTyConApp_maybe applied_class of
            Just (_tc, args) -> ASSERT( _tc == classTyCon cls )
                                return (cls, args)
@@ -320,7 +322,7 @@ tcHsOpenTypeNC   ty = do { ek <- newOpenTypeKind
 tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
 
 -- Like tcHsType, but takes an expected kind
-tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM Type
+tcCheckLHsType :: LHsType GhcRn -> Kind -> TcM TcType
 tcCheckLHsType hs_ty exp_kind
   = addTypeCtxt hs_ty $
     tc_lhs_type typeLevelMode hs_ty exp_kind
@@ -469,13 +471,13 @@ tc_infer_hs_type mode (HsAppTy ty1 ty2)
   = do { let (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
        ; (fun_ty', fun_kind) <- tc_infer_lhs_type mode fun_ty
        ; fun_kind' <- zonkTcType fun_kind
-       ; tcInferApps mode fun_ty fun_ty' fun_kind' arg_tys }
+       ; tcTyApps mode fun_ty fun_ty' fun_kind' arg_tys }
 tc_infer_hs_type mode (HsParTy t)     = tc_infer_lhs_type mode t
 tc_infer_hs_type mode (HsOpTy lhs (L loc_op op) rhs)
   | not (op `hasKey` funTyConKey)
   = do { (op', op_kind) <- tcTyVar mode op
        ; op_kind' <- zonkTcType op_kind
-       ; tcInferApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
+       ; tcTyApps mode (noLoc $ HsTyVar NotPromoted (L loc_op op)) op' op_kind' [lhs, rhs] }
 tc_infer_hs_type mode (HsKindSig ty sig)
   = do { sig' <- tc_lhs_kind (kindLevel mode) sig
        ; ty' <- tc_lhs_type mode ty sig'
@@ -785,42 +787,8 @@ bigConstraintTuple arity
        2 (text "Instead, use a nested tuple")
 
 ---------------------------
--- | Apply a type of a given kind to a list of arguments. This instantiates
--- invisible parameters as necessary. However, it does *not* necessarily
--- apply all the arguments, if the kind runs out of binders.
--- Never calls 'matchExpectedFunKind'; when the kind runs out of binders,
--- this stops processing.
--- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
--- These kinds should be used to instantiate invisible kind variables;
--- they come from an enclosing class for an associated type/data family.
--- This version will instantiate all invisible arguments left over after
--- the visible ones. Used only when typechecking type/data family patterns
--- (where we need to instantiate all remaining invisible parameters; for
--- example, consider @type family F :: k where F = Int; F = Maybe@. We
--- need to instantiate the @k@.)
-tcInferArgs :: Outputable fun
-            => fun                      -- ^ the function
-            -> [TyConBinder]            -- ^ function kind's binders
-            -> Maybe (VarEnv Kind)      -- ^ possibly, kind info (see above)
-            -> [LHsType GhcRn]          -- ^ args
-            -> TcM (TCvSubst, [TyBinder], [TcType], [LHsType GhcRn], Int)
-               -- ^ (instantiating subst, un-insted leftover binders,
-               --   typechecked args, untypechecked args, n)
-tcInferArgs fun tc_binders mb_kind_info args
-  = do { let binders = tyConBindersTyBinders tc_binders  -- UGH!
-       ; (subst, leftover_binders, args', leftovers, n)
-           <- tc_infer_args typeLevelMode fun binders mb_kind_info args 1
-        -- now, we need to instantiate any remaining invisible arguments
-       ; let (invis_bndrs, other_binders) = break isVisibleBinder leftover_binders
-       ; (subst', invis_args)
-           <- tcInstBinders subst mb_kind_info invis_bndrs
-       ; return ( subst'
-                , other_binders
-                , args' `chkAppend` invis_args
-                , leftovers, n ) }
-
 -- | See comments for 'tcInferArgs'. But this version does not instantiate
--- any remaining invisible arguments.
+-- any remaining invisible arguments. "RAE" update
 tc_infer_args :: Outputable fun
               => TcTyMode
               -> fun                      -- ^ the function
@@ -855,51 +823,80 @@ tc_infer_args mode orig_ty binders mb_kind_info orig_args n0
     go subst [] all_args n acc
       = return (subst, [], reverse acc, all_args, n)
 
--- | Applies a type to a list of arguments.
--- Always consumes all the arguments, using 'matchExpectedFunKind' as
--- necessary. If you wish to apply a type to a list of HsTypes, this is
--- your function.
--- Used for type-checking types only.
+-- | Apply a type of a given kind to a list of arguments. This instantiates
+-- invisible parameters as necessary. Always consumes all the arguments,
+-- using matchExpectedFunKind as necessary.
+-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.
+-- These kinds should be used to instantiate invisible kind variables;
+-- they come from an enclosing class for an associated type/data family.
 tcInferApps :: TcTyMode
+            -> Maybe (VarEnv Kind)  -- ^ Possibly, kind info (see above)
             -> LHsType GhcRn        -- ^ Function (for printing only)
             -> TcType               -- ^ Function (could be knot-tied)
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
-            -> TcM (TcType, TcKind) -- ^ (f args, result kind)
-tcInferApps mode orig_ty ty ki args = go [] ty ki args 1
+            -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
+tcInferApps mode mb_kind_info orig_ty ty ki args = go [] [] ty ki args 1
   where
-    go _acc_args fun fun_kind []   _ = return (fun, fun_kind)
-    go acc_args fun fun_kind args n
+    go _acc_hs_args acc_args fun fun_kind []   _ = return (fun, reverse acc_args, fun_kind)
+    go acc_hs_args acc_args fun fun_kind args n
       | let (binders, res_kind) = splitPiTys fun_kind
       , not (null binders)
       = do { (subst, leftover_binders, args', leftover_args, n')
-                <- tc_infer_args mode orig_ty binders Nothing args n
+                <- tc_infer_args mode orig_ty binders mb_kind_info args n
            ; let fun_kind' = substTyUnchecked subst $
                              mkPiTys leftover_binders res_kind
-           ; go (reverse (dropTail (length leftover_args) args) ++ acc_args)
+           ; go (reverse (dropTail (length leftover_args) args) ++ acc_hs_args)
+                (reverse args' ++ acc_args)
                 (mkNakedAppTys fun args') fun_kind' leftover_args n' }
 
-    go acc_args fun fun_kind (arg:args) n
-      = do { (co, arg_k, res_k) <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_args))
+    go acc_hs_args acc_args fun fun_kind (arg:args) n
+      = do { (co, arg_k, res_k) <- matchExpectedFunKind (mkHsAppTys orig_ty (reverse acc_hs_args))
                                                         fun_kind
            ; arg' <- addErrCtxt (funAppCtxt orig_ty arg n) $
                      tc_lhs_type mode arg arg_k
-           ; go (arg : acc_args)
+           ; go (arg : acc_hs_args) (arg' : acc_args)
                 (mkNakedAppTy (fun `mkNakedCastTy` co) arg')
                 res_k args (n+1) }
 
+-- | Applies a type to a list of arguments.
+-- Always consumes all the arguments, using 'matchExpectedFunKind' as
+-- necessary. If you wish to apply a type to a list of HsTypes, this is
+-- your function.
+-- Used for type-checking types only.
+tcTyApps :: TcTyMode
+         -> LHsType GhcRn        -- ^ Function (for printing only)
+         -> TcType               -- ^ Function (could be knot-tied)
+         -> TcKind               -- ^ Function kind (zonked)
+         -> [LHsType GhcRn]      -- ^ Args
+         -> TcM (TcType, TcKind) -- ^ (f args, result kind)
+tcTyApps mode orig_ty ty ki args
+  = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_ty ty ki args
+       ; return (ty', ki') }
+
 --------------------------
-checkExpectedKind :: HsType GhcRn         -- 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    -- a possibly-inst'ed, casted type :: exp_kind
+-- like checkExpectedKindX, but returns only the final type; convenient wrapper
+checkExpectedKind :: HsType GhcRn
+                  -> TcType
+                  -> TcKind
+                  -> TcKind
+                  -> TcM TcType
+checkExpectedKind hs_ty ty act exp = fstOf3 <$> checkExpectedKindX Nothing hs_ty ty act exp
+
+checkExpectedKindX :: Outputable hs_ty
+                   => Maybe (VarEnv Kind)  -- Possibly, instantiations for kind vars
+                   -> hs_ty                -- 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)
+    -- (an possibly-inst'ed, casted type :: exp_kind, 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
-checkExpectedKind hs_ty ty act_kind exp_kind
- = do { (ty', act_kind') <- instantiate ty act_kind exp_kind
+checkExpectedKindX mb_kind_env hs_ty ty act_kind exp_kind
+ = do { (ty', new_args, act_kind') <- instantiate ty act_kind exp_kind
       ; let origin = TypeEqOrigin { uo_actual   = act_kind'
                                   , uo_expected = exp_kind
                                   , uo_thing    = Just (ppr hs_ty)
@@ -909,7 +906,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind
                                           , ppr exp_kind
                                           , ppr co_k ])
       ; let result_ty = ty' `mkNakedCastTy` co_k
-      ; return result_ty }
+      ; return (result_ty, new_args, co_k) }
   where
     -- 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.
@@ -919,26 +916,29 @@ checkExpectedKind hs_ty ty act_kind exp_kind
                 -> TcKind    -- of this kind
                 -> TcKind   -- but expected to be of this one
                 -> TcM ( TcType   -- the inst'ed type
+                       , [TcType] -- the new args
                        , TcKind ) -- its new kind
     instantiate ty act_ki exp_ki
       = let (exp_bndrs, _) = splitPiTysInvisible exp_ki in
-        instantiateTyUntilN (length exp_bndrs) ty act_ki
+        instantiateTyUntilN mb_kind_env (length exp_bndrs) ty act_ki
 
 -- | 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@.)
-instantiateTyN :: Int                              -- ^ @n@
+instantiateTyN :: Maybe (VarEnv Kind)              -- ^ Predetermined instantiations
+                                                   -- (for assoc. type patterns)
+               -> Int                              -- ^ @n@
                -> TcType                           -- ^ the type
                -> [TyBinder] -> TcKind             -- ^ its kind
-               -> TcM (TcType, TcKind)             -- ^ The inst'ed type with kind
-instantiateTyN n ty bndrs inner_ki
+               -> TcM (TcType, [TcType], TcKind)   -- ^ The inst'ed type, new args, kind
+instantiateTyN mb_kind_env n ty bndrs inner_ki
   = let   -- NB: splitAt is forgiving with invalid numbers
         (inst_bndrs, leftover_bndrs) = splitAt n bndrs
         ki          = mkPiTys bndrs inner_ki
         empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ki))
     in
-    if n <= 0 then return (ty, ki) else
-    do { (subst, inst_args) <- tcInstBinders empty_subst Nothing inst_bndrs
+    if n <= 0 then return (ty, [], ki) else
+    do { (subst, inst_args) <- tcInstBinders empty_subst mb_kind_env inst_bndrs
        ; let rebuilt_ki = mkPiTys leftover_bndrs inner_ki
              ki'        = substTy subst rebuilt_ki
        ; traceTc "instantiateTyN" (vcat [ ppr ty <+> dcolon <+> ppr ki
@@ -946,18 +946,20 @@ instantiateTyN n ty bndrs inner_ki
                                         , ppr subst
                                         , ppr rebuilt_ki
                                         , ppr ki' ])
-       ; return (mkNakedAppTys ty inst_args, ki') }
+       ; return (mkNakedAppTys ty inst_args, inst_args, ki') }
 
 -- | Instantiate a type to have at most @n@ invisible arguments.
-instantiateTyUntilN :: Int         -- ^ @n@
+instantiateTyUntilN :: Maybe (VarEnv Kind)   -- ^ Possibly, instantiations for vars
+                    -> Int         -- ^ @n@
                     -> TcType      -- ^ the type
                     -> TcKind      -- ^ its kind
-                    -> TcM (TcType, TcKind)   -- ^ The inst'ed type with kind
-instantiateTyUntilN n ty ki
+                    -> TcM (TcType, [TcType], TcKind)   -- ^ The inst'ed type, new args,
+                                                        -- final kind
+instantiateTyUntilN mb_kind_env n ty ki
   = let (bndrs, inner_ki) = splitPiTysInvisible ki
         num_to_inst       = length bndrs - n
     in
-    instantiateTyN num_to_inst ty bndrs inner_ki
+    instantiateTyN mb_kind_env num_to_inst ty bndrs inner_ki
 
 ---------------------------
 tcHsContext :: LHsContext GhcRn -> TcM [PredType]
@@ -1039,8 +1041,8 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
            ; return (ty, tc_kind) }
 
       | otherwise
-      = do { (tc_ty, kind) <- instantiateTyN (length (tyConBinders tc_tc))
-                                             ty tc_kind_bndrs tc_inner_ki
+      = do { (tc_ty, _, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
+                                                ty tc_kind_bndrs tc_inner_ki
            -- tc and tc_ty must not be traced here, because that would
            -- force the evaluation of a potentially knot-tied variable (tc),
            -- and the typechecker would hang, as per #11708
@@ -1771,17 +1773,22 @@ tcTyClTyVars tycon_name thing_inside
          thing_inside binders res_kind }
 
 -----------------------------------
-tcDataKindSig :: Kind -> TcM ([TyConBinder], Kind)
+tcDataKindSig :: Bool  -- ^ Do we require the result to be *?
+              -> Kind -> TcM ([TyConBinder], Kind)
 -- GADT decls can have a (perhaps partial) kind signature
 --      e.g.  data T :: * -> * -> * where ...
 -- This function makes up suitable (kinded) type variables for
--- the argument kinds, and checks that the result kind is indeed *.
+-- the argument kinds, and checks that the result kind is indeed * if requested.
+-- (Otherwise, checks to make sure that the result kind is either * or a type variable.)
+-- See Note [Arity of data families] in FamInstEnv for more info.
 -- We use it also to make up argument type variables for for data instances.
 -- Never emits constraints.
 -- Returns the new TyVars, the extracted TyBinders, and the new, reduced
 -- result kind (which should always be Type or a synonym thereof)
-tcDataKindSig kind
-  = do  { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
+tcDataKindSig check_for_type kind
+  = do  { checkTc (isLiftedTypeKind res_kind || (not check_for_type &&
+                                                 isJust (tcGetCastedTyVar_maybe res_kind)))
+                  (badKindSig check_for_type kind)
         ; span <- getSrcSpanM
         ; us   <- newUniqueSupply
         ; rdr_env <- getLocalRdrEnv
@@ -1801,9 +1808,11 @@ tcDataKindSig kind
   where
     (tv_bndrs, res_kind) = splitPiTys kind
 
-badKindSig :: Kind -> SDoc
-badKindSig kind
- = hang (text "Kind signature on data type declaration has non-* return kind")
+badKindSig :: Bool -> Kind -> SDoc
+badKindSig check_for_type kind
+ = hang (sep [ text "Kind signature on data type declaration has non-*"
+             , (if check_for_type then empty else text "and non-variable") <+>
+               text "return kind" ])
         2 (ppr kind)
 
 {-
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 022668b470..703089ddc6 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -638,8 +638,9 @@ tcDataFamInstDecl mb_clsinfo
        ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
 
          -- Kind check type patterns
+       ; let mb_kind_env = thdOf3 <$> mb_clsinfo
        ; tcFamTyPats (famTyConShape fam_tc) mb_clsinfo pats
-                     (kcDataDefn (unLoc fam_tc_name) pats defn) $
+                     (kcDataDefn mb_kind_env (unLoc fam_tc_name) pats defn) $
              \tvs pats res_kind ->
     do { stupid_theta <- solveEqualities $ tcHsContext ctxt
 
@@ -655,17 +656,27 @@ tcDataFamInstDecl mb_clsinfo
        ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
        ; axiom_name  <- newFamInstAxiomName fam_tc_name [pats']
 
+         -- Deal with any kind signature.
+         -- See also Note [Arity of data families] in FamInstEnv
+       ; (extra_tcbs, final_res_kind) <- tcDataKindSig True res_kind'
+
        ; let (eta_pats, etad_tvs) = eta_reduce pats'
              eta_tvs              = filterOut (`elem` etad_tvs) tvs'
+                 -- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced
+
              full_tvs             = eta_tvs ++ etad_tvs
                  -- Put the eta-removed tyvars at the end
                  -- Remember, tvs' is in arbitrary order (except kind vars are
                  -- first, so there is no reason to suppose that the etad_tvs
                  -- (obtained from the pats) are at the end (Trac #11148)
-             orig_res_ty          = mkTyConApp fam_tc pats'
+
+             extra_pats           = map (mkTyVarTy . binderVar) extra_tcbs
+             all_pats             = pats' `chkAppend` extra_pats
+             orig_res_ty          = mkTyConApp fam_tc all_pats
 
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
-           do { let ty_binders = mkTyConBindersPreferAnon full_tvs liftedTypeKind
+           do { let ty_binders = mkTyConBindersPreferAnon full_tvs res_kind'
+                                 `chkAppend` extra_tcbs
               ; data_cons <- tcConDecls rec_rep_tc
                                         (ty_binders, orig_res_ty) cons
               ; tc_rhs <- case new_or_data of
@@ -676,10 +687,10 @@ tcDataFamInstDecl mb_clsinfo
               ; let axiom  = mkSingleCoAxiom Representational
                                              axiom_name eta_tvs [] fam_tc eta_pats
                                              (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
-                    parent = DataFamInstTyCon axiom fam_tc pats'
+                    parent = DataFamInstTyCon axiom fam_tc all_pats
 
 
-                      -- NB: Use the full_tvs from the pats. See bullet toward
+                      -- NB: Use the full ty_binders from the pats. See bullet toward
                       -- the end of Note [Data type families] in TyCon
                     rep_tc   = mkAlgTyCon rep_tc_name
                                           ty_binders liftedTypeKind
@@ -697,10 +708,10 @@ 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)
-       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats'
+       ; checkValidFamPats mb_clsinfo fam_tc tvs' [] pats' extra_pats
 
          -- Result kind must be '*' (otherwise, we have too few patterns)
-       ; checkTc (isLiftedTypeKind res_kind') $
+       ; checkTc (isLiftedTypeKind final_res_kind) $
          tooFewParmsErr (tyConArity fam_tc)
 
        ; checkValidTyCon rep_tc
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 6addbf2c38..77c5c232a1 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -33,7 +33,8 @@ import TcTyDecls
 import TcClassDcl
 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
 import TcDeriv (DerivInfo)
-import TcUnify
+import TcEvidence  ( tcCoercionKind, isEmptyTcEvBinds )
+import TcUnify     ( checkConstraints )
 import TcHsType
 import TcMType
 import TysWiredIn ( unitTy )
@@ -61,6 +62,7 @@ import Outputable
 import Maybes
 import Unify
 import Util
+import Pair
 import SrcLoc
 import ListSetOps
 import DynFlags
@@ -826,7 +828,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
   = tcTyClTyVars tc_name $ \ binders res_kind -> do
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
-  ; (extra_binders, real_res_kind) <- tcDataKindSig res_kind
+  ; (extra_binders, real_res_kind) <- tcDataKindSig False res_kind
   ; tc_rep_name <- newTyConRepName tc_name
   ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
                               real_res_kind
@@ -870,7 +872,11 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
            Just eqns -> do {
 
          -- Process the equations, creating CoAxBranches
-       ; let fam_tc_shape = (tc_name, length $ hsQTvExplicit tvs, binders, res_kind)
+       ; let fam_tc_shape = FamTyConShape { fs_name     = tc_name
+                                          , fs_arity    = length $ hsQTvExplicit tvs
+                                          , fs_flavor   = TypeFam
+                                          , fs_binders  = binders
+                                          , fs_res_kind = res_kind }
 
        ; branches <- mapM (tcTyFamInstEqn fam_tc_shape Nothing) eqns
          -- Do not attempt to drop equations dominated by earlier
@@ -970,7 +976,7 @@ tcDataDefn roles_info
          (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
                      , dd_ctxt = ctxt, dd_kindSig = mb_ksig
                      , dd_cons = cons })
- =  do { (extra_bndrs, real_res_kind) <- tcDataKindSig res_kind
+ =  do { (extra_bndrs, real_res_kind) <- tcDataKindSig True res_kind
        ; let final_bndrs  = tycon_binders `chkAppend` extra_bndrs
              roles        = roles_info tc_name
 
@@ -1090,7 +1096,8 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
     setSrcSpan loc $
     tcAddFamInstCtxt (text "default type instance") tc_name $
     do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
-       ; let shape@(fam_tc_name, fam_arity, _, _) = famTyConShape fam_tc
+       ; let shape@(FamTyConShape { fs_name = fam_tc_name
+                                  , fs_arity = fam_arity }) = famTyConShape fam_tc
 
        -- Kind of family check
        ; ASSERT( fam_tc_name == tc_name )
@@ -1104,12 +1111,19 @@ tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
        ; let pats = HsIB { hsib_vars = imp_vars ++ map hsLTyVarName exp_vars
                          , hsib_body = map hsLTyVarBndrToType exp_vars
                          , hsib_closed = False } -- this field is ignored, anyway
+
           -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
           -- the LHsQTyVars used for declaring a tycon, but the names here
           -- are different.
+
+          -- You might think we should pass in some ClsInstInfo, as we're looking
+          -- 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.
        ; (pats', rhs_ty)
            <- tcFamTyPats shape Nothing pats
-              (discardResult . tcCheckLHsType rhs) $ \tvs pats rhs_kind ->
+              (kcTyFamEqnRhs Nothing (mkFamApp fam_tc_name pats) rhs) $
+              \tvs pats rhs_kind ->
               do { rhs_ty <- solveEqualities $
                              tcCheckLHsType rhs rhs_kind
 
@@ -1150,7 +1164,7 @@ proper tcMatchTys here.)  -}
 
 -------------------------
 kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn GhcRn -> TcM ()
-kcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_)
+kcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name })
     (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
                      , tfe_pats  = pats
                      , tfe_rhs   = hs_ty }))
@@ -1159,20 +1173,47 @@ kcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_)
                  (wrongTyFamName fam_tc_name eqn_tc_name)
        ; discardResult $
          tc_fam_ty_pats fam_tc_shape Nothing -- not an associated type
-                        pats (discardResult . (tcCheckLHsType hs_ty)) }
+                        pats (kcTyFamEqnRhs Nothing (mkFamApp fam_tc_name pats) hs_ty) }
+
+-- Infer the kind of the type on the RHS of a type family eqn. Then use
+-- this kind to check the kind of the LHS of the equation. This is useful
+-- as the callback to tc_fam_ty_pats and the kind-checker to
+-- tcFamTyPats.
+kcTyFamEqnRhs :: Maybe ClsInstInfo
+              -> HsType GhcRn         -- ^ Eqn LHS (for errors only)
+              -> LHsType GhcRn        -- ^ Eqn RHS
+              -> TcKind               -- ^ Inferred kind of left-hand side
+              -> TcM ([TcType], TcKind)  -- ^ New pats, inst'ed kind of left-hand side
+kcTyFamEqnRhs mb_clsinfo lhs_ty rhs_hs_ty lhs_ki
+  = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
+         (_lhs_ty', new_pats, insted_lhs_ki)
+           <- instantiateTyUntilN mb_kind_env 0 bogus_ty lhs_ki
+       ; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki
+
+       ; return (new_pats, insted_lhs_ki) }
+  where
+    mb_kind_env = thdOf3 <$> mb_clsinfo
+
+    bogus_ty = pprPanic "kcTyFamEqnRhs" (ppr lhs_ty $$ ppr rhs_hs_ty)
+
+  -- useful when we need an HsType GhcRn for error messages
+  -- not exported from this module
+mkFamApp :: Name -> HsTyPats GhcRn -> HsType GhcRn
+mkFamApp fam_tc_name (HsIB { hsib_body = pats })
+  = unLoc $ mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_tc_name)) pats
 
 tcTyFamInstEqn :: FamTyConShape -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
                -> TcM CoAxBranch
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
-tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
+tcTyFamInstEqn fam_tc_shape@(FamTyConShape { fs_name = fam_tc_name }) mb_clsinfo
     (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
                      , tfe_pats  = pats
                      , tfe_rhs   = hs_ty }))
   = ASSERT( fam_tc_name == eqn_tc_name )
     setSrcSpan loc $
     tcFamTyPats fam_tc_shape mb_clsinfo pats
-                (discardResult . (tcCheckLHsType hs_ty)) $
+                (kcTyFamEqnRhs mb_clsinfo (mkFamApp fam_tc_name pats) hs_ty) $
                     \tvs pats res_kind ->
     do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
 
@@ -1185,25 +1226,62 @@ tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_,_) mb_clsinfo
                               (map (const Nominal) tvs')
                               loc) }
 
-kcDataDefn :: Name                -- ^ the family name, for error msgs only
+kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
+                                  -- (associated types only)
+           -> Name                -- ^ the family name, for error msgs only
            -> HsTyPats GhcRn      -- ^ the patterns, for error msgs only
            -> HsDataDefn GhcRn    -- ^ the RHS
-           -> TcKind              -- ^ the expected kind
-           -> TcM ()
+           -> TcKind              -- ^ the kind of the tycon applied to pats
+           -> TcM ([TcType], TcKind)
+             -- ^ the kind signature might force instantiation
+             -- of the tycon; this returns any extra args and the inst'ed kind
+             -- See Note [Instantiating a family tycon]
 -- Used for 'data instance' only
 -- Ordinary 'data' is handled by kcTyClDec
-kcDataDefn fam_name (HsIB { hsib_body = pats })
+kcDataDefn mb_kind_env fam_name pats
            (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
   = do  { _ <- tcHsContext ctxt
         ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
           -- See Note [Failing early in kcDataDefn]
-        ; discardResult $
-          case mb_kind of
-            Nothing -> unifyKind (Just hs_ty_pats) res_k liftedTypeKind
-            Just k  -> do { k' <- tcLHsKindSig k
-                          ; unifyKind (Just hs_ty_pats) res_k k' } }
+        ; exp_res_kind <- case mb_kind of
+            Nothing -> return liftedTypeKind
+            Just k  -> tcLHsKindSig k
+
+          -- The expected type might have a forall at the type. Normally, we
+          -- can't skolemise in kinds because we don't have type-level lambda.
+          -- But here, we're at the top-level of an instance declaration, so
+          -- we actually have a place to put the regeneralised variables.
+          -- Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
+          -- Examples in indexed-types/should_compile/T12369
+        ; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind
+
+        ; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise
+            -- we don't need to do anything substantive with the tvs' because the
+            -- quantifyTyVars in tcFamTyPats will catch them.
+
+        ; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind
+              tv_prs          = zip (map tyVarName tvs_to_skolemise) tvs'
+              skol_info       = SigSkol InstDeclCtxt exp_res_kind tv_prs
+
+        ; (ev_binds, (_, new_args, co))
+            <- solveEqualities $
+               checkConstraints skol_info tvs' [] $
+               checkExpectedKindX mb_kind_env hs_fam_app
+                                  bogus_ty res_k inner_res_kind'
+
+        ; let Pair lhs_ki rhs_ki = tcCoercionKind co
+
+        ; when debugIsOn $
+          do { (_, ev_binds) <- zonkTcEvBinds emptyZonkEnv ev_binds
+             ; MASSERT( isEmptyTcEvBinds ev_binds )
+             ; lhs_ki <- zonkTcType lhs_ki
+             ; rhs_ki <- zonkTcType rhs_ki
+             ; MASSERT( lhs_ki `tcEqType` rhs_ki ) }
+
+        ; return (new_args, lhs_ki) }
   where
-    hs_ty_pats = unLoc $ mkHsAppTys (noLoc $ HsTyVar NotPromoted (noLoc fam_name)) pats
+    bogus_ty   = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats)
+    hs_fam_app = mkFamApp fam_name pats
 
 {-
 Kind check type patterns and kind annotate the embedded type variables.
@@ -1231,6 +1309,28 @@ The type FamTyConShape gives just enough information to do the job.
 
 See also Note [tc_fam_ty_pats vs tcFamTyPats]
 
+Note [Instantiating a family tycon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's possible that kind-checking the result of a family tycon applied to
+its patterns will instantiate the tycon further. For example, we might
+have
+
+  type family F :: k where
+    F = Int
+    F = Maybe
+
+After checking (F :: forall k. k) (with no visible patterns), we still need
+to instantiate the k. With data family instances, this problem can be even
+more intricate, due to Note [Arity of data families] in FamInstEnv. See
+indexed-types/should_compile/T12369 for an example.
+
+So, the kind-checker must return both the new args (that is, Type
+(Type -> Type) for the equations above) and the instantiated kind.
+
+Because we don't need this information in the kind-checking phase of
+checking closed type families, we don't require these extra pieces of
+information in tc_fam_ty_pats. See also Note [tc_fam_ty_pats vs tcFamTyPats].
+
 Note [Failing early in kcDataDefn]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
@@ -1245,22 +1345,31 @@ two bad things could happen:
 -}
 
 -----------------
-type FamTyConShape = (Name, Arity, [TyConBinder], Kind)
+data TypeOrDataFamily = TypeFam | DataFam
+data FamTyConShape = FamTyConShape { fs_name :: Name
+                                   , fs_arity :: Arity
+                                   , fs_flavor :: TypeOrDataFamily
+                                   , fs_binders :: [TyConBinder]
+                                   , fs_res_kind :: Kind }
   -- See Note [Type-checking type patterns]
 
 famTyConShape :: TyCon -> FamTyConShape
 famTyConShape fam_tc
-  = ( tyConName fam_tc
-    , length $ filterOutInvisibleTyVars fam_tc (tyConTyVars fam_tc)
-    , tyConBinders fam_tc
-    , tyConResKind fam_tc )
+  = FamTyConShape { fs_name     = tyConName fam_tc
+                  , fs_arity    = length $ filterOutInvisibleTyVars fam_tc (tyConTyVars fam_tc)
+                  , fs_flavor   = flav
+                  , fs_binders  = tyConBinders fam_tc
+                  , fs_res_kind = tyConResKind fam_tc }
+  where
+    flav
+      | isTypeFamilyTyCon fam_tc = TypeFam
+      | otherwise                = DataFam
 
 tc_fam_ty_pats :: FamTyConShape
                -> Maybe ClsInstInfo
                -> HsTyPats GhcRn      -- Patterns
-               -> (TcKind -> TcM ())  -- Kind checker for RHS
-                                      -- result is ignored
-               -> TcM ([Type], Kind)
+               -> (TcKind -> TcM r)   -- Kind checker for RHS
+               -> TcM ([Type], r)     -- Returns the type-checked patterns
 -- Check the type patterns of a type or data family instance
 --     type instance F <pat1> <pat2> = <type>
 -- The 'tyvars' are the free type variables of pats
@@ -1272,43 +1381,60 @@ tc_fam_ty_pats :: FamTyConShape
 -- In that case, the type variable 'a' will *already be in scope*
 -- (and, if C is poly-kinded, so will its kind parameter).
 
-tc_fam_ty_pats (name, _, binders, res_kind) mb_clsinfo
-               (HsIB { hsib_body = arg_pats, hsib_vars = tv_names })
+tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity
+                              , fs_flavor = flav, fs_binders = binders
+                              , fs_res_kind = res_kind })
+               mb_clsinfo (HsIB { hsib_body = arg_pats, hsib_vars = tv_names })
                kind_checker
-  = do { -- Kind-check and quantify
+  = do { -- First, check the arity.
+         -- If we wait until validity checking, we'll get kind
+         -- errors below when an arity error will be much easier to
+         -- understand.
+         let should_check_arity
+               | TypeFam <- flav = True
+                  -- check for data families that don't have any polymorphism
+                  -- why not always? See [Arity of data families] in FamInstEnv
+               | otherwise       = isEmptyVarSet (tyCoVarsOfType res_kind)
+
+       ; when should_check_arity $
+         checkTc (arg_pats `lengthIs` arity) $
+         wrongNumberOfParmsErr (arity - count isInvisibleTyConBinder binders)
+                      -- report only explicit arguments
+
+         -- Kind-check and quantify
          -- See Note [Quantifying over family patterns]
-         (_, (insted_res_kind, typats)) <- tcImplicitTKBndrs tv_names $
-         do { (insting_subst, _leftover_binders, args, leftovers, n)
-                <- tcInferArgs name binders (thdOf3 <$> mb_clsinfo) arg_pats
-            ; case leftovers of
-                hs_ty:_ -> addErrTc $ too_many_args hs_ty n
-                _       -> return ()
-              -- don't worry about leftover_binders; TcValidity catches them
-
-            ; let insted_res_kind = substTyUnchecked insting_subst res_kind
-            ; kind_checker insted_res_kind
-            ; return ((insted_res_kind, args), emptyVarSet) }
-
-       ; return (typats, insted_res_kind) }
-  where
-    too_many_args hs_ty n
-      = hang (text "Too many parameters to" <+> ppr name <> colon)
-           2 (vcat [ ppr hs_ty <+> text "is unexpected;"
-                   , text (if n == 1 then "expected" else "expected only") <+>
-                     speakNOf (n-1) (text "parameter") ])
+       ; (_, result) <- tcImplicitTKBndrs tv_names $
+         do { let loc          = nameSrcSpan name
+                  lhs_fun      = L loc (HsTyVar NotPromoted (L loc name))
+                  bogus_fun_ty = pprPanic "tc_fam_ty_pats" (ppr name $$ ppr arg_pats)
+                  fun_kind     = mkTyConKind binders res_kind
+                  mb_kind_env  = thdOf3 <$> mb_clsinfo
+
+            ; (_, args, res_kind_out)
+                <- tcInferApps typeLevelMode mb_kind_env
+                               lhs_fun bogus_fun_ty fun_kind arg_pats
+
+            ; stuff <- kind_checker res_kind_out
+
+            ; return ((args, stuff), emptyVarSet) }
+
+       ; return result }
 
 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
 tcFamTyPats :: FamTyConShape
             -> Maybe ClsInstInfo
             -> HsTyPats GhcRn        -- patterns
-            -> (TcKind -> TcM ())    -- kind-checker for RHS
+            -> (TcKind -> TcM ([TcType], TcKind))
+                -- kind-checker for RHS
+                -- See Note [Instantiating a family tycon]
             -> (   [TcTyVar]         -- Kind and type variables
                 -> [TcType]          -- Kind and type arguments
                 -> TcKind
                 -> TcM a)            -- NB: You can use solveEqualities here.
             -> TcM a
-tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
-  = do { (typats, res_kind)
+tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo pats
+            kind_checker thing_inside
+  = do { (typats, (more_typats, res_kind))
             <- solveEqualities $  -- See Note [Constraints in patterns]
                tc_fam_ty_pats fam_shape mb_clsinfo pats kind_checker
 
@@ -1333,7 +1459,8 @@ tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
             -- them into skolems, so that we don't subsequently
             -- replace a meta kind var with (Any *)
             -- Very like kindGeneralize
-       ; vars  <- zonkTcTypesAndSplitDepVars typats
+       ; let all_pats = typats `chkAppend` more_typats
+       ; vars  <- zonkTcTypesAndSplitDepVars all_pats
        ; qtkvs <- quantifyTyVars emptyVarSet vars
 
        ; MASSERT( isEmptyVarSet $ coVarsOfTypes typats )
@@ -1341,14 +1468,14 @@ tcFamTyPats fam_shape@(name,_,_,_) mb_clsinfo pats kind_checker thing_inside
            -- above would fail. TODO (RAE): Update once the solveEqualities
            -- bit is cleverer.
 
-       ; traceTc "tcFamTyPats" (ppr name $$ ppr typats $$ ppr qtkvs)
+       ; traceTc "tcFamTyPats" (ppr name $$ ppr all_pats $$ ppr qtkvs)
             -- Don't print out too much, as we might be in the knot
 
        ; tcExtendTyVarEnv qtkvs $
             -- Extend envt with TcTyVars not TyVars, because the
             -- kind checking etc done by thing_inside does not expect
             -- to encounter TyVars; it expects TcTyVars
-         thing_inside qtkvs typats res_kind }
+         thing_inside qtkvs all_pats res_kind }
 
 {-
 Note [Constraints in patterns]
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 4f7507745e..d896f4118f 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -56,7 +56,6 @@ import Util
 import ListSetOps
 import SrcLoc
 import Outputable
-import BasicTypes
 import Module
 import Unique      ( mkAlphaTyVarUnique )
 import qualified GHC.LanguageExtensions as LangExt
@@ -1684,7 +1683,7 @@ checkValidTyFamEqn :: Maybe ClsInstInfo
                    -> TcM ()
 checkValidTyFamEqn mb_clsinfo fam_tc tvs cvs typats rhs loc
   = setSrcSpan loc $
-    do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats
+    do { checkValidFamPats mb_clsinfo fam_tc tvs cvs typats []
 
          -- The argument patterns, and RHS, are all boxed tau types
          -- E.g  Reject type family F (a :: k1) :: k2
@@ -1722,7 +1721,10 @@ checkFamInstRhs lhsTys famInsts
         what    = text "type family application" <+> quotes (pprType (TyConApp tc tys))
         bad_tvs = fvTypes tys \\ fvs
 
-checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
+checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar]
+                  -> [Type]   -- ^ patterns the user wrote
+                  -> [Type]   -- ^ "extra" patterns from a data instance kind sig
+                  -> TcM ()
 -- Patterns in a 'type instance' or 'data instance' decl should
 -- a) contain no type family applications
 --    (vanilla synonyms are fine, though)
@@ -1730,29 +1732,16 @@ checkValidFamPats :: Maybe ClsInstInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type]
 --    e.g. we disallow (Trac #7536)
 --         type T a = Int
 --         type instance F (T a) = a
--- c) Have the right number of patterns
--- d) For associated types, are consistently instantiated
-checkValidFamPats mb_clsinfo fam_tc tvs cvs ty_pats
-  = do { -- A family instance must have exactly the same number of type
-         -- parameters as the family declaration.  You can't write
-         --     type family F a :: * -> *
-         --     type instance F Int y = y
-         -- because then the type (F Int) would be like (\y.y)
-         checkTc (ty_pats `lengthIs` fam_arity) $
-           wrongNumberOfParmsErr (fam_arity - count isInvisibleTyConBinder fam_bndrs)
-             -- report only explicit arguments
-
-       ; mapM_ checkValidTypePat ty_pats
-
-       ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes ty_pats) (tvs ++ cvs)
-       ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs ty_pats)
+-- c) For associated types, are consistently instantiated
+checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats
+  = do { mapM_ checkValidTypePat user_ty_pats
 
-         -- Check that type patterns match the class instance head
-       ; checkConsistentFamInst mb_clsinfo fam_tc tvs ty_pats }
-  where
-     fam_arity = tyConArity fam_tc
-     fam_bndrs = tyConBinders fam_tc
+       ; let unbound_tcvs = filterOut (`elemVarSet` exactTyCoVarsOfTypes user_ty_pats)
+                                      (tvs ++ cvs)
+       ; checkTc (null unbound_tcvs) (famPatErr fam_tc unbound_tcvs user_ty_pats)
 
+         -- Check that type patterns match the class instance head
+       ; checkConsistentFamInst mb_clsinfo fam_tc tvs (user_ty_pats `chkAppend` extra_ty_pats) }
 
 checkValidTypePat :: Type -> TcM ()
 -- Used for type patterns in class instances,
@@ -1774,11 +1763,6 @@ isTyFamFree = null . tcTyFamInsts
 
 -- Error messages
 
-wrongNumberOfParmsErr :: Arity -> SDoc
-wrongNumberOfParmsErr exp_arity
-  = text "Number of parameters must match family declaration; expected"
-    <+> ppr exp_arity
-
 inaccessibleCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
 inaccessibleCoAxBranch fi_ax cur_branch
   = text "Type family instance equation is overlapped:" $$
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index 6d179a9a10..f40dabe3fd 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -125,8 +125,45 @@ data FamFlavor
   = SynFamilyInst         -- A synonym family
   | DataFamilyInst TyCon  -- A data family, with its representation TyCon
 
-{- Note [Eta reduction for data families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{-
+Note [Arity of data families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Data family instances might legitimately be over- or under-saturated.
+
+Under-saturation has two potential causes:
+ U1) Eta reduction. See Note [Eta reduction for data families].
+ U2) When the user has specified a return kind instead of written out patterns.
+     Example:
+
+       data family Sing (a :: k)
+       data instance Sing :: Bool -> Type
+
+     The data family tycon Sing has an arity of 2, the k and the a. But
+     the data instance has only one pattern, Bool (standing in for k).
+     This instance is equivalent to `data instance Sing (a :: Bool)`, but
+     without the last pattern, we have an under-saturated data family instance.
+     On its own, this example is not compelling enough to add support for
+     under-saturation, but U1 makes this feature more compelling.
+
+Over-saturation is also possible:
+  O1) If the data family's return kind is a type variable (see also #12369),
+      an instance might legitimately have more arguments than the family.
+      Example:
+
+        data family Fix :: (Type -> k) -> k
+        data instance Fix f = MkFix1 (f (Fix f))
+        data instance Fix f x = MkFix2 (f (Fix f x) x)
+
+      In the first instance here, the k in the data family kind is chosen to
+      be Type. In the second, it's (Type -> Type).
+
+      However, we require that any over-saturation is eta-reducible. That is,
+      we require that any extra patterns be bare unrepeated type variables;
+      see Note [Eta reduction for data families]. Accordingly, the FamInst
+      is never over-saturated.
+
+Note [Eta reduction for data families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this
    data family T a b :: *
    newtype instance T Int a = MkT (IO a) deriving( Monad )
@@ -156,7 +193,7 @@ See also Note [Newtype eta] in TyCon.
 
 Bottom line:
   For a FamInst with fi_flavour = DataFamilyInst rep_tc,
-  - fi_tvs may be shorter than tyConTyVars of rep_tc
+  - fi_tvs may be shorter than tyConTyVars of rep_tc.
   - fi_tys may be shorter than tyConArity of the family tycon
        i.e. LHS is unsaturated
   - fi_rhs will be (rep_tc fi_tvs)
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index d717ba66d3..403fc42b50 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -222,7 +222,10 @@ See also Note [Wrappers for data instance tycons] in MkId.hs
         DataFamInstTyCon T [Int] ax_ti
 
 * The axiom ax_ti may be eta-reduced; see
-  Note [Eta reduction for data family axioms] in TcInstDcls
+  Note [Eta reduction for data family axioms] in FamInstEnv
+
+* Data family instances may have a different arity than the data family.
+  See Note [Arity of data families] in FamInstEnv
 
 * The data constructor T2 has a wrapper (which is what the
   source-level "T2" invokes):
@@ -940,7 +943,8 @@ data AlgTyConFlav
           -- use the tyConTyVars of this TyCon
         TyCon   -- The family TyCon
         [Type]  -- Argument types (mentions the tyConTyVars of this TyCon)
-                -- Match in length the tyConTyVars of the family TyCon
+                -- No shorter in length than the tyConTyVars of the family TyCon
+                -- How could it be longer? See [Arity of data families] in FamInstEnv
 
         -- E.g.  data instance T [a] = ...
         -- gives a representation tycon:
@@ -961,7 +965,7 @@ okParent :: Name -> AlgTyConFlav -> Bool
 okParent _       (VanillaAlgTyCon {})            = True
 okParent _       (UnboxedAlgTyCon {})            = True
 okParent tc_name (ClassTyCon cls _)              = tc_name == tyConName (classTyCon cls)
-okParent _       (DataFamInstTyCon _ fam_tc tys) = tys `lengthIs` tyConArity fam_tc
+okParent _       (DataFamInstTyCon _ fam_tc tys) = tys `lengthAtLeast` tyConArity fam_tc
 
 isNoParent :: AlgTyConFlav -> Bool
 isNoParent (VanillaAlgTyCon {}) = True
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 16d3963764..da212bf5a3 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -988,7 +988,7 @@ piResultTy_maybe ty arg
 -- so we pay attention to efficiency, especially in the special case
 -- where there are no for-alls so we are just dropping arrows from
 -- a function type/kind.
-piResultTys :: Type -> [Type] -> Type
+piResultTys :: HasDebugCallStack => Type -> [Type] -> Type
 piResultTys ty [] = ty
 piResultTys ty orig_args@(arg:args)
   | Just ty' <- coreView ty