A raft of comments about TyBinders

I had a conversation with Richard about TyBinders
and VisibilityFlags.  This patch adds a lot of comments
to explain what is going on.  I feel much more secure now.

Richard please check.

6 files changed, 429 insertions, 274 deletions

diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index f10b1ba5c9..1e4af2d475 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -290,6 +290,12 @@ data DataCon
         --      dcOrigArgTys  = [x,y]
         --      dcRepTyCon       = T
 
+        -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
+        -- FOR THE PARENT TyCon. With GADTs the data con might not even have
+        -- the same number of type variables!
+        -- [This is a change (Oct05): previously, vanilla datacons guaranteed to
+        --  have the same type variables as their parent TyCon, but that seems ugly.]
+
         dcVanilla :: Bool,      -- True <=> This is a vanilla Haskell 98 data constructor
                                 --          Its type is of form
                                 --              forall a1..an . t1 -> ... tm -> T a1..an
@@ -300,25 +306,18 @@ data DataCon
                 --       syntax, provided its type looks like the above.
                 --       The declaration format is held in the TyCon (algTcGadtSyntax)
 
-        dcUnivTyVars   :: [TyVar],      -- Universally-quantified type vars [a,b,c]
-                                        -- INVARIANT: length matches arity of the dcRepTyCon
-                                        ---           result type of (rep) data con is exactly (T a b c)
-        dcUnivTyBinders :: [TyBinder],  -- Binders for universal tyvars. These will all
-                                        -- be Named, and all be Invisible or Specified.
-                                        -- Storing these separately from dcUnivTyVars
-                                        -- is solely because we usually don't need the
-                                        -- binders, and the extraction of the tyvars is
-                                        -- unnecessary work. See also
-                                        -- Note [TyBinders in DataCons]
-
-        dcExTyVars     :: [TyVar],    -- Existentially-quantified type vars
-                -- In general, the dcUnivTyVars are NOT NECESSARILY THE SAME AS THE TYVARS
-                -- FOR THE PARENT TyCon. With GADTs the data con might not even have
-                -- the same number of type variables.
-                -- [This is a change (Oct05): previously, vanilla datacons guaranteed to
-                --  have the same type variables as their parent TyCon, but that seems ugly.]
-
-        dcExTyBinders  :: [TyBinder],  -- see dcUnivTyBinders
+        -- Universally-quantified type vars [a,b,c]
+        dcUnivTyVars    :: [TyVar],     -- Two linked fields
+        dcUnivTyBinders :: [TyBinder],  -- see Note [TyBinders in DataCons]
+
+            -- INVARIANT: length matches arity of the dcRepTyCon
+            --
+            -- INFARIANT: result type of (rep) data con is exactly (T a b c)
+
+        -- Existentially-quantified type vars [x,y]
+        dcExTyVars     :: [TyVar],     -- Two linked fields
+        dcExTyBinders  :: [TyBinder],  -- see Note [TyBinders in DataCons]
+
 
         -- INVARIANT: the UnivTyVars and ExTyVars all have distinct OccNames
         -- Reason: less confusing, and easier to generate IfaceSyn
@@ -420,6 +419,41 @@ data DataCon
   }
   deriving Data.Typeable.Typeable
 
+
+{- Note [TyBinders in DataCons]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+DataCons and PatSyns store their universal and existential type
+variables in a pair of fields, e.g.
+        dcUnivTyVars    :: [TyVar],
+        dcUnivTyBinders :: [TyBinder],
+and similarly dcExTyVars/dcExTyVarBinders
+
+Of these, the former is always redundant:
+  dcUnivTyVars = [ tv | Named tv _ <- dcUnivTyBinders ]
+
+Specifically:
+
+ * The two fields correspond 1-1
+
+ * Each TyBinder a Named (no Anons)
+
+ * The TyVar in each TyBinder is the same as the TyVar in
+   the corresponding tyvar in the TyVars list.
+
+ * Each Visibilty flag (va, vb, etc) is Invisible or Specified.
+   None are Visible. (See Note [No Visible TyBinder in terms];
+   a DataCon is a term-level function.)
+
+Why store these fields redundantly?  Purely convenience.  In most
+places in GHC, it's just the TyVars that are needed, so that's what's
+returned from, say, dataConFullSig.
+
+Why do we need the TyBinders?  So that we can construct the right
+type for the DataCon with its foralls attributed the correce visiblity.
+That in turn governs whether you can use visible type application
+at a call of the data constructor.
+-}
+
 data DataConRep
   = NoDataConRep              -- No wrapper
 
