docs: update information on RequiredTypeArguments

Update the User's Guide and Release Notes to account for the recent
progress in the implementation of RequiredTypeArguments.

docs/users_guide/9.10.1-notes.rst

@@ -6,17 +6,34 @@ Version 9.10.1
 Language
 ~~~~~~~~
 
-- Part 1 of GHC Proposal `#281
-  <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
-  "Visible forall in types of terms" has been implemented.
+- GHC Proposal `#281 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
+  "Visible forall in types of terms" has been partially implemented.
   The following code is now accepted by GHC::
 
-    idv :: forall a -> a -> a
-    idv (type a) (x :: a) = x
+    {-# LANGUAGE RequiredTypeArguments #-}
 
-    x = idv (type Int) 42
+    vshow :: forall a -> Show a => a -> String
+    vshow t x = show (x :: t)
+
+    s1 = vshow Int    42      -- "42"
+    s2 = vshow Double 42      -- "42.0"
+
+  The use of ``forall a ->`` instead of ``forall a.`` indicates a *required* type
+  argument. A required type argument is visually indistinguishable from a value
+  argument but does not exist at runtime.
+
+  This feature is guarded behind :extension:`RequiredTypeArguments`.
+
+- The :extension:`ExplicitNamespaces` extension can now be used in conjunction
+  with :extension:`RequiredTypeArguments` to select the type namespace in a
+  required type argument::
+
+    data T = T               -- the name `T` is ambiguous
+    f :: forall a -> ...     -- `f` expects a required type argument
+
+    x1 = f T         -- refers to the /data/ constructor `T`
+    x2 = f (type T)  -- refers to the /type/ constructor `T`
 
-  This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
 - With :extension:`LinearTypes`, ``let`` and ``where`` bindings can
   now be linear. So the following now typechecks::
 
@@ -28,7 +45,6 @@ Language
       where
         y = f x
 
-
 - Due to an oversight, previous GHC releases (starting from 9.4) allowed the use
   of promoted data types in kinds, even when :extension:`DataKinds` was not
   enabled. That is, GHC would erroneously accept the following code: ::

docs/users_guide/exts/required_type_arguments.rst

@@ -19,42 +19,94 @@ dependent quantification in types of terms::
   id     :: forall a.   a -> a         -- invisible dependent quantification
   id_vdq :: forall a -> a -> a         --   visible dependent quantification
 
-Note that the arrow in ``forall a ->`` is part of the syntax and not a function
-arrow, just like the dot in ``forall a.`` is not a type operator. The essence of
-a ``forall`` is the same regardless of whether it is followed by a dot or an
-arrow: it introduces a type variable. But the way we bind and specify this type
-variable at the term level differs.
+The arrow in ``forall a ->`` is part of the syntax and not a function arrow,
+just like the dot in ``forall a.`` is not a type operator.
 
-When we define ``id``, we can use a lambda to bind a variable that stands for
-the function argument::
+The choice between ``forall a.`` and ``forall a ->`` does not have any effect on
+program execution. Both quantifiers introduce type variables, which are erased
+during compilation. Rather, the main difference is in the syntax used at call
+sites::
 
-  -- For reference: id :: forall a. a -> a
-  id = \x -> x
+  x1 = id       True     -- invisible forall, the type argument is inferred by GHC
+  x2 = id @Bool True     -- invisible forall, the type argument is supplied by the programmer
 
-At the same time, there is no mention of ``a`` in this definition at all. It is
-bound by the compiler behind the scenes, and that is why we call the ordinary
-``forall a.`` an *invisible* quantifier. Compare that to ``forall a ->``, which
-is considered *visible*::
+  x3 = id_vdq _    True  --   visible forall, the type argument is inferred by GHC
+  x4 = id_vdq Bool True  --   visible forall, the type argument is supplied by the programmer
 
-  -- For reference: id_vdq :: forall a -> a -> a
-  id_vdq = \(type t) x -> x
+.. _dependent-quantifier:
 
-This time we have two binders in the lambda:
-* ``type t``, corresponding to ``forall a ->`` in the signature
-* ``x``, corresponding to ``a ->`` in the signature
+Terminology: Dependent quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Both ``forall a.`` and ``forall a ->`` are said to be "dependent" because the
+result type depends on the supplied type argument: ::
+
+  id @Integer :: Integer -> Integer
+  id @String  :: String  -> String
+
+  id_vdq Integer :: Integer -> Integer
+  id_vdq String  :: String  -> String
+
+Notice how the RHS of the signature is influenced by the LHS.
+
+This is in contrast to the function arrow ``->``, which is a non-dependent
+quantifier::
+
+  putStrLn "Hello" :: IO ()
+  putStrLn "World" :: IO ()
+
+The type of ``putStrLn`` is ``String -> IO ()``. No matter what string we pass
+as input, the result type ``IO ()`` does not depend on it.
+
+This notion of dependence is weaker than the one used in dependently-typed
+languages (see :ref:`pi-types`).
+
+Terminology: Visible quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We say that ``forall a.`` is an *invisible* quantifier and ``forall a ->`` is a
+*visible* quantifier. This notion of "visibility" is unrelated to implicit
+quantification, which happens when the quantifier is omitted: ::
 
-And of course, now we also have the option of using the bound ``t`` in a
-subsequent pattern, as well as on the right-hand side of the lambda::
+  id     ::             a -> a    -- implicit quantification, invisible forall
+  id     :: forall a.   a -> a    -- explicit quantification, invisible forall
+  id_vdq :: forall a -> a -> a    -- explicit quantification,   visible forall
 
-  -- For reference: id_vdq :: forall a -> a -> a
-  id_vdq = \(type t) (x :: t) -> x :: t
-  --              ↑        ↑          ↑
-  --            bound     used       used
+The property of "visibility" actually describes whether the corresponding type
+argument is visible at the definition site and at call sites: ::
 
-At use sites, we also instantiate this type variable explicitly::
+  -- Invisible quantification
+  id :: forall a. a -> a
+  id x = x                -- defn site: `a` is not mentioned
+  call_id = id True       -- call site: `a` is invisibly instantiated to `Bool`
 
-  n = id_vdq (type Integer) 42
-  s = id_vdq (type String)  "Hello"
+  -- Visible quantification
+  id_vdq :: forall a -> a -> a
+  id_vdq t x = x                  -- defn site: `a` is visibly bound to `t`
+  call_id_vdq = id_vdq Bool True  -- call site: `a` is visibly instantiated to `Bool`
+
+In the equation for ``id`` there is just one binder on the LHS, ``x``, and it
+corresponds to the value argument, not to the type argument. Compare that with
+the definition of ``id_vdq``::
+
+  id_vdq :: forall a -> a -> a
+  id_vdq t x = x
+
+This time we have two binders on the LHS:
+
+* ``t``, corresponding to ``forall a ->`` in the signature
+* ``x``, corresponding to ``a ->`` in the signature
+
+The bound ``t`` can be used in subsequent patterns, as well as on the right-hand
+side of the equation::
+
+  id_vdq :: forall a -> a -> a
+  id_vdq t (x :: t) = x :: t
+  --     ↑       ↑         ↑
+  --   bound    used      used
+
+We use the terms "visible type argument" and "required type argument"
+interchangeably.
 
 Relation to :extension:`TypeApplications`
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -70,12 +122,12 @@ not reflected syntactically in the expression, it is invisible unless we use a
 Required type arguments are compulsory. They must appear syntactically at call
 sites::
 
-  x1 = id_vdq (type Bool) True    -- OK
-  x2 = id_vdq             True    -- not OK
+  x1 = id_vdq Bool True    -- OK
+  x2 = id_vdq      True    -- not OK
 
 You may use an underscore to infer a required type argument::
 
-  x3 = id_vdq (type _) True       -- OK
+  x3 = id_vdq _ True       -- OK
 
 That is, it is mostly a matter of syntax whether to use ``forall a.`` with type
 applications or ``forall a ->``. One advantage of required type arguments is that
@@ -92,20 +144,265 @@ With :extension:`RequiredTypeArguments`, we can imagine a slightly different API
 
   sizeOf :: forall a -> Storable a => Int
 
-If ``sizeOf`` had this type, we could write ``sizeOf (type Bool)`` without
+If ``sizeOf`` had this type, we could write ``sizeOf Bool`` without
 passing a dummy value.
 
+Required type arguments are erased during compilation. While the source program
+appears to bind and pass required type arguments alongside value arguments, the
+compiled program does not. There is no runtime overhead associated with required
+type arguments relative to the usual, invisible type arguments.
+
 Relation to :extension:`ExplicitNamespaces`
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The ``type`` keyword that we used in the examples is not actually part of
-:extension:`RequiredTypeArguments`. It is guarded behind
-:extension:`ExplicitNamespaces`. As described in the proposal, required type
-arguments can be passed without a syntactic marker, making them syntactically
-indistinguishble from ordinary function arguments::
+A required type argument is syntactically indistinguishable from a value
+argument. In a function call ``f arg1 arg2 arg3``, it is impossible to tell,
+without looking at the type of ``f``, which of the three arguments are required
+type arguments, if any.
+
+At the same time, one of the design goals of GHC is to be able to perform name
+resolution (find the binding sites of identifiers) without involving the type
+system. Consider: ::
+
+  data Ty = Int | Double | String deriving Show
+  main = print Int
+
+In this example, there are two constructors named ``Int`` in scope:
+
+* The **type constructor** ``Int`` of kind ``Type`` (imported from ``Prelude``)
+* The **data constructor** ``Int`` of type ``Ty`` (defined locally)
+
+How does the compiler or someone reading the code know that ``print Int`` is
+supposed to refer to the data constructor, not the type constructor?  In GHC,
+this is resolved as follows. Each identifier is said to occur either in
+**type syntax** or **term syntax**, depending on the surrounding syntactic
+context::
+
+  -- Examples of X in type syntax
+  type T = X      -- RHS of a type synonym
+  data D = MkD X  -- field of a data constructor declaration
+  a :: X          -- RHS of a type signature
+  b = f (c :: X)  -- RHS of a type signature (in expressions)
+  f (x :: X) = x  -- RHS of a type signature (in patterns)
+
+  -- Examples of X in term syntax
+  c X = a         -- LHS of a function equation
+  c a = X         -- RHS of a function equation
+
+One could imagine the entire program "zoned" into type syntax and term syntax,
+each zone having its own rules for name resolution:
+
+* In type syntax, type constructors take precedence over data constructors.
+* In term syntax, data constructors take precedence over type constructors.
+
+This means that in the ``print Int`` example, the data constructor is selected
+solely based on the fact that the ``Int`` occurs in term syntax. This is firmly
+determined before GHC attempts to type-check the expression, so the type of
+``print`` does not influence which of the two ``Int``\s is passed to it.
+
+This may not be the desired behavior in a required type argument. Consider::
+
+  vshow :: forall a -> Show a => a -> String
+  vshow t x = show (x :: t)
+
+  s1 = vshow Int    42      -- "42"
+  s2 = vshow Double 42      -- "42.0"
+
+The function calls ``vshow Int 42`` and ``vshow Double 42`` are written in
+*term* syntax, while the intended referents of ``Int`` and ``Double`` are the
+respective *type* constructors. As long as there are no data constructors named
+``Int`` or ``Double`` in scope, the example works as intended. However, if such
+clashing constructor names are introduced, they may disrupt name resolution::
+
+  data Ty = Int | Double | String
+
+  vshow :: forall a -> Show a => a -> String
+  vshow t x = show (x :: t)
+
+  s1 = vshow Int    42      -- error: Expected a type, but ‘Int’ has kind ‘Ty’
+  s2 = vshow Double 42      -- error: Expected a type, but ‘Double’ has kind ‘Ty’
+
+In this example the intent was to refer to ``Int`` and ``Double`` as types, but
+the names were resolved in favor of data constructors, resulting in type errors.
+
+The example can be fixed with the help of :extension:`ExplicitNamespaces`, which
+allows embedding type syntax into term syntax using the ``type`` keyword::
+
+  s1 = vshow (type Int)    42
+  s2 = vshow (type Double) 42
+
+A similar problem occurs with list and tuple syntax. In type syntax, ``[a]`` is
+the type of a list, i.e. ``Data.List.List a``. In term syntax, ``[a]`` is a
+singleton list, i.e. ``a : []``. A naive attempt to use the list type as a
+required type argument will result in a type error::
+
+  s3 = vshow [Int] [1,2,3]  -- error: Expected a type, but ‘[Int]’ has kind ‘[Type]’
+
+The problem is that GHC assumes ``[Int]`` to stand for ``Int : []`` instead of
+the intended ``Data.List.List Int``. This, too, can be solved using the ``type`` keyword::
+
+  s3 = vshow (type [Int]) [1,2,3]
+
+Since the ``type`` keyword is merely a namespace disambiguation mechanism, it
+need not apply to the entire type argument. Using it to disambiguate only a part
+of the type argument is also valid::
+
+  f :: forall a -> ...   -- `f`` is a function that expects a required type argument
+
+  r1 = f (type (Either () Int))           -- `type` applied to the entire type argument
+  r2 = f (Either (type ()) Int)           -- `type` applied to one part of it
+  r3 = f (Either (type ()) (type Int))    -- `type` applied to multiple parts
+
+That is, the expression ``Either (type ()) (type Int)`` does *not* indicate that
+``Either`` is applied to two type arguments; rather, the entire expression is a
+single type argument and ``type`` is used to disambiguate parts of it.
+
+Outside a required type argument, it is illegal to use ``type``:
+::
+
+  r4 = type Int  -- illegal use of ‘type’
+
+Finally, there are types that require the ``type`` keyword only due to
+limitations of the current implementation::
+
+  a1 = f (type (Int -> Bool))                       -- function type
+  a2 = f (type (Read T => T))                       -- constrained type
+  a3 = f (type (forall a. a))                       -- universally quantified type
+  a4 = f (type (forall a. Read a => String -> a))   -- a combination of the above
+
+This restriction will be relaxed in a future release of GHC.
+
+Effect on implicit quantification
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit quantification is said to occur when GHC inserts an implicit ``forall``
+to bind type variables::
+
+  const :: a -> b -> a               -- implicit quantification
+  const :: forall a b. a -> b -> a   -- explicit quantification
+
+Normally, implicit quantification is unaffected by term variables in scope:
+::
+  f a = ...  -- the LHS binds `a`
+    where const :: a -> b -> a
+             -- implicit quantification over `a` takes place
+             -- despite the `a` bound on the LHS of `f`
+
+When :extension:`RequiredTypeArguments` is in effect, names bound in term syntax
+are not implicitly quantified. This allows us to accept the following example: ::
+
+  readshow :: forall a -> (Read a, Show a) => String -> String
+  readshow t s = show (read s :: t)
+
+  s1 = readshow Int    "42"      -- "42"
+  s2 = readshow Double "42"      -- "42.0"
+
+Note how ``t`` is bound on the LHS of a function equation (term syntax), and
+then used in a type annotation (type syntax). Under the usual rules for implicit
+quantification, the ``t`` would have been implicitly quantified: ::
+
+  -- RequiredTypeArguments
+  readshow t s = show (read s :: t)   -- the `t` is captured
+  --       ↑                     ↑
+  --      bound                 used
+
+  -- NoRequiredTypeArguments
+  readshow t s = show (read s :: t)   -- the `t` is implicitly quantified as follows:
+  readshow t s = show (read s :: forall t. t)
+  --       ↑                            ↑  ↑
+  --      bound                      bound used
+
+On the one hand, taking the current scope into account allows us to accept
+programs like the one above. On the other hand, some existing programs will no
+longer compile: ::
+
+  a = 42
+  f :: a -> a    -- RequiredTypeArguments: the top-level `a` is captured
+
+Because of that, merely enabling :extension:`RequiredTypeArguments` might lead
+to type errors of this form::
+
+  Term variable ‘a’ cannot be used here
+    (term variables cannot be promoted)
+
+There are two possible ways to fix this error::
+
+  a = 42
+  f1 :: b -> b              -- (1) use a different variable name
+  f2 :: forall a. a -> a    -- (2) use an explicit forall
+
+If you are converting a large codebase to be compatible with
+:extension:`RequiredTypeArguments`, consider using
+:ghc-flag:`-Wterm-variable-capture` during the migration. It is a warning that
+detects instances of implicit quantification incompatible with
+:extension:`RequiredTypeArguments`: ::
+
+  The type variable ‘a’ is implicitly quantified,
+  even though another variable of the same name is in scope:
+    ‘a’ defined at ...
+
+.. _pi-types:
+
+Relation to Π-types
+~~~~~~~~~~~~~~~~~~~
+
+Both ``forall a.`` and ``forall a ->`` are dependent quantifiers in the narrow
+sense defined in :ref:`dependent-quantifier`. However, neither of them
+constitutes a dependent function type (Π-type) that might be familiar to users
+coming from dependently-typed languages or proof assistants.
+
+* Haskell has always had functions whose result *value* depends on
+  the argument *value*::
+
+    not True  = False   -- argument value: True;  result value: False
+    (*2) 5    = 10      -- argument value: 5;     result value: 10
+
+  This captures the usual idea of a function, denoted ``a -> b``.
+
+* Haskell also has functions whose result *type* depends on the argument *type*:
+  ::
+
+    id    @Int  :: Int  -> Int    -- argument type: Int;  result type: Int  -> Int
+    id_vdq Bool :: Bool -> Bool   -- argument type: Bool; result type: Bool -> Bool
+
+  This captures the idea of parametric polymorphism, denoted ``forall a. b`` or
+  ``forall a -> b``.
+
+* Furthermore, Haskell has functions whose result *value* depends on the
+  argument *type*::
+
+    maxBound @Int8   = 127    -- argument type: Int8;  result value: 127
+    maxBound @Int16  = 32767  -- argument type: Int16; result value: 32767
+
+  This captures the idea of ad-hoc (class-based) polymorphism,
+  denoted ``C a => b``.
+
+* However, Haskell does **not** have direct support for functions whose result
+  *type* depends on the argument *value*. In the literature, these are often
+  called "dependent functions", or "Π-types".
+
+  Consider: ::
+
+    type F :: Bool -> Bool
+    type family F b where
+      F True  = ...
+      F False = ...
+
+    f :: Bool -> Bool
+    f True  = ...
+    f False = ...
+
+  In this example, we define a type family ``F`` to pattern-match on ``b`` at
+  the type level; and a function ``f`` to pattern-match on ``b`` at the term
+  level. However, it is impossible to quantify over ``b`` in such a way that
+  both ``F`` and ``f`` could be applied to it::
+
+    depfun :: forall (b :: Bool) -> F b  -- Allowed
+    depfun b = ... (f b) ...             -- Not allowed
 
-  n = id_vdq Integer 42
+  It is illegal to pass ``b`` to ``f`` because ``b`` does not exist at runtime.
+  Types and type arguments are erased before runtime.
 
-In this example we pass ``Integer`` as opposed to ``(type Integer)``.
-This means that :extension:`RequiredTypeArguments` is not tied to the ``type``
-syntax, which belongs to :extension:`ExplicitNamespaces`.
\ No newline at end of file
+The :extension:`RequiredTypeArguments` extension does not add dependent
+functions, which would be a much bigger step. Rather :extension:`RequiredTypeArguments`
+just makes it possible for the type arguments of a function to be compulsory.
\ No newline at end of file

docs/users_guide/using-warnings.rst

@@ -2440,8 +2440,8 @@ of ``-W(no-)*``.
     For example: ::
 
        a = 15
-       f :: a -> a    -- Does ‘a’ refer to the term-level binding
-                      -- or is it implicitly quantified?
+       f :: a -> a    -- NoRequiredTypeArguments: The ‘a’ is implicitly quantified
+                      -- RequiredTypeArguments:   The ‘a’ refers to the term-level binding
 
     When :ghc-flag:`-Wterm-variable-capture` is enabled, GHC warns against implicit quantification
     that would stop working under :extension:`RequiredTypeArguments`.