Allow promoting and singling of visible type applications in data constructor patterns

[RyanGlScott]

GHC 9.2 introduces the ability to have visible type applications in data constructor patterns like so:

blah :: Maybe a -> [a]
blah (Just @a x)  = [x :: a]
blah (Nothing @a) = [] :: [a]

Can we promote and single such a definition in singletons? While supporting visible type applications in their full generality in singletons is challenging (see #378), visible type applications in data constructor patterns are a relatively self-contained, well behaved part of TypeApplications. This is because singletons can reliably guarantee that promoted and singled data constructors will have the same behavior vis-à-vis visible type applications as their term-level counterparts (see #408), which means that as long as we restrict ourselves to data constructors, the TypeApplications-related issues mentioned in #378 shouldn't arise.

Here is a first attempt at implementing this:

diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs
index 373c35e..cb889b4 100644
--- a/singletons-th/src/Data/Singletons/TH/Promote.hs
+++ b/singletons-th/src/Data/Singletons/TH/Promote.hs
@@ -1051,12 +1051,11 @@ promotePat (DVarP name) = do
   tell $ PromDPatInfos [(name, tyName)] OSet.empty
   return (DVarT tyName, ADVarP name)
 promotePat (DConP name tys pats) = do
-  unless (null tys) $
-    qReportWarning "Visible type applications in patterns are ignored by `singletons-th`."
   opts <- getOptions
+  kis <- traverse promoteType tys
   (types, pats') <- mapAndUnzipM promotePat pats
   let name' = promotedDataTypeOrConName opts name
-  return (foldType (DConT name') types, ADConP name pats')
+  return (foldType (foldl DAppKindT (DConT name') kis) types, ADConP name kis pats')
 promotePat (DTildeP pat) = do
   qReportWarning "Lazy pattern converted into regular pattern in promotion"
   second ADTildeP <$> promotePat pat
diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs
index 6096539..e8564b8 100644
--- a/singletons-th/src/Data/Singletons/TH/Single.hs
+++ b/singletons-th/src/Data/Singletons/TH/Single.hs
@@ -790,9 +790,9 @@ singPat var_proms = go
                   Just tyname -> return tyname
       pure $ DVarP (singledValueName opts name)
                `DSigP` (singFamily `DAppT` DVarT tyname)
-    go (ADConP name pats) = do
+    go (ADConP name tys pats) = do
       opts <- getOptions
-      DConP (singledDataConName opts name) [] <$> mapM go pats
+      DConP (singledDataConName opts name) tys <$> mapM go pats
     go (ADTildeP pat) = do
       qReportWarning
         "Lazy pattern converted into regular pattern during singleton generation."
diff --git a/singletons-th/src/Data/Singletons/TH/Syntax.hs b/singletons-th/src/Data/Singletons/TH/Syntax.hs
index 523341e..0297407 100644
--- a/singletons-th/src/Data/Singletons/TH/Syntax.hs
+++ b/singletons-th/src/Data/Singletons/TH/Syntax.hs
@@ -114,7 +114,7 @@ data ADExp = ADVarE Name
 -- A DPat with a pattern-signature node annotated with its type-level equivalent
 data ADPat = ADLitP Lit
            | ADVarP Name
-           | ADConP Name [ADPat]
+           | ADConP Name [DType] [ADPat]
            | ADTildeP ADPat
            | ADBangP ADPat
            | ADSigP DType -- The promoted pattern. Will not contain any wildcards,

This suffices to allow the blah function above to be promoted and singled. There's one remaining issue left to fix: wildcard patterns. If you have this program:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -ddump-splices #-}
module VTAPats where

import Data.Singletons.Base.TH
import Prelude.Singletons

$(singletons [d|
  argh :: Maybe () -> ()
  argh (Nothing @_) = ()
  argh (Just ())    = ()
  |])

Then it will fail like so:

[1 of 1] Compiling VTAPats          ( Bug.hs, interpreted )

Bug.hs:14:2: error: Q monad failure
   |
14 | $(singletons [d|
   |  ^^^^^^^^^^^^^^^...

Bug.hs:14:2: error:
    Illegal Haskell construct encountered:
headed by: DWildCardT
applied to: []
   |
14 | $(singletons [d|
   |  ^^^^^^^^^^^^^^^...

See #480.