@@ -718,49 +752,11 @@ isMarkedStrict :: StrictnessMark -> Bool
 isMarkedStrict NotMarkedStrict = False
 isMarkedStrict _               = True   -- All others are strict
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
 \subsection{Construction}
 *                                                                      *
-************************************************************************
-
-Note [TyBinders in DataCons]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A DataCon needs to keep track of the visibility of its universals and
-existentials, so that visible type application can work properly. This
-is done by storing the universal and existential TyBinders, along with
-the TyVars. These TyBinders should all be Named and should all be
-Invisible or Specified; we don't have Visible or Anon type arguments.
-
-During construction of a DataCon, we often have the TyBinders of the
-parent TyCon. But those TyBinders are *different* than those of the
-DataCon. Here is an example:
-
-  data Proxy a = P
-
-The TyCon has these TyBinders:
-
-  [ Named (k :: *) Invisible, Anon k ]
-
-Note that Proxy's kind is forall k. k -> *. But the DataCon P should
-have (universal) TyBinders
-
-  [ Named (k :: *) Invisible, Named (a :: k) Specified ]
-
-So we want to take the TyCon's TyBinders and the TyCon's TyVars and
-merge them, pulling variable names from the TyVars but visibilities
-from the TyBinders, perserving Invisible but changing Visible to
-Specified. (The `a` in Proxy is indeed Visible, but the `a` in P should
-be Specified.) This merging operation is done in buildDataCon. In contrast,
-the TyBinders passed to mkDataCon are the real TyBinders stored in the
-DataCon. Note that passing the TyVars into mkDataCon is redundant, but
-convenient for both caller and the function's implementation.
-
-In most places in GHC, it's just the TyVars that are needed,
-so that's what's returned from, say, dataConFullSig.
-
--}
+********************************************************************* -}
 
 -- | Build a new data constructor
 mkDataCon :: Name
diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs
index 9e87ecf042..3eea30018f 100644
--- a/compiler/basicTypes/PatSyn.hs
+++ b/compiler/basicTypes/PatSyn.hs
@@ -64,16 +64,21 @@ data PatSyn
                                        -- record pat syn or same length as
                                        -- psArgs
 
-        psUnivTyVars  :: [TyVar],      -- Universially-quantified type variables
-        psUnivTyBinders :: [TyBinder], -- same, with visibility info
-        psReqTheta    :: ThetaType,    -- Required dictionaries
-                                       -- these constraints are very much like
-                                       -- stupid thetas (which is a useful
-                                       -- guideline when implementing)
-                                       -- but are actually needed.
-        psExTyVars    :: [TyVar],      -- Existentially-quantified type vars
-        psExTyBinders :: [TyBinder],   -- same, with visibility info
-        psProvTheta   :: ThetaType,    -- Provided dictionaries
+        -- Universially-quantified type variables
+        psUnivTyVars    :: [TyVar],    -- Two linked fields; see DataCon
+        psUnivTyBinders :: [TyBinder], -- Note [TyBinders in DataCons]
+
+        -- Required dictionaries (may mention psUnivTyVars)
+        psReqTheta    :: ThetaType,
+
+        -- Existentially-quantified type vars
+        psExTyVars    :: [TyVar],      -- Two linked fields; see DataCon
+        psExTyBinders :: [TyBinder],   -- Note [TyBinders in DataCons]
+
+        -- Provided dictionaries (may mention psUnivTyVars or psExTyVars)
+        psProvTheta   :: ThetaType,
+
+        -- Result type
         psOrigResTy   :: Type,         -- Mentions only psUnivTyVars
 
         -- See Note [Matchers and builders for pattern synonyms]
diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index e20a6c6a8d..f62e5eeacb 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -29,6 +29,7 @@ import MkId
 import Class
 import TyCon
 import Type
+import TyCoRep( TyBinder(..) )
 import Id
 import TcType
 
@@ -136,14 +137,7 @@ buildDataCon fam_envs src_name declared_infix prom_info src_bangs impl_bangs fie
         ; traceIf (text "buildDataCon 1" <+> ppr src_name)
         ; us <- newUniqueSupply
         ; dflags <- getDynFlags
