[Git][ghc/ghc][wip/sand-witch/pattern- at a-binders] Add note about left-to-right scoping

[Andrei Borzenkov (@sand-witch)]

Andrei Borzenkov pushed to branch wip/sand-witch/pattern- at a-binders at Glasgow Haskell Compiler / GHC


Commits:
42891dd2 by Andrei Borzenkov at 2023-07-11T22:33:59+04:00
Add note about left-to-right scoping

- - - - -


1 changed file:

- compiler/GHC/Rename/Pat.hs


Changes:

=====================================
compiler/GHC/Rename/Pat.hs
=====================================
@@ -1116,6 +1116,7 @@ rnHsTyPat ctxt sigType = case sigType of
 -- For the OccSet in the ReaderT, see Note [Locally bound names in type patterns]
 -- For the HsTyPatRnBuilderRn in the WriterT, see Note [Implicit and explicit type variable binders]
 -- For the CpsRn base monad, see Note [CpsRn monad]
+-- For why we need CpsRn in TPRnM see Note [Left-to-right scoping of type patterns]
 newtype TPRnM a =
   MkTPRnM (ReaderT (HsDocContext, OccSet) (WriterT HsTyPatRnBuilder CpsRn) a)
   deriving newtype (Functor, Applicative, Monad)
@@ -1422,4 +1423,68 @@ as `collectPatBinders` and `tcHsTyPat`, so we store it in the extension field of
 
 To collect lists of those variables efficiently we use `HsTyPatRnBuilder` which is exactly like
 `HsTyPatRn`, but uses Bags.
+
+Note [Left-to-right scoping of type patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In term-level patterns, we use continuation passing to implement left-to-right
+scoping, see Note [CpsRn monad]. Left-to-right scoping manifests itself when
+e.g. view patterns are involved:
+
+  f (x, g x -> Just y) = ...
+
+Here the first occurrence of `x` is a binder, and the second occurrence is a
+use of `x` in a view pattern. This example does not work if we swap the
+components of the tuple:
+
+  f (g x -> Just y, x) = ...
+  --  ^^^
+  -- Variable not in scope: x
+
+In type patterns there are no view patterns, but there is a different feature
+that is served well by left-to-right scoping: kind annotations. Compare:
+
+  f (Proxy @(T k (a :: k))) = ...
+  g (Proxy @(T (a :: k) k)) = ...
+
+In `f`, the first occurrence of `k` is an explicit binder,
+  and the second occurrence is a usage. Simple.
+In `g`, the first occurrence of `k` is an implicit binder,
+  and then the second occurrence is an explicit binder that shadows it.
+
+So we get two different results after renaming:
+
+  f (Proxy @(T k1 (a :: k1))) = ...
+  g (Proxy @(T (a :: k1) k2)) = ...
+
+This makes GHC accept the first example but rejects the second example with an
+error about duplicate binders.
+
+One could argue that we don't want order-sensitivity here. Historically, we
+used a different principle when renaming types: collect all free variables,
+bind them on the outside, and then rename all occurrences as usages.
+This approach does not scale to multiple patterns. Consider:
+
+  f' (MkP @k @(a :: k)) = ...
+  g' (MkP @(a :: k) @k) = ...
+
+Here a difference in behavior is inevitable, as we rename type patterns
+one at a time. Could we perhaps concatenate the free variables from all
+type patterns in a ConPat? But then we still get the same problem one level up,
+when we have multiple patterns in a function LHS
+
+  f'' (Proxy @k) (Proxy @(a :: k)) = ...
+  g'' (Proxy @(a :: k)) (Proxy @k) = ...
+
+And if we tried to provide order sensitivity at this level, then we'd still be left
+with lambdas:
+
+  f''' (Proxy @k)        = \(Proxy @(a :: k)) -> ...
+  g''' (Proxy @(a :: k)) = \(Proxy @k)        -> ...
+
+
+So we have at least three options where we could do free variable extraction:
+HsConPatTyArg, ConPat, or a Match (used to represent a function LHS). And none
+of those would be general enough. Rather than make an arbitrary choice, we
+embrace left-to-right scoping in types and implement it with CPS, just like
+it's done for view patterns in terms.
 -}



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42891dd2e9cbf9c7e71635f6f93ae85cce5c180e

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/42891dd2e9cbf9c7e71635f6f93ae85cce5c180e
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230711/54998806/attachment-0001.html>