Andrei Borzenkov authored Aug 16, 2023 and Marge Bot committed Feb 19, 2024

GHC Proposal 448 introduces binders for invisible type arguments
(@a-binders) in various contexts. This patch implements @-binders
in lambda patterns and function equations:

  {-# LANGUAGE TypeAbstractions #-}

  id1 :: a -> a
  id1 @t x = x :: t      -- @t-binder on the LHS of a function equation

  higherRank :: (forall a. (Num a, Bounded a) => a -> a) -> (Int8, Int16)
  higherRank f = (f 42, f 42)

  ex :: (Int8, Int16)
  ex = higherRank (\ @a x -> maxBound @a - x )
                         -- @a-binder in a lambda pattern in an argument
                         -- to a higher-order function

Syntax
------

To represent those @-binders in the AST, the list of patterns in Match
now uses ArgPat instead of Pat:

  data Match p body
     = Match {
         ...
-        m_pats  :: [LPat p],
+        m_pats  :: [LArgPat p],
         ...
   }

+ data ArgPat pass
+   = VisPat (XVisPat pass) (LPat pass)
+   | InvisPat (XInvisPat pass) (HsTyPat (NoGhcTc pass))
+   | XArgPat !(XXArgPat pass)

The VisPat constructor represents patterns for visible arguments,
which include ordinary value-level arguments and required type arguments
(neither is prefixed with a @), while InvisPat represents invisible type
arguments (prefixed with a @).

Parser
------

In the grammar (Parser.y), the lambda and lambda-cases productions of
aexp non-terminal were updated to accept argpats instead of apats:

  aexp : ...
-        | '\\' apats '->' exp
+        | '\\' argpats '->' exp
         ...
-        | '\\' 'lcases' altslist(apats)
+        | '\\' 'lcases' altslist(argpats)
         ...

+ argpat : apat
+        | PREFIX_AT atype

Function left-hand sides did not require any changes to the grammar, as
they were already parsed with productions capable of parsing @-binders.
Those binders were being rejected in post-processing (isFunLhs), and now
we accept them.

In Parser.PostProcess, patterns are constructed with the help of
PatBuilder, which is used as an intermediate data structure when
disambiguating between FunBind and PatBind. In this patch we define
ArgPatBuilder to accompany PatBuilder. ArgPatBuilder is a short-lived
data structure produced in isFunLhs and consumed in checkFunBind.

Renamer
-------

Renaming of @-binders builds upon prior work on type patterns,
implemented in 2afbddb0, which guarantees proper scoping and
shadowing behavior of bound type variables.

This patch merely defines rnLArgPatsAndThen to process a mix of visible
and invisible patterns:

+ rnLArgPatsAndThen :: NameMaker -> [LArgPat GhcPs] -> CpsRn [LArgPat GhcRn]
+ rnLArgPatsAndThen mk = mapM (wrapSrcSpanCps rnArgPatAndThen) where
+   rnArgPatAndThen (VisPat x p)    = ... rnLPatAndThen ...
+   rnArgPatAndThen (InvisPat _ tp) = ... rnHsTyPat ...

Common logic between rnArgPats and rnPats is factored out into the
rn_pats_general helper.

Type checker
------------

Type-checking of @-binders builds upon prior work on lazy skolemisation,
implemented in f5d3e03c.

This patch extends tcMatchPats to handle @-binders. Now it takes and
returns a list of LArgPat rather than LPat:

  tcMatchPats ::
              ...
-             -> [LPat GhcRn]
+             -> [LArgPat GhcRn]
              ...
-             -> TcM ([LPat GhcTc], a)
+             -> TcM ([LArgPat GhcTc], a)

Invisible binders in the Match are matched up with invisible (Specified)
foralls in the type. This is done with a new clause in the `loop` worker
of tcMatchPats:

  loop :: [LArgPat GhcRn] -> [ExpPatType] -> TcM ([LArgPat GhcTc], a)
  loop (L l apat : pats) (ExpForAllPatTy (Bndr tv vis) : pat_tys)
    ...
    -- NEW CLAUSE:
    | InvisPat _ tp <- apat, isSpecifiedForAllTyFlag vis
    = ...

In addition to that, tcMatchPats no longer discards type patterns. This
is done by filterOutErasedPats in the desugarer instead.

x86_64-linux-deb10-validate+debug_info
Metric Increase:
    MultiLayerModulesTH_OneShot