-        ; let   -- See Note [TyBinders in DataCons] in DataCon
-              dc_bndrs = zipWith mk_binder univ_tvs univ_bndrs
-              mk_binder tv bndr = mkNamedBinder vis tv
-                where
-                  vis = case binderVisibility bndr of
-                    Invisible -> Invisible
-                    _         -> Specified
-
+        ; let dc_bndrs    = mkDataConUnivTyBinders univ_bndrs univ_tvs
               stupid_ctxt = mkDataConStupidTheta rep_tycon arg_tys univ_tvs
               data_con = mkDataCon src_name declared_infix prom_info
                                    src_bangs field_lbls
@@ -177,6 +171,69 @@ mkDataConStupidTheta tycon arg_tys univ_tvs
                       tyCoVarsOfType pred `intersectVarSet` arg_tyvars
 
 
+mkDataConUnivTyBinders :: [TyBinder] -> [TyVar]   -- From the TyCon
+                       -> [TyBinder]              -- For the DataCon
+-- See Note [Building the TyBinders for a DataCon]
+mkDataConUnivTyBinders bndrs tvs
+ = zipWith mk_binder bndrs tvs
+ where
+   mk_binder bndr tv = mkNamedBinder vis tv
+      where
+        vis = case bndr of
+                Anon _          -> Specified
+                Named _ Visible -> Specified
+                Named _ vis     -> vis
+
+{- Note [Building the TyBinders for a DataCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A DataCon needs to keep track of the visibility of its universals and
+existentials, so that visible type application can work properly. This
+is done by storing the universal and existential TyBinders, along with
+the TyVars.  See Note [TyBinders in DataCons] in DataCon.
+
+During construction of a DataCon, we often start from the TyBinders of
+the parent TyCon.  For example
+   data Maybe a = Nothing | Just a
+The DataCons start from the TyBinders of the parent TyCon.
+
+But the ultimate TyBinders for the DataCon are *different* than those
+of the DataCon. Here is an example:
+
+  data App a b = MkApp (a b) -- App :: forall {k}. (k->*) -> k -> *
+
+The TyCon has
+
+  tyConTyVars    = [ k:*,                      a:k->*,      b:k]
+  tyConTyBinders = [ Named (k :: *) Invisible, Anon (k->*), Anon k ]
+
+The TyBinders for App line up with App's kind, given above.
+
+But the DataCon MkApp has the type
+  MkApp :: forall {k} (a:k->*) (b:k). a b -> App k a b
+
+That is, its TyBinders should be
+
+  dataConUnivTyVars = [ Named (k:*)    Invisible
+                      , Named (a:k->*) Specified
+                      , Named (b:k)    Specified ]
+
+So we want to take the TyCon's TyBinders and the TyCon's TyVars and
+merge them, pulling
+  - variable names from the TyVars
+  - visibilities from the TyBinders
+  - but changing Anon/Visible to Specified
+
+The last part about Visible->Specified comes from this:
+  data T k (a:k) b = MkT (a b)
+Here k is Visible in T's kind, but we don't have Visible binders in
+the TyBinders for a term (see Note [No Visible TyBinder in terms]
+in TyCoRep), so we change it to Specified when making MkT's TyBinders
+
+This merging operation is done by mkDataConUnivTyBinders. In contrast,
+the TyBinders passed to mkDataCon are the final TyBinders stored in the
+DataCon (mkDataCon does no further work).
+-}
+
 ------------------------------------------------------
 buildPatSyn :: Name -> Bool
             -> (Id,Bool) -> Maybe (Id, Bool)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 429c4b815d..6fff74e4b7 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -902,7 +902,7 @@ tcDataDefn rec_info     -- Knot-tied; don't look at this eagerly
                      , dd_cons = cons })
  =  do { (extra_tvs, extra_bndrs, real_res_kind) <- tcDataKindSig res_kind
        ; let final_bndrs  = tycon_binders `chkAppend` extra_bndrs
-             final_tvs    = tvs `chkAppend` extra_tvs
+             final_tvs    = tvs           `chkAppend` extra_tvs
              roles        = rti_roles rec_info tc_name
 
        ; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 0a5436fcf6..6cbdfda033 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -168,16 +168,19 @@ import Data.IORef ( IORef )   -- for CoercionHole
 import GHC.Stack (CallStack)
 #endif
 
-{-
-%************************************************************************
-%*                                                                      *
-\subsection{The data type}
-%*                                                                      *
-%************************************************************************
--}
+{- **********************************************************************
+*                                                                       *
+                        Type
+*                                                                       *
+********************************************************************** -}
 
 -- | The key representation of types within the compiler
 
+type KindOrType = Type -- See Note [Arguments to type constructors]
+
+-- | The key type representing kinds in the compiler.
+type Kind = Type
+
 -- If you edit this type, you may need to update the GHC formalism
 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
 data Type
@@ -241,64 +244,8 @@ data TyLit
   | StrTyLit FastString
   deriving (Eq, Ord, Data.Data, Data.Typeable)
 
--- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
--- ('Named') or nondependent ('Anon'). They may also be visible or not.
--- See also Note [TyBinder]
-data TyBinder
-  = Named TyVar VisibilityFlag  -- Always a TyVar (not CoVar or Id)
-  | Anon Type   -- Visibility is determined by the type (Constraint vs. *)
-    deriving (Data.Typeable, Data.Data)
-
--- | Is something required to appear in source Haskell ('Visible'),
--- permitted by request ('Specified') (visible type application), or
--- prohibited entirely from appearing in source Haskell ('Invisible')?
--- Examples in Note [VisibilityFlag]
-data VisibilityFlag = Visible | Specified | Invisible
-  deriving (Eq, Data.Typeable, Data.Data)
-
--- | Do these denote the same level of visibility? Except that
--- 'Specified' and 'Invisible' are considered the same. Used
--- for printing.
-sameVis :: VisibilityFlag -> VisibilityFlag -> Bool
-sameVis Visible Visible = True
-sameVis Visible _       = False
-sameVis _       Visible = False
-sameVis _       _       = True
-
-instance Binary VisibilityFlag where
-  put_ bh Visible   = putByte bh 0
-  put_ bh Specified = putByte bh 1
-  put_ bh Invisible = putByte bh 2
-
-  get bh = do
-    h <- getByte bh
-    case h of
-      0 -> return Visible
-      1 -> return Specified
-      _ -> return Invisible
-
-type KindOrType = Type -- See Note [Arguments to type constructors]
-
--- | The key type representing kinds in the compiler.
-type Kind = Type
-
-{-
-Note [TyBinder]
-~~~~~~~~~~~~~~~
-This represents the type of binders -- that is, the type of an argument
-to a Pi-type. GHC Core currently supports two different Pi-types:
-a non-dependent function, written with ->, and a dependent compile-time-only
-polytype, written with forall. Both Pi-types classify terms/types that
-take an argument. In other words, if `x` is either a function or a polytype,
-`x arg` makes sense (for an appropriate `arg`). It is thus often convenient
-to group Pi-types together. This is ForAllTy.
-
-The two constructors for TyBinder sort out the two different possibilities.
-`Named` builds a polytype, while `Anon` builds an ordinary function.
-(ForAllTy (Anon arg) res used to be called FunTy arg res.)
-
-Note [The kind invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [The kind invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The kinds
    #          UnliftedTypeKind
    OpenKind   super-kind of *, #
@@ -408,54 +355,208 @@ Another helpful principle with eqType is this:
 
 This principle also tells us that eqType must relate only types with the
 same kinds.
+-}
 
-Note [VisibilityFlag]
-~~~~~~~~~~~~~~~~~~~~~
-All named binders are equipped with a visibility flag, which says
-whether or not arguments for this binder should be visible (explicit)
-in source Haskell. Historically, all named binders (that is, polytype
-binders) have been Invisible. But now it's more complicated.
+{- **********************************************************************
+*                                                                       *
+                  TyBinder and VisibilityFlag
+*                                                                       *
+********************************************************************** -}
 
-Invisible:
- Argument does not ever appear in source Haskell. With visible type
- application, only GHC-generated polytypes have Invisible binders.
- This exactly corresponds to "generalized" variables from the
- Visible Type Applications paper (ESOP'16).
+-- | A 'TyBinder' represents an argument to a function. TyBinders can be dependent
+-- ('Named') or nondependent ('Anon'). They may also be visible or not.
+-- See Note [TyBinders]
+data TyBinder
+  = Named TyVar VisibilityFlag  -- Always a TyVar (not CoVar or Id)
+  | Anon Type   -- Visibility is determined by the type (Constraint vs. *)
+    deriving (Data.Typeable, Data.Data)
 
- Example: f x = x
- `f` will be inferred to have type `forall a. a -> a`, where `a` is
- Invisible. Note that there is no type annotation for `f`.
+-- | Is something required to appear in source Haskell ('Visible'),
+-- permitted by request ('Specified') (visible type application), or
+-- prohibited entirely from appearing in source Haskell ('Invisible')?
+-- See Note [TyBinders and VisibilityFlags]
+data VisibilityFlag = Visible | Specified | Invisible
+  deriving (Eq, Data.Typeable, Data.Data)
 
- Printing: With -fprint-explicit-foralls, Invisible binders are written
- in braces. Otherwise, they are printed like Specified binders.
+-- | Do these denote the same level of visibility? Except that
+-- 'Specified' and 'Invisible' are considered the same. Used
+-- for printing.
+sameVis :: VisibilityFlag -> VisibilityFlag -> Bool
+sameVis Visible Visible = True
+sameVis Visible _       = False
+sameVis _       Visible = False
+sameVis _       _       = True
 
-Specified:
- The argument for this binder may appear in source Haskell only with
- visible type application. Otherwise, it is omitted.
+{- Note [TyBinders]
+~~~~~~~~~~~~~~~~~~~
+A ForAllTy contains a TyBinder.
 
- Example: id :: forall a. a -> a
- `a` is a Specified binder, because you can say `id @Int` in source Haskell.
+A TyBinder represents the type of binders -- that is, the type of an
+argument to a Pi-type. GHC Core currently supports two different
+Pi-types:
 
- Example: const :: a -> b -> a
- Both `a` and `b` are Specified binders, even though they are not bound
- by an explicit forall.
+ * A non-dependent function,
+   written with ->, e.g. ty1 -> ty2
+   represented as ForAllTy (Anon ty1) ty2
 
- Printing: a list of Specified binders are put between `forall` and `.`:
- const :: forall a b. a -> b -> a
+ * A dependent compile-time-only polytype,
+   written with forall, e.g.  forall (a:*). ty
+   represented as ForAllTy (Named a v) ty
 
-Visible:
- The argument must be given. Visible binders come up only with TypeInType.
+Both Pi-types classify terms/types that take an argument. In other
+words, if `x` is either a function or a polytype, `x arg` makes sense
+(for an appropriate `arg`). It is thus often convenient to group
+Pi-types together.  This is ForAllTy.
 
- Example: data Proxy k (a :: k) = P
- The kind of Proxy is forall k -> k -> *, where k is a Visible binder.
+The two constructors for TyBinder sort out the two different possibilities.
+`Named` builds a polytype, while `Anon` builds an ordinary function.
+(ForAllTy (Anon arg) res used to be called FunTy arg res.)
 
- Printing: As in the example above, Visible binders are put between `forall`
- and `->`. This syntax is not parsed (yet), however.
+Note [TyBinders and VisibilityFlags]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A ForAllTy contains a TyBinder.  Each Named TyBinders are equipped
+with a VisibilityFlag, which says whether or not arguments for this
+binder should be visible (explicit) in source Haskell.
+
+-----------------------------------------------------------------------
+                                            Occurrences look like this
+ TyBinder          GHC displays type as     in Haskell souce code
+-----------------------------------------------------------------------
+In the type of a term
+ Anon:             f :: type -> type         Arg required:     f x
+ Named Invisible:  f :: forall {a}. type     Arg not allowed:  f
+ Named Specified:  f :: forall a. type       Arg optional:     f  or  f @Int
+ Named Visible:         Illegal: See Note [No Visible TyBinder in terms]
+
+In the kind of a type
+ Anon:             T :: kind -> kind         Required:            T *
+ Named Invisible:  T :: forall {k}. kind     Arg not allowed:     T
+ Named Specified:  T :: forall k. kind       Arg not allowed[1]:  T
+ Named Visible:    T :: forall k -> kind     Required:            T *
+------------------------------------------------------------------------
+
+[1] In types, in the Specified case, it would make sense to allow
+    optional kind applications, thus (T @*), but we have not
+    yet implemented that
+
+---- Examples of where the different visiblities come from -----
+
+In term declarations:
+
+* Invisible.  Function defn, with no signature:  f1 x = x
+  We infer f1 :: forall {a}. a -> a, with 'a' Invisible
+  It's Invisible because it doesn't appear in any
+  user-written signature for f1
+
+* Specified.  Function defn, with signature (implicit forall):
+     f2 :: a -> a; f2 x = x
+  So f2 gets the type f2 :: forall a. a->a, with 'a' Specified
+  even though 'a' is not bound in the source code by an explicit forall
+
+* Specified.  Function defn, with signature (explicit forall):
+     f3 :: forall a. a -> a; f3 x = x
+  So f3 gets the type f3 :: forall a. a->a, with 'a' Specified
+
+* Invisible/Specified.  Function signature with inferred kind polymorphism.
+     f4 :: a b -> Int
+  So 'f4' get the type f4 :: forall {k} (a:k->*) (b:k). a b -> Int
+  Here 'k' is Invisible (it's not mentioned in the type),
+  but 'a' and 'b' are Specified.
+
+* Specified.  Function signature with explicit kind polymorphism
+     f5 :: a (b :: k) -> Int
+  This time 'k' is Specified, because it is mentioned explicitly,
+  so we get f5 :: forall (k:*) (a:k->*) (b:k). a b -> Int
+
+* Similarly pattern synonyms:
+  Invisible - from inferred types (e.g. no pattern type signature)
+            - or from inferred kind polymorphism
+
+In type declarations:
+
+* Invisible (k)
+     data T1 a b = MkT1 (a b)
+  Here T1's kind is  T1 :: forall {k:*}. (k->*) -> k -> *
+  The kind variable 'k' is Invisible, since it is not mentioned
+
+  Note that 'a' and 'b' correspond to /Anon/ TyBinders in T1's kind,
+  and Anon binders don't have a visibility flag. (Or you could think
+  of Anon having an implicit Visible flag.)
+
+* Specified (k)
+     data T2 (a::k->*) b = MkT (a b)
+  Here T's kind is  T :: forall (k:*). (k->*) -> k -> *
+  The kind vairable 'k' is Specified, since it is mentioned in
+  the signature.
+
+* Visible (k)
+     data T k (a::k->*) b = MkT (a b)
+  Here T's kind is  T :: forall k:* -> (k->*) -> k -> *
+  The kind Visible, since it bound in a positional way in T's declaration
+  Every use of T must be explicitly applied to a kind
+
+* Invisible (k1), Specified (k)
+     data T a b (c :: k) = MkT (a b) (Proxy c)
+  Here T's kind is  T :: forall {k1:*} (k:*). (k1->*) -> k1 -> k -> *
+  So 'k' is Specified, becuase it appears explicitly,
+  but 'k1' is Invisible, becuase it does not
+
+---- Printing -----
+
+ We print forall types with enough syntax to tell you their visiblity
+ flag.  But this is not source Haskell, and these types may not all
+ be parsable.
+
+ Specified: a list of Specified binders is written between `forall` and `.`:
+               const :: forall a b. a -> b -> a
+
+ Invisible: with -fprint-explicit-foralls, Invisible binders are written
+            in braces:
+               f :: forall {k} (a:k). S k a -> Int
+            Otherwise, they are printed like Specified binders.
+
+ Visible: binders are put between `forall` and `->`:
+              T :: forall k -> *
+
+---- Other points -----
+
+* In classic Haskell, all named binders (that is, the type variables in
+  a polymorphic function type f :: forall a. a -> a) have been Invisible.
+
+* Invisible variables correspond to "generalized" variables from the
+  Visible Type Applications paper (ESOP'16).
+
+Note [No Visible TyBinder in terms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We don't allow Visible foralls for term variables, including pattern
+synonyms and data constructors.  Why?  Because then an application
+would need a /compulsory/ type argument (possibly without an "@"?),
+thus (f Int); and we don't have concrete syntax for that.
 
--------------------------------------
-                Note [PredTy]
+We could change this decision, but Visible, Named TyBinders are rare
+anyway.  (Most are Anons.)
 -}
 
+instance Binary VisibilityFlag where
+  put_ bh Visible   = putByte bh 0
+  put_ bh Specified = putByte bh 1
+  put_ bh Invisible = putByte bh 2
+
+  get bh = do
+    h <- getByte bh
+    case h of
+      0 -> return Visible
+      1 -> return Specified
+      _ -> return Invisible
+
+
+{- **********************************************************************
+*                                                                       *
+                        PredType
+*                                                                       *
+********************************************************************** -}
+
+
 -- | A type of the form @p@ of kind @Constraint@ represents a value whose type is
 -- the Haskell predicate @p@, where a predicate is what occurs before
 -- the @=>@ in a Haskell type.
@@ -494,6 +595,7 @@ The predicate really does turn into a real extra argument to the
 function.  If the argument has type (p :: Constraint) then the predicate p is
 represented by evidence of type p.
 
+
 %************************************************************************
 %*                                                                      *
             Simple constructors
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index b980c9bd0b..787da10a3c 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -307,7 +307,6 @@ This is important. In an instance declaration we expect
 
 Note [TyCon Role signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 Every tycon has a role signature, assigning a role to each of the tyConTyVars
 (or of equal length to the tyConArity, if there are no tyConTyVars). An
 example demonstrates these best: say we have a tycon T, with parameters a at
@@ -342,7 +341,6 @@ datacon arity were the same.
 
 Note [Injective type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 We allow injectivity annotations for type families (both open and closed):
 
   type family F (a :: k) (b :: k) = r | r -> a
@@ -397,19 +395,11 @@ data TyCon
 
         tyConName   :: Name,     -- ^ Name of the constructor
 
+        -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-
-        tyConResKind :: Kind,       -- ^ Cached result kind
-
-        tyConKind   :: Kind,     -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity  :: Arity,    -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
         tcRepName :: TyConRepName
     }
@@ -434,23 +424,16 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
+        -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-
-        tyConResKind :: Kind,       -- ^ Cached result kind
-
-        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
+        -- See Note [tyConTyVars and tyConBinders]
         tyConTyVars  :: [TyVar], -- ^ The kind and type variables used in the
                                  -- type constructor.
-                                 -- Invariant: length tyvars = arity
+                                 -- Invariant: length tyConTyVars = tyConArity
                                  -- Precisely, this list scopes over:
                                  --
                                  -- 1. The 'algTcStupidTheta'
@@ -461,7 +444,7 @@ data TyCon
                                  -- constructors.
 
         tcRoles      :: [Role],  -- ^ The role for each type variable
-                                 -- This list has the same length as tyConTyVars
+                                 -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
         tyConCType   :: Maybe CType,-- ^ The C type that should be used
@@ -504,26 +487,19 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
+        -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-
-        tyConResKind :: Kind,     -- ^ Cached result kind.
-
-        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
+        -- See Note [tyConTyVars and tyConBinders]
         tyConTyVars  :: [TyVar], -- ^ List of type and kind variables in this
                                  -- TyCon. Includes implicit kind variables.
-                                 -- Invariant: length tyConTyVars = tyConArity
+                                 -- Scopes over: synTcRhs
 
         tcRoles      :: [Role],  -- ^ The role for each type variable
-                                 -- This list has the same length as tyConTyVars
+                                 -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
         synTcRhs     :: Type     -- ^ Contains information about the expansion
@@ -539,31 +515,18 @@ data TyCon
 
         tyConName    :: Name,    -- ^ Name of the constructor
 
+        -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-
-        tyConResKind :: Kind,     -- ^ Cached result kind
-
-        tyConKind    :: Kind,    -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity   :: Arity,   -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
+        -- See Note [tyConTyVars and tyConBinders]
         tyConTyVars  :: [TyVar], -- ^ The kind and type variables used in the
                                  -- type constructor.
                                  -- Invariant: length tyvars = arity
-                                 -- Precisely, this list scopes over:
-                                 --
-                                 -- 1. The 'algTcStupidTheta'
-                                 -- 2. The cached types in 'algTyConRhs.NewTyCon'
-                                 -- 3. The family instance types if present
-                                 --
-                                 -- Note that it does /not/ scope over the data
-                                 -- constructors.
+            -- Needed to connect an associated family TyCon
+            -- with its parent class; see TcValidity.checkConsistentFamInst
 
         famTcResVar  :: Maybe Name,   -- ^ Name of result type variable, used
                                       -- for pretty-printing with --show-iface
@@ -593,22 +556,14 @@ data TyCon
 
         tyConName     :: Name,   -- ^ Name of the constructor
 
+        -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-
-        tyConResKind   :: Kind,      -- ^ Cached result kind
-
-        tyConKind     :: Kind,   -- ^ Kind of this TyCon (full kind, not just
-                                 -- the return kind)
-
-        tyConArity    :: Arity,  -- ^ Number of arguments this TyCon must
-                                 -- receive to be considered saturated
-                                 -- (including implicit kind variables)
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
 
         tcRoles       :: [Role], -- ^ The role for each type variable
-                                 -- This list has the same length as tyConTyVars
+                                 -- This list has length = tyConArity
                                  -- See also Note [TyCon Role signatures]
 
         isUnlifted   :: Bool,    -- ^ Most primitive tycons are unlifted (may
@@ -622,34 +577,32 @@ data TyCon
 
   -- | Represents promoted data constructor.
   | PromotedDataCon {          -- See Note [Promoted data constructors]
-        tyConUnique   :: Unique, -- ^ Same Unique as the data constructor
-        tyConName     :: Name,   -- ^ Same Name as the data constructor
-        tyConArity    :: Arity,
+        tyConUnique  :: Unique,     -- ^ Same Unique as the data constructor
+        tyConName    :: Name,       -- ^ Same Name as the data constructor
+
+        -- See Note [The binders/kind/arity fields of a TyCon]
         tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-        tyConResKind   :: Kind,   -- ^ Cached result kind
-        tyConKind     :: Kind,   -- ^ Type of the data constructor
-        tcRoles       :: [Role], -- ^ Roles: N for kind vars, R for type vars
-        dataCon       :: DataCon,-- ^ Corresponding data constructor
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind   :: Kind,        -- ^ Kind of this TyCon
+        tyConArity  :: Arity,       -- ^ Arity
+
+        tcRoles       :: [Role],    -- ^ Roles: N for kind vars, R for type vars
+        dataCon       :: DataCon,   -- ^ Corresponding data constructor
         tcRepName     :: TyConRepName,
         promDcRepInfo :: RuntimeRepInfo  -- ^ See comments with 'RuntimeRepInfo'
     }
 
   -- | These exist only during a recursive type/class type-checking knot.
   | TcTyCon {
-      tyConUnique :: Unique,
-      tyConName   :: Name,
-      tyConUnsat  :: Bool,  -- ^ can this tycon be unsaturated?
-      tyConArity  :: Arity,
-      tyConBinders :: [TyBinder],   -- ^ The TyBinders for this TyCon's kind.
-                                    -- length tyConBinders == tyConArity.
-                                    -- This is a cached value and is redundant with
-                                    -- the tyConKind.
-      tyConResKind :: Kind,          -- ^ Cached result kind
-
-      tyConKind   :: Kind
+        tyConUnique :: Unique,
+        tyConName   :: Name,
+        tyConUnsat  :: Bool,  -- ^ can this tycon be unsaturated?
+
+        -- See Note [The binders/kind/arity fields of a TyCon]
+        tyConBinders :: [TyBinder], -- ^ The TyBinders for this TyCon's kind.
+        tyConResKind :: Kind,       -- ^ Result kind
+        tyConKind    :: Kind,       -- ^ Kind of this TyCon
+        tyConArity   :: Arity       -- ^ Arity
       }
   deriving Typeable
 
@@ -850,7 +803,49 @@ data FamTyConFlav
    -- | Built-in type family used by the TypeNats solver
    | BuiltInSynFamTyCon BuiltInSynFamily
 
-{-
+{- Note [The binders/kind/arity fields of a TyCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+All TyCons have this group of fields
+  tyConBinders :: [TyBinder]
+  tyConResKind :: Kind
+  tyConKind    :: Kind   -- Cached = mkForAllTys tyConBinders tyConResKind
+  tyConArity   :: Arity  -- Cached = length tyConBinders
+
+They fit together like so:
+
+* tyConBinders gives the telescope of Named (forall'd)
+  Anon (ordinary ->) binders
+
+* Note that tyConBinders /includes/ Anon arguments.  For example:
+    type App a (b :: k) = a b
+      -- App :: forall {k}; (k->*) -> k -> *
+  we get
+    tyConTyBinders = [ Named (k :: *) Invisible, Anon (k->*), Anon k ]
+
+* 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.
+
+Note [tyConBinders and tyConTyVars]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  type App a (b :: k) = a b
+    -- App :: forall {k}; (k->*) -> k -> *
+
+For App we get:
+  tyConTyVars    = [ k:*,                      a:k->*,      b:k]
+  tyConTyBinders = [ Named (k :: *) Invisible, Anon (k->*), Anon k ]
+
+The tyConBinder field is used to construct the kind of App, namely
+  App :: forall {k}; (k->*) -> k -> *
+The tyConTyVars field always corresponds 1-1 with tyConBinders, and
+records the names of the binders.  That is important for type synonyms,
+etc, where those names scope over some other field in the TyCon. In
+this case, 'a' and 'b' are mentioned in the RHS.
+
 Note [Closed type families]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 * In an open type family you can add new instances later.  This is the