Explicit Specificity

Implementation for Ticket #16393.
Explicit specificity allows users to manually create inferred type variables,
by marking them with braces.
This way, the user determines which variables can be instantiated through
visible type application.

The additional syntax is included in the parser, allowing users to write
braces in type variable binders (type signatures, data constructors etc).
This information is passed along through the renamer and verified in the
type checker.
The AST for type variable binders, data constructors, pattern synonyms,
partial signatures and Template Haskell has been updated to include the
specificity of type variables.

Minor notes:
- Bumps haddock submodule
- Disables pattern match checking in GHC.Iface.Type with GHC 8.8

2 files changed, 84 insertions, 0 deletions

diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst
index 5c478b8fa4..46a729af70 100644
--- a/docs/users_guide/8.12.1-notes.rst
+++ b/docs/users_guide/8.12.1-notes.rst
@@ -79,6 +79,13 @@ Language
 
   This change prepares the way for Quick Look impredicativity.
 
+* GHC now allows users to manually define the specificity of type variable
+  binders. By marking a variable with braces ``{tyvar}`` or ``{tyvar :: kind}``,
+  it becomes inferred despite appearing in a type signature. This feature
+  effectively allows users to choose which variables can or can't be
+  instantiated through visible type application. More information can be found
+  here: :ref:`Manually-defining-inferred-variables`.
+  
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/type_applications.rst b/docs/users_guide/exts/type_applications.rst
index 2a735436d8..c175008617 100644
--- a/docs/users_guide/exts/type_applications.rst
+++ b/docs/users_guide/exts/type_applications.rst
@@ -178,4 +178,81 @@ the rules in the subtler cases:
 The section in this manual on kind polymorphism describes how variables
 in type and class declarations are ordered (:ref:`inferring-variable-order`).
 
+.. _Manually-defining-inferred-variables:
 
+Manually defining inferred variables
+------------------------------------
+
+While user-written type or kind variables are specified by default, GHC permits
+labelling these variables as inferred. By writing the type variable binder in
+braces as ``{tyvar}`` or ``{tyvar :: kind}``, the new variable will be
+classified as inferred, not specified. Doing so gives the programmer control
+over which variables can be manually instantiated and which can't.
+Note that the braces do not influence scoping: variables in braces are still
+brought into scope just the same.
+Consider for example::
+
+  myConst :: forall {a} b. a -> b -> a
+  myConst x _ = x
+
+In this example, despite both variables appearing in a type signature, ``a`` is
+an inferred variable while ``b`` is specified. This means that the expression
+``myConst @Int`` has type ``forall {a}. a -> Int -> a``.
+
+The braces are allowed in the following places:
+
+- In the type signatures of functions, variables, class methods, as well as type
+  annotations on expressions. Consider the example above.
+
+- In data constructor declarations, using the GADT syntax. Consider::
+
+    data T a where MkT :: forall {k} (a :: k). Proxy a -> T a
+
+  The constructor ``MkT`` defined in this example is kind polymorphic, which is
+  emphasized to the reader by explicitly abstracting over the ``k`` variable.
+  As this variable is marked as inferred, it can not be manually instantiated.
+
+- In existential variable quantifications, e.g.::
+
+    data HList = HNil
+               | forall {a}. HCons a HList
+
+- In pattern synonym signatures. Consider for instance::
+
+    data T a where MkT :: forall a b. a -> b -> T a
+
+    pattern Pat :: forall {c}. () => forall {d}. c -> d -> T c
+    pattern Pat x y = MkT x y
+
+  Note that in this example, ``a`` is a universal variable in the data type
+  ``T``, where ``b`` is existential. When writing the pattern synonym, both
+  types are allowed to be specified or inferred.
+
+- On the right-hand side of a type synonym, e.g.::
+
+    type Foo = forall a {b}. Either a b
+
+- In type signatures on variables bound in RULES, e.g.::
+
+    {-# RULES "parametricity" forall (f :: forall {a}. a -> a). map f = id #-}
+
+The braces are *not* allowed in the following places:
+
+- In visible dependent quantifiers. Consider::
+
+    data T :: forall {k} -> k -> Type
+
+  This example is rejected, as a visible argument should by definition be
+  explicitly applied. Making them inferred (and thus not appliable) would be
+  conflicting.
+
+- In default type signatures for class methods, in SPECIALISE pragmas or in
+  instance declaration heads, e.g.::
+
+    instance forall {a}. Eq (Maybe a) where ...
+
+  The reason for this is, essentially, that none of these define a new
+  construct. This means that no new type is being defined where specificity
+  could play a role.
+
+- On the left-hand sides of type declarations, such as classes, data types, etc.