More wibbles to data families

Including fixing Trac #15817

7 files changed, 298 insertions, 164 deletions

diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index b7435e5b54..de4fd122b3 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -74,6 +74,7 @@ import Class
 import Name
 import PrelNames
 import Var
+import VarSet( emptyVarSet )
 import Outputable
 import Util
 import BasicTypes
@@ -1487,7 +1488,7 @@ buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
   = mkAlgTyCon tc_name binders liftedTypeKind roles cType stupid_theta
                rhs parent gadt_syn
   where
-    binders = mkTyConBindersPreferAnon ktvs liftedTypeKind
+    binders = mkTyConBindersPreferAnon ktvs emptyVarSet
 
 buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind   -- ^ /result/ kind
               -> [Role] -> KnotTied Type -> TyCon
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 5e821883ad..4a4d49b81e 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -27,8 +27,8 @@ module TcHsType (
         ContextKind(..),
 
                 -- Type checking type and class decls
-        kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
-        tcDataKindSig,
+        kcLookupTcTyCon, bindTyClTyVars,
+        etaExpandAlgTyCon, tcbVisibilities,
 
           -- tyvars
         zonkAndScopedSort,
@@ -79,7 +79,7 @@ import TcHsSyn
 import TcErrors ( reportAllUnsolved )
 import TcType
 import Inst   ( tcInstTyBinders, tcInstTyBinder )
-import TyCoRep( TyCoBinder(..), TyBinder )  -- Used in tcDataKindSig
+import TyCoRep( TyCoBinder(..), TyBinder )  -- Used in etaExpandAlgTyCon
 import Type
 import Coercion
 import RdrName( lookupLocalRdrOcc )
@@ -1890,6 +1890,35 @@ tcHsQTyVarBndr _ new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
 tcHsQTyVarBndr _ _ (XTyVarBndr _) = panic "tcHsTyVarBndr"
 
 
+--------------------------------------
+-- Binding type/class variables in the
+-- kind-checking and typechecking phases
+--------------------------------------
+
+bindTyClTyVars :: Name
+               -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
+-- ^ Used for the type variables of a type or class decl
+-- in the "kind checking" and "type checking" pass,
+-- but not in the initial-kind run.
+bindTyClTyVars tycon_name thing_inside
+  = do { tycon <- kcLookupTcTyCon tycon_name
+       ; let scoped_prs = tcTyConScopedTyVars tycon
+             res_kind   = tyConResKind tycon
+             binders    = tyConBinders tycon
+       ; traceTc "bindTyClTyVars" (ppr tycon_name <+> ppr binders)
+       ; tcExtendNameTyVarEnv scoped_prs $
+         thing_inside binders res_kind }
+
+-- getInitialKind has made a suitably-shaped kind for the type or class
+-- Look it up in the local environment. This is used only for tycons
+-- that we're currently type-checking, so we're sure to find a TcTyCon.
+kcLookupTcTyCon :: Name -> TcM TcTyCon
+kcLookupTcTyCon nm
+  = do { tc_ty_thing <- tcLookup nm
+       ; return $ case tc_ty_thing of
+           ATcTyCon tc -> tc
+           _           -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
+
 
 {- *********************************************************************
 *                                                                      *
@@ -2020,60 +2049,10 @@ Hence using zonked_kinds when forming tvs'.
 
 -}
 
---------------------
--- getInitialKind has made a suitably-shaped kind for the type or class
--- Look it up in the local environment. This is used only for tycons
--- that we're currently type-checking, so we're sure to find a TcTyCon.
-kcLookupTcTyCon :: Name -> TcM TcTyCon
-kcLookupTcTyCon nm
-  = do { tc_ty_thing <- tcLookup nm
-       ; return $ case tc_ty_thing of
-           ATcTyCon tc -> tc
-           _           -> pprPanic "kcLookupTcTyCon" (ppr tc_ty_thing) }
-
------------------------
--- | Bring tycon tyvars into scope. This is used during the "kind-checking"
--- pass in TcTyClsDecls. (Never in getInitialKind, never in the
--- "type-checking"/desugaring pass.)
--- Never emits constraints, though the thing_inside might.
-kcTyClTyVars :: Name -> TcM a -> TcM a
-kcTyClTyVars tycon_name thing_inside
-  = do { tycon <- kcLookupTcTyCon tycon_name
-       ; tcExtendNameTyVarEnv (tcTyConScopedTyVars tycon) $ thing_inside }
-
-tcTyClTyVars :: Name
-             -> ([TyConBinder] -> Kind -> TcM a) -> TcM a
--- ^ Used for the type variables of a type or class decl
--- on the second full pass (type-checking/desugaring) in TcTyClDecls.
--- This is *not* used in the initial-kind run, nor in the "kind-checking" pass.
--- Accordingly, everything passed to the continuation is fully zonked.
---
--- (tcTyClTyVars T [a,b] thing_inside)
---   where T : forall k1 k2 (a:k1 -> *) (b:k1). k2 -> *
---   calls thing_inside with arguments
---      [k1,k2,a,b] [k1:*, k2:*, Anon (k1 -> *), Anon k1] (k2 -> *)
---   having also extended the type environment with bindings
---   for k1,k2,a,b
---
--- Never emits constraints.
---
--- The LHsTyVarBndrs is always user-written, and the full, generalised
--- kind of the tycon is available in the local env.
-tcTyClTyVars tycon_name thing_inside
-  = do { tycon <- kcLookupTcTyCon tycon_name
-       ; let scoped_prs = tcTyConScopedTyVars tycon
-             res_kind   = tyConResKind tycon
-             binders    = tyConBinders tycon
-
-       ; traceTc "tcTyClTyVars" (ppr tycon_name <+> ppr binders)
-       ; pushTcLevelM_                   $
-         tcExtendNameTyVarEnv scoped_prs $
-         thing_inside binders res_kind }
-
 -----------------------------------
-tcDataKindSig :: [TyConBinder]
-              -> Kind
-              -> TcM ([TyConBinder], Kind)
+etaExpandAlgTyCon :: [TyConBinder]
+                  -> Kind
+                  -> TcM ([TyConBinder], Kind)
 -- GADT decls can have a (perhaps partial) kind signature
 --      e.g.  data T a :: * -> * -> * where ...
 -- This function makes up suitable (kinded) TyConBinders for the
@@ -2082,7 +2061,7 @@ tcDataKindSig :: [TyConBinder]
 -- Never emits constraints.
 -- It's a little trickier than you might think: see
 -- Note [TyConBinders for the result kind signature of a data type]
-tcDataKindSig tc_bndrs kind
+etaExpandAlgTyCon tc_bndrs kind
   = do  { loc     <- getSrcSpanM
         ; uniqs   <- newUniqueSupply
         ; rdr_env <- getLocalRdrEnv
@@ -2126,13 +2105,37 @@ badKindSig check_for_type kind
                text "return kind" ])
         2 (ppr kind)
 
+tcbVisibilities :: TyCon -> [Type] -> [TyConBndrVis]
+-- Result is in 1-1 correpondence with orig_args
+tcbVisibilities tc orig_args
+  = go (tyConKind tc) init_subst orig_args
+  where
+    init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes orig_args))
+    go _ _ []
+      = []
+
+    go fun_kind subst all_args@(arg : args)
+      | Just (tcb, inner_kind) <- splitPiTy_maybe fun_kind
+      = case tcb of
+          Anon _              -> AnonTCB      : go inner_kind subst  args
+          Named (Bndr tv vis) -> NamedTCB vis : go inner_kind subst' args
+                 where
+                    subst' = extendTCvSubst subst tv arg
+
+      | not (isEmptyTCvSubst subst)
+      = go (substTy subst fun_kind) init_subst all_args
+
+      | otherwise
+      = pprPanic "addTcbVisibilities" (ppr tc <+> ppr orig_args)
+
+
 {- Note [TyConBinders for the result kind signature of a data type]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Given
   data T (a::*) :: * -> forall k. k -> *
 we want to generate the extra TyConBinders for T, so we finally get
   (a::*) (b::*) (k::*) (c::k)
-The function tcDataKindSig generates these extra TyConBinders from
+The function etaExpandAlgTyCon generates these extra TyConBinders from
 the result kind signature.
 
 We need to take care to give the TyConBinders
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index fc2ea052e4..6f5ea359e5 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -543,7 +543,7 @@ tcClsInstDecl (L _ (XClsInstDecl _)) = panic "tcClsInstDecl"
 {-
 ************************************************************************
 *                                                                      *
-               Type checking family instances
+               Type family instances
 *                                                                      *
 ************************************************************************
 
@@ -561,7 +561,8 @@ 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 <- tcFamInstDeclChecks mb_clsinfo fam_lname
+       ; fam_tc <- tcLookupLocatedTyCon fam_lname
+       ; tcFamInstDeclChecks mb_clsinfo fam_tc
 
          -- (0) Check it's an open type family
        ; checkTc (isTypeFamilyTyCon fam_tc)     (wrongKindOfFamily fam_tc)
@@ -579,6 +580,56 @@ tcTyFamInstDecl mb_clsinfo (L loc decl@(TyFamInstDecl { tfid_eqn = eqn }))
        ; let axiom = mkUnbranchedCoAxiom rep_tc_name fam_tc co_ax_branch
        ; newFamInst SynFamilyInst axiom }
 
+
+---------------------
+tcFamInstDeclChecks :: AssocInstInfo -> TyCon -> TcM ()
+-- Used for both type and data families
+tcFamInstDeclChecks mb_clsinfo fam_tc
+  = do { -- Type family instances require -XTypeFamilies
+         -- and can't (currently) be in an hs-boot file
+       ; traceTc "tcFamInstDecl" (ppr fam_tc)
+       ; type_families <- xoptM LangExt.TypeFamilies
+       ; is_boot       <- tcIsHsBootOrSig   -- Are we compiling an hs-boot file?
+       ; checkTc type_families $ badFamInstDecl fam_tc
+       ; checkTc (not is_boot) $ badBootFamInstDeclErr
+
+       -- Check that it is a family TyCon, and that
+       -- oplevel type instances are not for associated types.
+       ; checkTc (isFamilyTyCon fam_tc) (notFamily fam_tc)
+
+       ; when (isNotAssociated mb_clsinfo &&   -- Not in a class decl
+               isTyConAssoc fam_tc)            -- but an associated type
+              (addErr $ assocInClassErr fam_tc)
+       }
+
+{- 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.
+
+
+************************************************************************
+*                                                                      *
+               Data family instances
+*                                                                      *
+************************************************************************
+
+For some reason data family instances are a lot more complicated
+than type family instances
+-}
+
 tcDataFamInstDecl :: AssocInstInfo
                   -> LDataFamInstDecl GhcRn -> TcM (FamInst, Maybe DerivInfo)
   -- "newtype instance" and "data instance"
@@ -597,7 +648,9 @@ tcDataFamInstDecl mb_clsinfo
                                         , dd_derivs  = derivs } }}}))
   = setSrcSpan loc             $
     tcAddDataFamInstCtxt decl  $
