Clean up and simplify the treatment of implicit binding

principles.rst

@@ -47,6 +47,7 @@ Accepted principles
 
 .. _`#281`: proposals/0281-visible-forall.rst
 .. _`#378`: proposals/0378-dependent-type-design.rst
+.. _`#425`: proposals/0425-decl-invis-binders.rst
 .. _`#448`: proposals/0448-type-variable-scoping.rst
 
 Syntax
@@ -158,32 +159,108 @@ there is an absence of punning.
 Name resolution and scoping
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
+Explicit Binding Principle (EBP)
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+.. _`Explicit Binding Principle`:
+
+**Principle**: Through the right combination of extensions, every implicit form of variable binding
+is must have an explicit equivalent that, regardless of the context, is unambiguously a binding site.
+
+Examples:
+
+#. Problem::
+
+     -- Assume no `a` in scope
+
+     id :: a -> a  -- The variable `a` has no explicit binding site.
+
+   Solution::
+
+     -- Assume no `a` in scope
+
+     id :: forall a. a -> a  -- The `a` in `forall a.` is an explicit binding site.
+
+   This is provided by ``-XExplicitForAll``, which predates the GHC proposal process.
+
+#. Problem::
+
+     -- Assume no `a` in scope
+
+     data Foo (a :: k)
+
+   Solution::
+
+     data Foo @k (a :: k)
+
+   This is provided by ``-XTypeAbstractions`` from `#425`_.
+
+#. Problem::
+
+     -- Assume no `b` in scope
+
+     f :: (Bool, Bool) -> Bool
+     f (x :: (b, b)) = ...   -- The variable `b` has no implicit binding site.
+
+   We could declare one or both of the ``b`` occurrences above a binding site,
+   as was the historical interpretation of this, but that doesn't help as this
+   syntax isn't unambiguously a binding site regardless of context (i.e.
+   regardless of whether there is a ``b`` already in scope).
+
+*Motivation:* The `Explicit Binding Principle`_ allows programmers to control exactly how variables come into
+scope.
+It ensures all short-hands can be explained in terms of an explicit, unambiguous equivalent that is easier to understand at the cost of being more verbose:
+
+- Positive-position signatures' free vars cause  implicit ``forall ... .``
+
+- Negative position free vars cause different sorts of binding:
+
+  - Signatures on term patterns (pattern signatures) cause implicit ``let type ... = _ in``
+
+  - Signatures on type variables (kind signatures) case implicit ``@...``
+
+From `#425`_, `#448`_.
+
 Lexical Scoping Principle (LSP)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
 .. _`Lexical Scoping Principle`:
 
 **Principle**:
 
-a. For every appearance of
-an identifier, it is possible to determine whether that appearance is a *binding site*
-or an *occurrence* without examining the context.
+a. For every appearance of an identifier, it is possible to determine whether that appearance is
+   a mere *occurrence*, and thus must be bound elsewhere for the program to be valid.
+   or the variable is a *binding site* (or causes an implicit binding site, basically the same thing).
+
+without examining the context.
 
 b. For every *occurrence* of an
 identifier, it is possible to uniquely identify its *binding site*, without
 involving the type system.
 
+This builds upon the `Explicit Binding Principle`_:
+whereas that former principle ensures that explicit alternatives to implicit binding constructs *exist at all*,
+this latter principle makes those explicit alternatives *compulsory*, because we must not have implicit binding in order to uphold this principle.
+
 The `Lexical Scoping Principle`_ is almost true today, with the following nuances:
 
-1. Template Haskell splices may need to be run before completing name resolution (and running those splices requires type-checking them).
+#. Template Haskell splices may need to be run before completing name resolution (and running those splices requires type-checking them).
+
+#. The `deprecated mechanism <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/duplicate_record_fields.html#selector-functions>`_ for disambiguating duplicate record fields violates the `Lexical Scoping Principle`_ by requiring the type system.
+
+#. In a pattern signature, if we have ``f (x :: Maybe a)``, the ``a``
+   is an occurrence if ``a`` is already in scope, and is implicitly bound otherwise.
 
-2. The `deprecated mechanism <https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/duplicate_record_fields.html#selector-functions>`_ for disambiguating duplicate record fields violates the `Lexical Scoping Principle`_ by requiring the type system.
+#. In a type signature, if we have ``f :: a -> a``, the ``a``
+   is an occurrence if ``a`` is already in scope, and it implicitly bound otherwise.
 
-3. In a pattern signature, if we have ``f (x :: Maybe a)``, the ``a``
-   is an occurrence if ``a`` is already in scope, and it is a binding site otherwise.
+#. In a kind signature, if we have ``data Foo (a :: k)``, the ``k``
+   is an occurrence if ``k`` is already in scope (historically impossible), and it implicitly bound otherwise.
 
-4. In a type signature, any out-of-scope variable is implicitly bound. This is not
-   technically a violation of this principle (the seemingly-unbound identifier in the type signature
+   Technically this might be a violation of this principle as the ``k`` is in fact always a use with the implicit bind coming before,
+   but implicit foot-gun behavior
+
+   (the seemingly-unbound identifier in the type signature
    is always an occurrence), but it's worth noting here.
 
 *Motivation:* These principles mean that we can understand the binding
@@ -197,31 +274,6 @@ variables and imported term variables.
 
 (a) from `#448`_; (b) from `#378`_.
 
-Explicit Binding Principle (EBP)
-^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-.. _`Explicit Binding Principle`:
-
-**Principle**: Through the right combination of extensions and/or warning flags, it is possible
-for a Haskell programmer to ensure that all identifiers in a program have an explicit binding site.
-
-Examples::
-
-   id :: a -> a    -- the variable `a` has no explicit binding site, but we can write `forall a.` to provide one
-
-   f :: (Bool, Bool) -> Bool
-   f (x :: (b, b)) = ...   -- the variable `b` is bound to `Bool` by this
-                           -- pattern signature. But either the first b is a binding
-                           -- site, in violation of the Lexical Scoping Principle (a),
-                           -- or there is no explicit binding site, in violation of
-                           -- the Explicit Binding Principle.
-
-*Motivation:* The `Explicit Binding Principle`_ allows programmers to control exactly how variables come into
-scope. It also prevents the possibility of typos that accidentally introduce new
-variables.
-
-From `#448`_.
-
 Contiguous Scoping Principle (CSP)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
@@ -296,4 +348,4 @@ advanced features even when writing simple code. In addition, the existence of a
 down GHC even when those features are not active. Yet this principle is important to keep in mind going forward,
 as we hope not to make the current situation worse.
 
-From `#378`_, slightly generalized.
+From `#378`_, slightly generalized.

proposals/0425-decl-invis-binders.rst

@@ -621,6 +621,15 @@ The proposed changes provide the programmer with a more principled way of
 brining type variables into scope in certain corner cases, simplify arity
 inference and scoping rules.
 
+This gets us closer to upholding two principles:
+
+- The `Explicit Binding Principle`_, because the new ``@``-binders is explicit unlike previous alternatives
+
+- The `Lexical Scoping Principle`_, because the new simplified rules about variables needing to occur on the LHS in certain situations.
+
+.. _`Explicit Binding Principle`: ../principles.rst#explicit-binding-principle
+.. _`Lexical Scoping Principle`: ../principles.rst#lexical-scoping-principle
+
 Costs and Drawbacks
 -------------------