Add support for visible foralls in lambda, \case, and \cases expressions

[RyanGlScott]

GHC 9.10 introduces the ability to use visible foralls in the types of terms. This means that the following can now be written:

idv :: forall a -> a -> a
idv (type a) (x :: a) = x
x = idv (type Int) 42

idv' :: forall a -> a -> a
idv' a (x :: a) = x
x' = idv' Int 42

This issue aims to add support for this on the th-desugar side. This turns out to be surprisingly non-trivial, however, and we will need to think a bit about the design.

Preliminaries: template-haskell–related changes

First, we need to update the relevant parts of th-desugar that interface with template-haskell. On the template-haskell side, the following changes were introduced in template-haskell-2.22.0.0 (bundled with GHC 9.10.1):

data Pat
  = ...
  | TypeP Type                      -- ^ @{ type p }@

data Exp
  = ...
  | TypeE Type                         -- ^ @{ type t }@

Naturally, we'll want to add DTypeP and DTypeE to th-desugar's ASTs as well. This proves relatively straightforward.

Challenge (1): translating lambdas and LambdaCase

Updating the th-desugar AST isn't enough to fully support embedded types in terms, however. First, consider this example:

f1 :: forall a -> a -> a
f1 (type a) (x :: a) = x :: a

th-desugar is capable of round-tripping f1 through desugaring and sweetening, as the round-tripped version will look identical to the original. However, let's change the implementation slightly:

f2 :: forall a -> a -> a
f2 = \(type a) (x :: a) -> x :: a

f2 is functionally the same as f1, but the body of f2 uses a lambda instead. This actually makes a big difference for th-desugar, since th-desugar is not capable of round-tripping f2. If you attempted to do so, you'd end up with something like this:

f2 :: forall a -> a -> a
f2 = \arg1 arg2 ->
  case (arg1, arg2) of
    (type a, x :: a) -> x :: a

This simply won't work, however, as you aren't allowed to use type a (an embedded type expression) like that. GHC will complain thusly:

error: [GHC-01928]
    • Illegal term-level use of the type variable ‘arg1’
    • In the expression: arg1
      In the expression: (arg1, arg2)
      In the expression: case (arg1, arg2) of (type a, x :: a) -> x :: a
   |
   |   case (arg1, arg2) of
   |         ^^^^

This affects not just lambda expressions, but also uses of \case. For example, given this:

f3 :: forall a -> a -> a
f3 = \case
  (type a) -> id @a

th-desugar would round-trip it to:

f3 :: forall a -> a -> a
f3 = \arg ->
  case arg of
    (type a) -> id @a

But again, GHC doesn't like this:

error: [GHC-01928]
    • Illegal term-level use of the type variable ‘arg’
    • In the expression: arg
      In the expression: case arg of (type a) -> id @a
      In the expression: \ arg -> case arg of (type a) -> id @a
   |
   |   case arg of
   |        ^^^

Similarly for \cases. If you have this:

f4 :: forall a -> a -> a
f4 = \cases
  (type a) (x :: a) -> x :: a

th-desugar will round-trip it to:

f4 :: forall a -> a -> a
f4 = \arg1 arg2 ->
  case (arg1, arg2) of
    (type a, x :: a) -> x :: a

Which fails for the same reasons as f2 above.

---

What should we do about this? One possibility is to detect embedded type patterns in lambda/LambdaCase expressions and exempt them from being included in the tuples that th-desugar generates when desugaring code. That is, round-trip this:

f2 :: forall a -> a -> a
f2 = \(type a) (x :: a) -> x :: a

To this:

f2 :: forall a -> a -> a
f2 = \(type a) arg ->
  case arg of
    (x :: a) -> x :: a

And similarly for f3 and f4. This plan doesn't quite work out of the box, however, since the definition of DLamE (th-desugar's AST for lambda expressions) is this:

data DDec
  = ...
  | DLamE [Name] DExp

This means that th-desugar's lambdas can only bind Names, not arbitrary patterns like type a. However, we are in luck, since we can bind a as a bare Name and it will still work:

f2 :: forall a -> a -> a
f2 = \a arg ->
  case arg of
    (x :: a) -> x :: a

Challenge (2): Renaming

I did something very sneaky in my fix for f2 above: I assumed that it was possible to lift out the type a pattern without needing to change the right-hand side of the lambda expression at all. That only worked in the f2 example through a fortunate coincidence, but we won't always be so lucky. Consider this more involved example:

g :: forall a -> Maybe a -> a -> a
g = \cases
  (type a1) (Just x) _ -> x :: a1
  (type a2) Nothing  y -> y :: a2

This time, we have a \cases expressions with multiple clauses, and each clause names the type variable something different a1 and a2. A naïve attempt to round-trip this might result in code that looks like this:

g :: forall a -> Maybe a -> a -> a
g = \a1 arg1 arg2 ->
  case (arg1, arg2) of
    (Just x,  _) -> x :: a1
    (Nothing, y) -> y :: a2

But this is wrong, since the a2 in y :: a2 no longer refers to the same type variable (a1) that is bound in the embedded type a1 pattern. We'd have a similar problem if we bound \a2 instead of \a1.

The only way I can think of to solve this challenge would be to rename any occurrences of bound type variables to ensure that they all refer to the same variable names. That is, desugar g to this:

g :: forall a -> Maybe a -> a -> a
g = \a1 arg1 arg2 ->
  case (arg1, arg2) of
    (Just x,  _) -> x :: a1
    (Nothing, y) -> y :: a1

Note that we now generate y :: a1 instead of y :: a2.

This is easier said than done, however, as we'd need to develop the necessary machinery for substituting into arbitrary expressions. th-desugar has some similar machinery here, but it's only suitable for substituting into types, not expressions. (See also #108.)

Challenge (3): Distinguishing type from term variables

I did yet another sneaky thing in the fix for f2 above: I assumed that it was straightforward to determine which bound variables were term variables or type variables. In the case of f2, this is obvious, since the type variable a occurs underneath a type marker. This isn't always so obvious in general, however. Consider:

h :: forall a -> a -> a
h = \a x -> x

If you look at the expression \a x -> a in isolation, it's not at all obvious whether a is a term-level or type-level variable. But we really do need to know this information, as we can't reliably desugar the expression unless we exempt a from being put into the generated tuple! Nor does the template-haskell AST tell us much: if we defined h within TemplateHaskellQuotes:

[d| h :: forall a -> a -> a
    h = \a x -> x |]

And then inspected a, we'd simply find a Name with a NameFlavour of NameU, which simply tells us that it's a unique name. Nor can we call reify on a's Name to see if it returns VarI (for term-level Names) or TyVarI (for type-level Names).

The only way I can think of solving this challenge is to look up the type signature of any lambda expression (or LambdaCase expression) that we are desugaring and use the type to determine if we are dealing with type variables or term variables. That's a pretty heavyweight solution, but I can't think of another way.

Radical idea

Many of the challenges discussed above ultimately arise from the limitation that DLamE only supports binding Names, not full patterns. As an radical alternative, we could consider changing the definition of DLamE to:

data DDec
  = ...
  | DLamE [DPat] DExp

And abandoning the whole desugar-lambdas-to-case-of-tuples plan entirely. That would avoid all of the issues above, at the expense of making DDec slightly less minimal (and perhaps making singletons-th's life harder). Is it worth it? I'm not sure.

[RyanGlScott]

Another radical idea

Inspired by this comment, we could replace DLamE and DCaseE with \cases, which might look something like:

data DExp
  = ...
  | DLamCasesE [DClause]

Most of the challenges in the comment above arise due to attempting to avoid passing embedded type expressions to intermediate tuples. Using \cases, we can avoid the need to construct intermediate tuples altogether.

Lambdas

In general, a lambda expression of the form:

\pat_1 ... pat_n -> exp

Desugars to:

\cases pat_1 ... pat_n -> exp

\case expressions

In general, a \case expression of the form:

\case
  pat_1 -> exp_1
  ...
  pat_n -> exp_n

Desugars to:

\cases
  pat_1 -> exp_1
  ...
  pat_n -> exp_n

\cases expressions

A \cases expression would round-trip back to itself.

case expressions

In general, a case expression of the form:

case exp_scrut of
  pat_1 -> exp_rhs_1
  ...
  pat_n -> exp_rhs_n

Desugars to:

(\cases
  pat_1 -> exp_rhs_1
  ...
  pat_n -> exp_rhs_n) exp_scrut

---

For more specific examples, here is how you would desugar each of the examples above:

f2

This:

f2 :: forall a -> a -> a
f2 = \(type a) (x :: a) -> x :: a

Desugars to:

f2 :: forall a -> a -> a
f2 = \cases (type a) (x :: a) -> x :: a

f3

This:

f3 :: forall a -> a -> a
f3 = \case
  (type a) -> id @a

Desugars to:

f3 :: forall a -> a -> a
f3 = \cases
  (type a) -> id @a

f4, g, and h

This:

f4 :: forall a -> a -> a
f4 = \cases
  (type a) (x :: a) -> x :: a

Would round-trip back to itself. Similarly for g and h.

---

Of course, we'd need to check to see if singletons-th would be happy with this new approach. Unlike the other radical idea above, however, I'd argue that this approach is actually more minimal than th-desugar's current approach, as we can replace DLamE and DCaseE (two separate DExp constructs) with a single language construct.

[RyanGlScott]

Some local experimentation suggests that the DLamCasesE approach could be viable, although there is a lot more work to be done to ensure that libraries like singletons-th can migrate gracefully. I've opened #210 to track this specific idea.

Unfortunately, I am doubtful that we will be able to implement #210 in time for a GHC 9.10–compatible th-desugar release. As such, I propose that we:

1. Do a very naïve desugaring of TypeP/InvisP for the next th-desugar release.
2. Acknowledge the limitations of the naïve approach in the "Known limitations" section of the README.
3. Repurpose this issue for the task of fully supporting TypeP/InvisP when desugaring lambda, \case, and \cases expressions.

The naïve approach, although limited, is perhaps not as bad as it sounds. Although you won't be able to write things like f = \(type a) (x :: a) -> x :: a, you can write f (type a) (x :: a) = x :: a instead, which is a serviceable workaround.

[RyanGlScott]

#211 implemented (1) and (2) from #204 (comment), so the only thing that remains is (3). I've retitled the issue to reflect this.