-    do { fam_tc <- tcFamInstDeclChecks mb_clsinfo lfam_name
+    do { fam_tc <- tcLookupLocatedTyCon lfam_name
+
+       ; tcFamInstDeclChecks mb_clsinfo fam_tc
 
        -- Check that the family declaration is for the right kind
        ; checkTc (isDataFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
@@ -609,25 +662,27 @@ tcDataFamInstDecl mb_clsinfo
              <- tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs
                                 fixity hs_ctxt hs_pats m_ksig hs_cons
 
-       -- Construct representation tycon
-       ; rep_tc_name <- newFamInstTyConName lfam_name pats
-       ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
+       -- Eta-reduce the axiom if possible
+       -- Quite tricky: see Note [Eta-reduction for data families]
+       ; let (eta_pats, eta_tcbs) = eta_reduce fam_tc pats
+             eta_tvs       = map binderVar eta_tcbs
+             post_eta_qtvs = filterOut (`elem` eta_tvs) qtvs
 
-       ; let (eta_pats, etad_tvs) = eta_reduce fam_tc pats
-             eta_tvs              = filterOut (`elem` etad_tvs) qtvs
-                 -- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced
-
-             full_tcbs = mkTyConBindersPreferAnon (eta_tvs ++ etad_tvs) res_kind
+             full_tcbs = mkTyConBindersPreferAnon post_eta_qtvs
+                            (tyCoVarsOfType (mkSpecForAllTys eta_tvs res_kind))
+                         ++ eta_tcbs
                  -- Put the eta-removed tyvars at the end
                  -- Remember, qtvs is in arbitrary order, except kind vars are
-                 -- first, so there is no reason to suppose that the etad_tvs
+                 -- first, so there is no reason to suppose that the eta_tvs
                  -- (obtained from the pats) are at the end (Trac #11148)
 
-       -- Deal with any kind signature.
+       -- Eta-expand the representation tycon until it has reult kind *
        -- See also Note [Arity of data families] in FamInstEnv
-       ; (extra_tcbs, final_res_kind) <- tcDataKindSig full_tcbs res_kind
+       -- NB: we can do this after eta-reducing the axiom, because if
+       --     we did it before the "extra" tvs from etaExpandAlgTyCon
+       --     would always be eta-reduced
+       ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind
        ; checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
-
        ; let extra_pats  = map (mkTyVarTy . binderVar) extra_tcbs
              all_pats    = pats `chkAppend` extra_pats
              orig_res_ty = mkTyConApp fam_tc all_pats
@@ -636,12 +691,12 @@ tcDataFamInstDecl mb_clsinfo
        ; traceTc "tcDataFamInstDecl" $
          vcat [ text "Fam tycon:" <+> ppr fam_tc
               , text "Pats:" <+> ppr pats
+              , text "visibliities:" <+> ppr (tcbVisibilities fam_tc pats)
               , text "all_pats:" <+> ppr all_pats
               , text "ty_binders" <+> ppr ty_binders
               , text "fam_tc_binders:" <+> ppr (tyConBinders fam_tc)
-              , text "deps:" <+> ppr (map isNamedTyConBinder (tyConBinders fam_tc))
               , text "eta_pats" <+> ppr eta_pats
-              , text "eta_tvs" <+> ppr eta_tvs ]
+              , text "eta_tcbs" <+> ppr eta_tcbs ]
 
        ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
            do { data_cons <- tcExtendTyVarEnv qtvs $
@@ -649,17 +704,18 @@ tcDataFamInstDecl mb_clsinfo
                              -- over the data constructors
                              tcConDecls rec_rep_tc ty_binders orig_res_ty hs_cons
 
+              ; rep_tc_name <- newFamInstTyConName lfam_name pats
+              ; axiom_name  <- newFamInstAxiomName lfam_name [pats]
               ; tc_rhs <- case new_or_data of
                      DataType -> return (mkDataTyConRhs data_cons)
                      NewType  -> ASSERT( not (null data_cons) )
                                  mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons)
 
-              ; let axiom  = mkSingleCoAxiom Representational
-                                             axiom_name eta_tvs [] fam_tc eta_pats
-                                             (mkTyConApp rep_tc (mkTyVarTys eta_tvs))
+              ; let axiom  = mkSingleCoAxiom Representational axiom_name
+                                 post_eta_qtvs [] fam_tc eta_pats
+                                 (mkTyConApp rep_tc (mkTyVarTys post_eta_qtvs))
                     parent = DataFamInstTyCon axiom fam_tc all_pats
 
-
                       -- 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
@@ -691,7 +747,7 @@ tcDataFamInstDecl mb_clsinfo
        ; fam_inst <- newFamInst (DataFamilyInst rep_tc) axiom
        ; return (fam_inst, m_deriv_info) }
   where
-    eta_reduce :: TyCon -> [Type] -> ([Type], [TyVar])
+    eta_reduce :: TyCon -> [Type] -> ([Type], [TyConBinder])
     -- See Note [Eta reduction for data families] in FamInstEnv
     -- Splits the incoming patterns into two: the [TyVar]
     -- are the patterns that can be eta-reduced away.
@@ -699,30 +755,32 @@ tcDataFamInstDecl mb_clsinfo
     --
     -- NB: quadratic algorithm, but types are small here
     eta_reduce fam_tc pats
-        = go (reverse (zip3 pats fvs_s deps)) []
+        = go (reverse (zip3 pats fvs_s vis_s)) []
         where
+          vis_s :: [TyConBndrVis]
+          vis_s = tcbVisibilities fam_tc pats
+
           fvs_s :: [TyCoVarSet]  -- 1-1 correspondence with pats
                                  -- Each elt is the free vars of all /earlier/ pats
           (_, fvs_s) = mapAccumL add_fvs emptyVarSet pats
           add_fvs fvs pat = (fvs `unionVarSet` tyCoVarsOfType pat, fvs)
 
-          deps :: [Bool]
-          deps = map isNamedBinder tc_bndrs ++ repeat False
-          (tc_bndrs, _) = splitPiTys (tyConKind fam_tc)
-
-    go ((pat, fvs_to_the_left, is_dep):pats) etad_tvs
-      | not is_dep
-      , Just tv <- getTyVar_maybe pat
+    go ((pat, fvs_to_the_left, tcb_vis):pats) etad_tvs
+      | Just tv <- getTyVar_maybe pat
       , not (tv `elemVarSet` fvs_to_the_left)
-      = go pats (tv : etad_tvs)
+      = go pats (Bndr tv tcb_vis : etad_tvs)
     go pats etad_tvs = (reverse (map fstOf3 pats), etad_tvs)
 
 tcDataFamInstDecl _ _ = panic "tcDataFamInstDecl"
 
+-----------------------
 tcDataFamHeader :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr GhcRn]
                 -> LexicalFixity -> LHsContext GhcRn
                 -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn]
                 -> TcM ([TyVar], [Type], Kind, ThetaType)
