Visible forall in GADTs

GHC Proposal #281 says

Data constructors. When RequiredTypeArguments is in effect, allow forall a -> in data constructor declarations.

Example:

data T a where
  MkT :: forall a -> a -> T a

At the moment, GHC does not support this and prints the following error message:

Test.hs:4:10: error: [GHC-51580]
    • Illegal visible, dependent quantification in the type of a term
    • In the definition of data constructor ‘MkT’

There's some interplay between this task and #18389. Here let's focus on adding support for forall tvs -> occurring before any term-level arguments. E.g. the following is out of scope of this ticket

data NestedQuant a where
  MkNestedQuant :: Int -> forall a -> a -> T a
  --               ^^^^^^
  --        term argument before a `forall`,
  --        save that for #18389

Back to the MkT example. In expressions, we should be able to pass the visible type argument:

t1 = MkT Int 42
t2 = MkT String "hello"
t3 = MkT (Int -> Bool) even

Similarly at the type level with DataKinds

type T1 = MkT Natural 42
type T2 = MkT Symbol "hello"
type T3 = MkT (Type -> Constraint) Num

And in patterns we should be able to bind it to a variable or unify with a type pattern

f1 (MkT a x) = ...            -- f1 :: forall {a}. T a -> ...
f2 (MkT Int n) = ...          -- f2 :: T Int -> ...
f3 (MkT (w -> Bool) g) = ...  -- f3 :: forall {w}. T (w -> Bool) -> ...

The implementation will require updating at least the following definitions:

• con_bndrs in ConDeclGADT will have to be updated to allow visible foralls alongside invisible foralls.

  E.g. forall a b. forall c -> forall d.

  #18389 may further generalize it to allow mixing foralls and function arrows ->, but here we keep it simple and assume all foralls are at the front.

  Done in fbc0b92a.

• PrefixCon in HsConDetails can no longer assume that all type arguments can be syntactically identified and separated from term arguments

  E.g. in f1 (MkT a x) = ... the a is a type argument and x is a term argument. Put them all in a single list. The type checker may still assume that type arguments all come before term arguments until #18389 removes this assumption, but the AST can't distinguish them.

  Done in 7b84c588, with a residual issue about TH #25842

• Pat needs to be extended with type syntax, and pat_to_type_pat updated to handle it.

  This should allow us to accept the f3 (MkT (w -> Bool) g) = ... example.

  PsErrTypeSyntaxInPat becomes outdated with this change and can be removed.

---

The examples in this ticket have been validated to work with TypeAbstractions

{-# LANGUAGE TypeAbstractions, DataKinds #-}

import Data.Kind
import GHC.TypeLits

data T a where
  MkT :: forall a. a -> T a

t1 = MkT @Int 42
t2 = MkT @String "hello"
t3 = MkT @(Int -> Bool) even

type T1 = MkT @Nat 42
type T2 = MkT @Symbol "hello"
type T3 = MkT @(Type -> Constraint) Num

f1 (MkT @a x) = x :: a
f2 (MkT @Int n) = n*2
f3 (MkT @(w -> Bool) g) = not . g

Now let's drop those @s!