+-- The "header" is the part other than the data constructors themselves
+-- e.g.  data instance D [a] :: * -> * = ...
+-- Here the "header" is the bit before the "=" sign
 tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons
   = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind)))
             <- pushTcLevelM_                                $
@@ -747,10 +805,10 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
        ; res_kind     <- zonkTcTypeToTypeX ze res_kind
        ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta
 
-       ; let pats = unravelFamInstPats lhs_ty
-
        -- Check that type patterns match the class instance head
+       ; let pats = unravelFamInstPats lhs_ty
        ; checkConsistentFamInst mb_clsinfo fam_tc pats
+
        ; return (qtvs, pats, res_kind, stupid_theta) }
   where
     fam_name  = tyConName fam_tc
@@ -769,29 +827,6 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
              -- Perhaps surprisingly, we don't need the skolemised tvs themselves
            ; return (substTy subst inner_kind) }
 
----------------------
-tcFamInstDeclChecks :: AssocInstInfo -> 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 (isNotAssociated mb_clsinfo &&   -- Not in a class decl
-               isTyConAssoc fam_tc)            -- but an associated type
-              (addErr $ assocInClassErr fam_tc_lname)
-
-       ; return fam_tc }
-
 {- Note [Result kind signature for a data family instance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The expected type might have a forall at the type. Normally, we
@@ -801,27 +836,93 @@ 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
 
-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 [Eta-reduction for data families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   data D :: * -> * -> * -> * -> *
 
-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
+   data instance D [(a,b)] p q :: * -> * where
+      D1 :: blah1
+      D2 :: blah2
+
+Then we'll generate a representation data type
+  data Drep a b p q z where
+      D1 :: blah1
+      D2 :: blah2
+
+and an axiom to connect them
+  axiom AxDrep forall a b p q z. D [(a,b]] p q z = Drep a b p q z
+
+except that we'll eta-reduce the axiom to
+  axiom AxDrep forall a b. D [(a,b]] = Drep a b
+There are several fiddly subtleties lurking here
+
+* The representation tycon Drep is parameerised over the free
+  variables of the pattern, in no particular order. So there is no
+  guarantee that 'p' and 'q' will come last in Drep's parameters, and
+  in the right order.  So, if the /patterns/ of the family insatance
+  are eta-redcible, we re-order Drep's parameters to put the
+  eta-reduced type variables last.
+
+* Although we eta-reduce the axiom, we eta-/expand/ the representation
+  tycon Drep.  The kind of D says it takses four arguments, but the
+  data instance header only supplies three.  But the AlgTyCOn for Drep
+  itself must have enough TyConBinders so that its result kind is Type.
+  So, with etaExpandAlgTyCon we make up some extra TyConBinders
+
+* The result kind in the instance might be a polykind, like this:
+     data family DP a :: forall k. k -> *
+     data instance DP [b] :: forall k1 k2. (k1,k2) -> *
+
+  So in type-checking the LHS (DP Int) we need to check that it is
+  more polymorphic than the signature.  To do that we must skolemise
+  the siganture and istantiate the call of DP.  So we end up with
+     data instance DP [b] @(k1,k2) (z :: (k1,k2)) where
+
+  Note that we must parameterise the representation tycon DPrep over
+  'k1' and 'k2', as well as 'b'.
+
+  The skolemise bit is done in tc_kind_sig, while the instantiate bit
+  is done by the checkExpectedKind that immediately follows.
+
+* Very fiddly point.  When we eta-reduce to
+     axiom AxDrep forall a b. D [(a,b]] = Drep a b
+
+  we want the kind of (D [(a,b)]) to be the same as the kind of
+  (Drep a b).  This ensures that applying the axiom doesn't change the
+  kind.  Why is that hard?  Because the kind of (Drep a b) depends on
+  the TyConBndrVis on Drep's arguments. In particular do we have
+    (forall (k::*). blah) or (* -> blah)?
+
+  We must match whatever D does!  In Trac #15817 we had
+      data family X a :: forall k. * -> *   -- Note: a forall that is not used
+      data instance X Int b = MkX
+
+  So the data intance is really
+      data istance X Int @k b = MkX
+
+  The axiom will look like
+      axiom    X Int = Xrep
+
+  and it's important that XRep :: forall k * -> *, following X.
+
+  To achieve this we get the TyConBndrVis flags from tcbVisibilities,
+  and use those flags for any eta-reduced arguments.  Sigh.
+
+* The final turn of the knife is that tcbVisibilities is itself
+  tricky to sort out.  Consider
+      data family D k :: k
+  Then consider D (forall k2. k2 -> k2) Type Type
+  The visibilty flags on an application of D may affected by the arguments
+  themselves.  Heavy sigh.  But not truly hard; that's what tcbVisibilities
+  does.
 
-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
+      Class instance declarations, pass 2
 *                                                                      *
 ********************************************************************* -}
 
@@ -2005,12 +2106,12 @@ notFamily tycon
   = vcat [ text "Illegal family instance for" <+> quotes (ppr tycon)
          , nest 2 $ parens (ppr tycon <+> text "is not an indexed type family")]
 
-assocInClassErr :: Located Name -> SDoc
+assocInClassErr :: TyCon -> SDoc
 assocInClassErr name
  = text "Associated type" <+> quotes (ppr name) <+>
    text "must be inside a class instance"
 
-badFamInstDecl :: Located Name -> SDoc
+badFamInstDecl :: TyCon -> SDoc
 badFamInstDecl tc_name
   = vcat [ text "Illegal family instance for" <+>
            quotes (ppr tc_name)
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 6f23e5aba6..3500b72a54 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1738,8 +1738,8 @@ zonkTyCoVar tv | isTcTyVar tv = zonkTcTyVar tv
                | otherwise    = ASSERT2( isCoVar tv, ppr tv )
                                 mkCoercionTy . mkCoVarCo <$> zonkTyCoVarKind tv
    -- Hackily, when typechecking type and class decls
-   -- we have TyVars in scopeadded (only) in
-   -- TcHsType.tcTyClTyVars, but it seems
+   -- we have TyVars in scope added (only) in
+   -- TcHsType.bindTyClTyVars, but it seems
    -- painful to make them into TcTyVars there
 
 zonkTyCoVarsAndFV :: TyCoVarSet -> TcM TyCoVarSet
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 41504d6840..9e869c3db9 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -380,8 +380,7 @@ TcTyCons are used for two distinct purposes
 
     Instead of trying, we just store the list of type variables to
     bring into scope, in the tyConScopedTyVars field of the TcTyCon.
-    These tyvars are brought into scope in kcTyClTyVars and
-    tcTyClTyVars, both in TcHsType.
+    These tyvars are brought into scope in TcHsType.bindTyClTyVars.
 
     In a TcTyCon, why is tyConScopedTyVars :: [(Name,TcTyVar)] rather
     than just [TcTyVar]?  Consider these mutually-recursive decls
@@ -731,7 +730,7 @@ paths for
 
 Note that neither code path worries about point (4) above, as this
 is nicely handled by not mangling the res_kind. (Mangling res_kinds is done
-*after* all this stuff, in tcDataDefn's call to tcDataKindSig.)
+*after* all this stuff, in tcDataDefn's call to etaExpandAlgTyCon.)
 
 We can tell Inferred apart from Specified by looking at the scoped
 tyvars; Specified are always included there.
@@ -1023,23 +1022,21 @@ kcTyClDecl (DataDecl { tcdLName    = (dL->L _ name)
     --    (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
 
   | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
-  = kcTyClTyVars name $
+  = bindTyClTyVars name $ \ _ _ ->
     do  { _ <- tcHsContext ctxt
         ; mapM_ (wrapLocM_ kcConDecl) cons }
 
-kcTyClDecl (SynDecl { tcdLName = (dL->L _ name)
-                    , tcdRhs = lrhs })
-  = kcTyClTyVars name $
-    do  { syn_tc <- kcLookupTcTyCon name
+kcTyClDecl (SynDecl { tcdLName = dl->L _ name, tcdRhs = rhs })
+  = bindTyClTyVars name $ \ _ res_kind ->
+    discardResult $ tcCheckLHsType rhs res_kind
         -- NB: check against the result kind that we allocated
         -- in getInitialKinds.
-        ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }
 
 kcTyClDecl (ClassDecl { tcdLName = (dL->L _ name)
                       , tcdCtxt = ctxt, tcdSigs = sigs })
-  = kcTyClTyVars name $
+  = bindTyClTyVars name $ \ _ _ ->
     do  { _ <- tcHsContext ctxt
-        ; mapM_ (wrapLocM_ kc_sig)     sigs }
+        ; mapM_ (wrapLocM_ kc_sig) sigs }
   where
     kc_sig (ClassOpSig _ _ nms op_ty) = kcHsSigType nms op_ty
     kc_sig _                          = return ()
@@ -1266,7 +1263,7 @@ tcTyClDecl1 _parent roles_info
             (SynDecl { tcdLName = (dL->L _ tc_name)
                      , tcdRhs   = rhs })
   = ASSERT( isNothing _parent )
-    tcTyClTyVars tc_name $ \ binders res_kind ->
+    bindTyClTyVars tc_name $ \ binders res_kind ->
     tcTySynRhs roles_info tc_name binders res_kind rhs
 
   -- "data/newtype" declaration
@@ -1274,7 +1271,7 @@ tcTyClDecl1 _parent roles_info
             (DataDecl { tcdLName = (dL->L _ tc_name)
                       , tcdDataDefn = defn })
   = ASSERT( isNothing _parent )
-    tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
+    bindTyClTyVars tc_name $ \ tycon_binders res_kind ->
     tcDataDefn roles_info tc_name tycon_binders res_kind defn
 
 tcTyClDecl1 _parent roles_info
@@ -1306,7 +1303,7 @@ tcClassDecl1 :: RolesInfo -> Name -> LHsContext GhcRn
 tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
   = fixM $ \ clas ->
     -- We need the knot because 'clas' is passed into tcClassATs
-    tcTyClTyVars class_name $ \ binders res_kind ->
+    bindTyClTyVars class_name $ \ binders res_kind ->
     do { MASSERT2( tcIsConstraintKind res_kind
                  , ppr class_name $$ ppr res_kind )
        ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
@@ -1432,7 +1429,7 @@ tcDefaultAssocDecl fam_tc [dL->L loc (FamEqn { feqn_tycon = L _ tc_name
        -- Typecheck RHS
        ; let hs_pats = map hsLTyVarBndrToType exp_vars
 
-          -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
+          -- NB: Use tcFamTyPats, not bindTyClTyVars. The latter expects to get
           -- the LHsQTyVars used for declaring a tycon, but the names here
           -- are different.
 
@@ -1501,7 +1498,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
                               , fdTyVars = user_tyvars
                               , fdInjectivityAnn = inj })
   | DataFamily <- fam_info
-  = tcTyClTyVars tc_name $ \ binders res_kind -> do
+  = bindTyClTyVars tc_name $ \ binders res_kind -> do
   { traceTc "data family:" (ppr tc_name)
   ; checkFamFlag tc_name
 
@@ -1527,7 +1524,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
   ; return tycon }
 
   | OpenTypeFamily <- fam_info
-  = tcTyClTyVars tc_name $ \ binders res_kind -> do
+  = bindTyClTyVars tc_name $ \ binders res_kind -> do
   { traceTc "open type family:" (ppr tc_name)
   ; checkFamFlag tc_name
   ; inj' <- tcInjectivity binders inj
@@ -1543,8 +1540,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info
          -- the variables in the header scope only over the injectivity
          -- declaration but this is not involved here
        ; (inj', binders, res_kind)
-            <- tcTyClTyVars tc_name
-               $ \ binders res_kind ->
+            <- bindTyClTyVars tc_name $ \ binders res_kind ->
                do { inj' <- tcInjectivity binders inj
                   ; return (inj', binders, res_kind) }
 
@@ -1662,7 +1658,7 @@ tcDataDefn roles_info
  =  do { gadt_syntax <- dataDeclChecks tc_name new_or_data ctxt cons
 
        ; tcg_env <- getGblEnv
-       ; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
+       ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind
 
        ; let hsc_src = tcg_src tcg_env
        ; unless (mk_permissive_kind hsc_src cons) $
@@ -1890,7 +1886,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
        ; traceTc "tcTyFamInstEqnGuts }" (ppr fam_tc <+> pprTyVars qtvs)
        ; return (qtvs, pats, rhs_ty) }
   where
-    tc_lhs | null hs_pats
+    tc_lhs | null hs_pats  -- See Note [Apparently-nullary families]
            = do { (args, rhs_kind) <- tcInstTyBinders $
                                       splitPiTysInvisibleN (tyConArity fam_tc)
                                                            (tyConKind  fam_tc)
@@ -1898,6 +1894,34 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
            | otherwise
            = tcFamTyPats fam_tc mb_clsinfo hs_pats
 
+{- Note [Apparently-nullary families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  type family F :: k -> *
+
+This really means
+  type family F @k :: k -> *
+
+That is, the family has arity 1, and can match on the kind. So it's
+not really a nullary family.   NB that
+  type famly F2 :: forall k. k -> *
+is quite different and really does have arity 0.
+
+Returning to F we might have
+  type instannce F = Maybe
+which instantaite 'k' to '*' and really means
+  type instannce F @* = Maybe
+
+Conclusion: in this odd case where there are no LHS patterns, we
+should instantiate any invisible foralls in F's kind, to saturate
+its arity (but no more).  This is what happens in tc_lhs in
+tcTyFamInstEqnGuts.
+
+If there are any visible patterns, then the first will force
+instantiation of any Inferred quantifiers for F -- remember,
+Inferred quantifiers always come first.
+-}
+
 
 -----------------
 tcFamTyPats :: TyCon -> AssocInstInfo
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index a40a02dd2a..eb0b84d47e 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -564,7 +564,7 @@ They fit together like so:
   Note that that are three binders here, including the
   kind variable k.
 
-- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
+* See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
   for what the visibility flag means.
 
 * Each TyConBinder tyConBinders has a TyVar (sometimes it is TyCoVar), and
@@ -584,10 +584,15 @@ They fit together like so:
 
   tyConKind is the full kind of the TyCon, not just the result kind
 
-* tyConArity is the arguments this TyCon must be applied to, to be
-  considered saturated.  Here we mean "applied to in the actual Type",
-  not surface syntax; i.e. including implicit kind variables.
-  So it's just (length tyConBinders)
+* For type families, tyConArity is the arguments this TyCon must be
+  applied to, to be considered saturated.  Here we mean "applied to in
+  the actual Type", not surface syntax; i.e. including implicit kind
+  variables.  So it's just (length tyConBinders)
+
+* For an algebraic data type, or data instance, the tyConResKind is
+  always (TYPE r); that is, the tyConBinders are enough to saturate
+  the type constructor.  I'm not quite sure why we have this invariant,
+  but it's enforced by etaExpandAlgTyCon
 -}
 
 instance Outputable tv => Outputable (VarBndr tv TyConBndrVis) where
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index f20aaf7678..aa67e06a2a 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1403,12 +1403,12 @@ mkLamTypes vs ty = foldr mkLamType ty vs
 -- We want (k:*) Named, (b:k) Anon, (c:k) Anon
 --
 -- All non-coercion binders are /visible/.
-mkTyConBindersPreferAnon :: [TyVar] -> Type -> [TyConBinder]
-mkTyConBindersPreferAnon vars inner_ty = ASSERT( all isTyVar vars)
-                                               fst (go vars)
+mkTyConBindersPreferAnon :: [TyVar] -> TyCoVarSet -> [TyConBinder]
+mkTyConBindersPreferAnon vars inner_tkvs = ASSERT( all isTyVar vars)
+                                           fst (go vars)
   where
     go :: [TyVar] -> ([TyConBinder], VarSet) -- also returns the free vars
-    go [] = ([], tyCoVarsOfType inner_ty)
+    go [] = ([], inner_tkvs)
     go (v:vs) | v `elemVarSet` fvs
               = ( Bndr v (NamedTCB Required) : binders
                 , fvs `delVarSet` v `unionVarSet` kind_vars )