{- Data/Singletons/Promote/Defun.hs

(c) Richard Eisenberg, Jan Stolarek 2014
rae@cs.brynmawr.edu

This file creates defunctionalization symbols for types during promotion.
-}

{-# LANGUAGE TemplateHaskell #-}

module Data.Singletons.Promote.Defun where

import Language.Haskell.TH.Desugar
import Data.Singletons.Promote.Monad
import Data.Singletons.Promote.Type
import Data.Singletons.Names
import Language.Haskell.TH.Syntax
import Data.Singletons.Syntax
import Data.Singletons.TH.Options
import Data.Singletons.Util
import Control.Monad
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import Data.Maybe

defunInfo :: DInfo -> PrM [DDec]
defunInfo :: DInfo -> PrM [DDec]
defunInfo (DTyConI DDec
dec Maybe [DDec]
_instances) = DDec -> PrM [DDec]
buildDefunSyms DDec
dec
defunInfo (DPrimTyConI Name
_name Int
_numArgs Bool
_unlifted) =
  String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DDec]) -> String -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ String
"Building defunctionalization symbols of primitive " String -> String -> String
forall a. [a] -> [a] -> [a]
++
         String
"type constructors not supported"
defunInfo (DVarI Name
_name DType
_ty Maybe Name
_mdec) =
  String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of values not supported"
defunInfo (DTyVarI Name
_name DType
_ty) =
  String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of type variables not supported"
defunInfo (DPatSynI {}) =
  String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of pattern synonyms not supported"

-- Defunctionalize type families defined at the top level (i.e., not associated
-- with a type class).
defunTopLevelTypeDecls ::
     [TySynDecl]
  -> [ClosedTypeFamilyDecl]
  -> [OpenTypeFamilyDecl]
  -> PrM ()
defunTopLevelTypeDecls :: [TySynDecl]
-> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
defunTopLevelTypeDecls [TySynDecl]
ty_syns [ClosedTypeFamilyDecl]
c_tyfams [OpenTypeFamilyDecl]
o_tyfams = do
  [DDec]
defun_ty_syns <-
    (TySynDecl -> PrM [DDec]) -> [TySynDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (\(TySynDecl Name
name [DTyVarBndr]
tvbs DType
rhs) -> Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndr]
tvbs DType
rhs) [TySynDecl]
ty_syns
  [DDec]
defun_c_tyfams <-
    (ClosedTypeFamilyDecl -> PrM [DDec])
-> [ClosedTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD (DTypeFamilyHead -> PrM [DDec])
-> (ClosedTypeFamilyDecl -> DTypeFamilyHead)
-> ClosedTypeFamilyDecl
-> PrM [DDec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ClosedTypeFamilyDecl -> DTypeFamilyHead
forall (info :: FamilyInfo). TypeFamilyDecl info -> DTypeFamilyHead
getTypeFamilyDecl) [ClosedTypeFamilyDecl]
c_tyfams
  [DDec]
defun_o_tyfams <-
    (OpenTypeFamilyDecl -> PrM [DDec])
-> [OpenTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD (DTypeFamilyHead -> PrM [DDec])
-> (OpenTypeFamilyDecl -> DTypeFamilyHead)
-> OpenTypeFamilyDecl
-> PrM [DDec]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpenTypeFamilyDecl -> DTypeFamilyHead
forall (info :: FamilyInfo). TypeFamilyDecl info -> DTypeFamilyHead
getTypeFamilyDecl) [OpenTypeFamilyDecl]
o_tyfams
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM ()
forall a b. (a -> b) -> a -> b
$ [DDec]
defun_ty_syns [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
defun_c_tyfams [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
defun_o_tyfams

-- Defunctionalize all the type families associated with a type class.
defunAssociatedTypeFamilies ::
     [DTyVarBndr]         -- The type variables bound by the parent class
  -> [OpenTypeFamilyDecl] -- The type families associated with the parent class
  -> PrM ()
defunAssociatedTypeFamilies :: [DTyVarBndr] -> [OpenTypeFamilyDecl] -> PrM ()
defunAssociatedTypeFamilies [DTyVarBndr]
cls_tvbs [OpenTypeFamilyDecl]
atfs = do
  [DDec]
defun_atfs <- (OpenTypeFamilyDecl -> PrM [DDec])
-> [OpenTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM OpenTypeFamilyDecl -> PrM [DDec]
defun [OpenTypeFamilyDecl]
atfs
  [DDec] -> PrM ()
forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
emitDecs [DDec]
defun_atfs
  where
    defun :: OpenTypeFamilyDecl -> PrM [DDec]
    defun :: OpenTypeFamilyDecl -> PrM [DDec]
defun (TypeFamilyDecl DTypeFamilyHead
tf_head) =
      (DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
ascribe_tf_tvb_kind Maybe DType -> Maybe DType
forall a. a -> a
id DTypeFamilyHead
tf_head

    -- Maps class-bound type variables to their kind annotations (if supplied).
    -- For example, `class C (a :: Bool) b (c :: Type)` will produce
    -- {a |-> Bool, c |-> Type}.
    cls_tvb_kind_map :: Map Name DKind
    cls_tvb_kind_map :: Map Name DType
cls_tvb_kind_map = [(Name, DType)] -> Map Name DType
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (DTyVarBndr -> Name
extractTvbName DTyVarBndr
tvb, DType
tvb_kind)
                                    | DTyVarBndr
tvb <- [DTyVarBndr]
cls_tvbs
                                    , Just DType
tvb_kind <- [DTyVarBndr -> Maybe DType
extractTvbKind DTyVarBndr
tvb]
                                    ]

    -- If the parent class lacks a SAK, we cannot safely default kinds to
    -- Type. All we can do is make use of whatever kind information that parent
    -- class provides and let kind inference do the rest.
    --
    -- We can sometimes learn more specific information about unannotated type
    -- family binders from the parent class, as in the following example:
    --
    --   class C (a :: Bool) where
    --     type T a :: Type
    --
    -- Here, we know that `T :: Bool -> Type` because we can infer that the `a`
    -- in `type T a` should be of kind `Bool` from the class SAK.
    ascribe_tf_tvb_kind :: DTyVarBndr -> DTyVarBndr
    ascribe_tf_tvb_kind :: DTyVarBndr -> DTyVarBndr
ascribe_tf_tvb_kind DTyVarBndr
tvb =
      case DTyVarBndr
tvb of
        DKindedTV{} -> DTyVarBndr
tvb
        DPlainTV Name
n  -> DTyVarBndr -> (DType -> DTyVarBndr) -> Maybe DType -> DTyVarBndr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DTyVarBndr
tvb (Name -> DType -> DTyVarBndr
DKindedTV Name
n) (Maybe DType -> DTyVarBndr) -> Maybe DType -> DTyVarBndr
forall a b. (a -> b) -> a -> b
$ Name -> Map Name DType -> Maybe DType
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name DType
cls_tvb_kind_map

buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms DDec
dec =
  case DDec
dec of
    DDataD NewOrData
_new_or_data DCxt
_cxt Name
_tyName [DTyVarBndr]
_tvbs Maybe DType
_k [DCon]
ctors [DDerivClause]
_derivings ->
      [DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors
    DClosedTypeFamilyD DTypeFamilyHead
tf_head [DTySynEqn]
_ ->
      DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD DTypeFamilyHead
tf_head
    DOpenTypeFamilyD DTypeFamilyHead
tf_head ->
      DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD DTypeFamilyHead
tf_head
    DTySynD Name
name [DTyVarBndr]
tvbs DType
rhs ->
      Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndr]
tvbs DType
rhs
    DClassD DCxt
_cxt Name
name [DTyVarBndr]
tvbs [FunDep]
_fundeps [DDec]
_members ->
      Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
tvbs (DType -> Maybe DType
forall a. a -> Maybe a
Just (Name -> DType
DConT Name
constraintName))
    DDec
_ -> String -> PrM [DDec]
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DDec]) -> String -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ String
"Defunctionalization symbols can only be built for " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                String
"type families and data declarations"

-- Unlike open type families, closed type families that lack SAKS do not
-- default anything to Type, instead relying on kind inference to figure out
-- unspecified kinds.
buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD = (DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
forall a. a -> a
id Maybe DType -> Maybe DType
forall a. a -> a
id

-- If an open type family lacks a SAK and has type variable binders or a result
-- without explicit kinds, then they default to Type (hence the uses of
-- default{Tvb,Maybe}ToTypeKind).
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD =
  (DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
defaultTvbToTypeKind (DType -> Maybe DType
forall a. a -> Maybe a
Just (DType -> Maybe DType)
-> (Maybe DType -> DType) -> Maybe DType -> Maybe DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DType -> DType
defaultMaybeToTypeKind)

buildDefunSymsTypeFamilyHead
  :: (DTyVarBndr -> DTyVarBndr)   -- How to default each type variable binder
  -> (Maybe DKind -> Maybe DKind) -- How to default the result kind
  -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead :: (DTyVarBndr -> DTyVarBndr)
-> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
default_tvb Maybe DType -> Maybe DType
default_kind
    (DTypeFamilyHead Name
name [DTyVarBndr]
tvbs DFamilyResultSig
result_sig Maybe InjectivityAnn
_) = do
  let arg_tvbs :: [DTyVarBndr]
arg_tvbs = (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> DTyVarBndr
default_tvb [DTyVarBndr]
tvbs
      res_kind :: Maybe DType
res_kind = Maybe DType -> Maybe DType
default_kind (DFamilyResultSig -> Maybe DType
resultSigToMaybeKind DFamilyResultSig
result_sig)
  Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
arg_tvbs Maybe DType
res_kind

buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndr]
tvbs DType
rhs = Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
tvbs Maybe DType
mb_res_kind
  where
    -- If a type synonym lacks a SAK, we can "infer" its result kind by
    -- checking for an explicit kind annotation on the right-hand side.
    mb_res_kind :: Maybe DKind
    mb_res_kind :: Maybe DType
mb_res_kind = case DType
rhs of
                    DSigT DType
_ DType
k -> DType -> Maybe DType
forall a. a -> Maybe a
Just DType
k
                    DType
_         -> Maybe DType
forall a. Maybe a
Nothing

buildDefunSymsDataD :: [DCon] -> PrM [DDec]
buildDefunSymsDataD :: [DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors =
  (DCon -> PrM [DDec]) -> [DCon] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM DCon -> PrM [DDec]
promoteCtor [DCon]
ctors
  where
    promoteCtor :: DCon -> PrM [DDec]
    promoteCtor :: DCon -> PrM [DDec]
promoteCtor (DCon [DTyVarBndr]
tvbs DCxt
_ Name
name DConFields
fields DType
res_ty) = do
      let arg_tys :: DCxt
arg_tys = DConFields -> DCxt
tysOfConFields DConFields
fields
      DCxt
arg_kis <- (DType -> PrM DType) -> DCxt -> PrM DCxt
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DCxt
arg_tys
      DType
res_ki  <- DType -> PrM DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
res_ty
      let con_ki :: DType
con_ki = [DTyVarBndr] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr]
tvbs [] DCxt
arg_kis DType
res_ki
      Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
      Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DType -> DefunKindInfo
DefunSAK DType
con_ki

-- Generate defunctionalization symbols for a name, using reifyFixityWithLocals
-- to determine what the fixity of each symbol should be
-- (see Note [Fixity declarations for defunctionalization symbols])
-- and dsReifyType to determine whether defunctionalization should make use
-- of SAKs or not (see Note [Defunctionalization game plan]).
defunReify :: Name           -- Name of the declaration to be defunctionalized
           -> [DTyVarBndr]   -- The declaration's type variable binders
                             -- (only used if the declaration lacks a SAK)
           -> Maybe DKind    -- The declaration's return kind, if it has one
                             -- (only used if the declaration lacks a SAK)
           -> PrM [DDec]
defunReify :: Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defunReify Name
name [DTyVarBndr]
tvbs Maybe DType
m_res_kind = do
  Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
  Maybe DType
m_sak    <- Name -> PrM (Maybe DType)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DType)
dsReifyType Name
name
  let defun :: DefunKindInfo -> PrM [DDec]
defun = Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity
  case Maybe DType
m_sak of
    Just DType
sak -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DType -> DefunKindInfo
DefunSAK DType
sak
    Maybe DType
Nothing  -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndr] -> Maybe DType -> DefunKindInfo
DefunNoSAK [DTyVarBndr]
tvbs Maybe DType
m_res_kind

-- Generate symbol data types, Apply instances, and other declarations required
-- for defunctionalization.
-- See Note [Defunctionalization game plan] for an overview of the design
-- considerations involved.
defunctionalize :: Name
                -> Maybe Fixity
                -> DefunKindInfo
                -> PrM [DDec]
defunctionalize :: Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity DefunKindInfo
defun_ki = do
  case DefunKindInfo
defun_ki of
    DefunSAK DType
sak ->
      -- Even if a declaration has a SAK, its kind may not be vanilla.
      case DType -> Either String ([DTyVarBndr], DCxt, DCxt, DType)
unravelVanillaDType_either DType
sak of
        -- If the kind isn't vanilla, use the fallback approach.
        -- See Note [Defunctionalization game plan],
        -- Wrinkle 2: Non-vanilla kinds.
        Left String
_ -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defun_fallback [] (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
sak)
        -- Otherwise, proceed with defun_vanilla_sak.
        Right ([DTyVarBndr]
sak_tvbs, DCxt
_sak_cxt, DCxt
sak_arg_kis, DType
sak_res_ki)
               -> [DTyVarBndr] -> DCxt -> DType -> PrM [DDec]
defun_vanilla_sak [DTyVarBndr]
sak_tvbs DCxt
sak_arg_kis DType
sak_res_ki
    -- If a declaration lacks a SAK, it likely has a partial kind.
    -- See Note [Defunctionalization game plan], Wrinkle 1: Partial kinds.
    DefunNoSAK [DTyVarBndr]
tvbs Maybe DType
m_res -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defun_fallback [DTyVarBndr]
tvbs Maybe DType
m_res
  where
    -- Generate defunctionalization symbols for things with vanilla SAKs.
    -- The symbols themselves will also be given SAKs.
    defun_vanilla_sak :: [DTyVarBndr] -> [DKind] -> DKind -> PrM [DDec]
    defun_vanilla_sak :: [DTyVarBndr] -> DCxt -> DType -> PrM [DDec]
defun_vanilla_sak [DTyVarBndr]
sak_tvbs DCxt
sak_arg_kis DType
sak_res_ki = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      Name
extra_name <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"arg"
      -- Use noExactName below to avoid #17537.
      [Name]
arg_names <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (DCxt -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
sak_arg_kis) (Name -> Name
noExactName (Name -> Name) -> PrM Name -> PrM Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"a")

      let -- The inner loop. @go n arg_nks res_nks@ returns @(res_k, decls)@.
          -- Using one particular example:
          --
          -- @
          -- type ExampleSym2 :: a -> b -> c ~> d ~> Type
          -- data ExampleSym2 x y where ...
          -- type instance Apply (ExampleSym2 x y) z = ExampleSym3 x y z
          -- ...
          -- @
          --
          -- We have:
          --
          -- * @n@ is 2. This is incremented in each iteration of `go`.
          --
          -- * @arg_nks@ is [(x, a), (y, b)]. Each element in this list is a
          -- (type variable name, type variable kind) pair. The kinds appear in
          -- the SAK, separated by matchable arrows (->).
          --
          -- * @res_tvbs@ is [(z, c), (w, d)]. Each element in this list is a
          -- (type variable name, type variable kind) pair. The kinds appear in
          -- @res_k@, separated by unmatchable arrows (~>).
          --
          -- * @res_k@ is `c ~> d ~> Type`. @res_k@ is returned so that earlier
          --   defunctionalization symbols can build on the result kinds of
          --   later symbols. For instance, ExampleSym1 would get the result
          --   kind `b ~> c ~> d ~> Type` by prepending `b` to ExampleSym2's
          --   result kind `c ~> d ~> Type`.
          --
          -- * @decls@ are all of the declarations corresponding to ExampleSym2
          --   and later defunctionalization symbols. This is the main payload of
          --   the function.
          --
          -- This function is quadratic because it appends a variable at the end of
          -- the @arg_nks@ list at each iteration. In practice, this is unlikely
          -- to be a performance bottleneck since the number of arguments rarely
          -- gets to be that large.
          go :: Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
          go :: Int -> [(Name, DType)] -> [(Name, DType)] -> (DType, [DDec])
go Int
n [(Name, DType)]
arg_nks [(Name, DType)]
res_nkss =
            case [(Name, DType)]
res_nkss of
              [] ->
                let -- Somewhat surprisingly, we do *not* generate SAKs for
                    -- fully saturated defunctionalization symbols.
                    -- See Note [No SAKs for fully saturated defunctionalization symbols]
                    sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndr] -> Maybe DType -> [DDec]
mk_sat_decs Options
opts Int
n (((Name, DType) -> DTyVarBndr) -> [(Name, DType)] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map ((Name -> DType -> DTyVarBndr) -> (Name, DType) -> DTyVarBndr
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> DType -> DTyVarBndr
DKindedTV) [(Name, DType)]
arg_nks)
                                           (DType -> Maybe DType
forall a. a -> Maybe a
Just DType
sak_res_ki)
                in (DType
sak_res_ki, [DDec]
sat_decs)
              (Name, DType)
res_nk:[(Name, DType)]
res_nks ->
                let (DType
res_ki, [DDec]
decs)   = Int -> [(Name, DType)] -> [(Name, DType)] -> (DType, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([(Name, DType)]
arg_nks [(Name, DType)] -> [(Name, DType)] -> [(Name, DType)]
forall a. [a] -> [a] -> [a]
++ [(Name, DType)
res_nk]) [(Name, DType)]
res_nks
                    tyfun :: DType
tyfun            = DType -> DType -> DType
buildTyFunArrow ((Name, DType) -> DType
forall a b. (a, b) -> b
snd (Name, DType)
res_nk) DType
res_ki
                    defun_sak_dec :: DDec
defun_sak_dec    = Name -> DType -> DDec
DKiSigD (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n) (DType -> DDec) -> DType -> DDec
forall a b. (a -> b) -> a -> b
$
                                       [DTyVarBndr] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [DTyVarBndr]
sak_tvbs [] (((Name, DType) -> DType) -> [(Name, DType)] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name, DType) -> DType
forall a b. (a, b) -> b
snd [(Name, DType)]
arg_nks) DType
tyfun
                    defun_other_decs :: [DDec]
defun_other_decs = Options
-> Int -> [DTyVarBndr] -> Name -> Name -> Maybe DType -> [DDec]
mk_defun_decs Options
opts Int
n (((Name, DType) -> DTyVarBndr) -> [(Name, DType)] -> [DTyVarBndr]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> DTyVarBndr
DPlainTV (Name -> DTyVarBndr)
-> ((Name, DType) -> Name) -> (Name, DType) -> DTyVarBndr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, DType) -> Name
forall a b. (a, b) -> a
fst) [(Name, DType)]
arg_nks)
                                                     ((Name, DType) -> Name
forall a b. (a, b) -> a
fst (Name, DType)
res_nk) Name
extra_name Maybe DType
forall a. Maybe a
Nothing
                in (DType
tyfun, DDec
defun_sak_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
defun_other_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)

      [DDec] -> PrM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (DType, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((DType, [DDec]) -> [DDec]) -> (DType, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int -> [(Name, DType)] -> [(Name, DType)] -> (DType, [DDec])
go Int
0 [] ([(Name, DType)] -> (DType, [DDec]))
-> [(Name, DType)] -> (DType, [DDec])
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [(Name, DType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
arg_names DCxt
sak_arg_kis

    -- If defun_sak can't be used to defunctionalize something, this fallback
    -- approach is used. This is used when defunctionalizing something with a
    -- partial kind
    -- (see Note [Defunctionalization game plan], Wrinkle 1: Partial kinds)
    -- or a non-vanilla kind
    -- (see Note [Defunctionalization game plan], Wrinkle 2: Non-vanilla kinds).
    defun_fallback :: [DTyVarBndr] -> Maybe DKind -> PrM [DDec]
    defun_fallback :: [DTyVarBndr] -> Maybe DType -> PrM [DDec]
defun_fallback [DTyVarBndr]
tvbs' Maybe DType
m_res' = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      Name
extra_name <- String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"arg"
      -- Use noExactTyVars below to avoid #11812.
      ([DTyVarBndr]
tvbs, Maybe DType
m_res) <- [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType)
eta_expand ([DTyVarBndr] -> [DTyVarBndr]
forall a. Data a => a -> a
noExactTyVars [DTyVarBndr]
tvbs') (Maybe DType -> Maybe DType
forall a. Data a => a -> a
noExactTyVars Maybe DType
m_res')

      let -- The inner loop. @go n arg_tvbs res_tvbs@ returns @(m_res_k, decls)@.
          -- Using one particular example:
          --
          -- @
          -- data ExampleSym2 (x :: a) y :: c ~> d ~> Type where ...
          -- type instance Apply (ExampleSym2 x y) z = ExampleSym3 x y z
          -- ...
          -- @
          --
          -- This works very similarly to the `go` function in
          -- `defun_vanilla_sak`. The main differences are:
          --
          -- * This function does not produce any SAKs for defunctionalization
          --   symbols.
          --
          -- * Instead of [(Name, DKind)], this function uses [DTyVarBndr] as
          --   the types of @arg_tvbs@ and @res_tvbs@. This is because the
          --   kinds are not always known. By a similar token, this function
          --   uses Maybe DKind, not DKind, as the type of @m_res_k@, since
          --   the result kind is not always fully known.
          go :: Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DKind, [DDec])
          go :: Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DType, [DDec])
go Int
n [DTyVarBndr]
arg_tvbs [DTyVarBndr]
res_tvbss =
            case [DTyVarBndr]
res_tvbss of
              [] ->
                let sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndr] -> Maybe DType -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndr]
arg_tvbs Maybe DType
m_res
                in (Maybe DType
m_res, [DDec]
sat_decs)
              DTyVarBndr
res_tvb:[DTyVarBndr]
res_tvbs ->
                let (Maybe DType
m_res_ki, [DDec]
decs) = Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DType, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr
res_tvb]) [DTyVarBndr]
res_tvbs
                    m_tyfun :: Maybe DType
m_tyfun          = Maybe DType -> Maybe DType -> Maybe DType
buildTyFunArrow_maybe (DTyVarBndr -> Maybe DType
extractTvbKind DTyVarBndr
res_tvb)
                                                             Maybe DType
m_res_ki
                    defun_decs' :: [DDec]
defun_decs'      = Options
-> Int -> [DTyVarBndr] -> Name -> Name -> Maybe DType -> [DDec]
mk_defun_decs Options
opts Int
n [DTyVarBndr]
arg_tvbs
                                                     (DTyVarBndr -> Name
extractTvbName DTyVarBndr
res_tvb)
                                                     Name
extra_name Maybe DType
m_tyfun
                in (Maybe DType
m_tyfun, [DDec]
defun_decs' [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)

      [DDec] -> PrM [DDec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (Maybe DType, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((Maybe DType, [DDec]) -> [DDec])
-> (Maybe DType, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int -> [DTyVarBndr] -> [DTyVarBndr] -> (Maybe DType, [DDec])
go Int
0 [] [DTyVarBndr]
tvbs

    mk_defun_decs :: Options
                  -> Int
                  -> [DTyVarBndr]
                  -> Name
                  -> Name
                  -> Maybe DKind
                  -> [DDec]
    mk_defun_decs :: Options
-> Int -> [DTyVarBndr] -> Name -> Name -> Maybe DType -> [DDec]
mk_defun_decs Options
opts Int
n [DTyVarBndr]
arg_tvbs Name
tyfun_name Name
extra_name Maybe DType
m_tyfun =
      let data_name :: Name
data_name   = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n
          next_name :: Name
next_name   = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
          con_name :: Name
con_name    = String -> String -> Name -> Name
prefixName String
"" String
":" (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ String -> String -> Name -> Name
suffixName String
"KindInference" String
"###" Name
data_name
          arg_names :: [Name]
arg_names   = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr -> Name
extractTvbName [DTyVarBndr]
arg_tvbs
          params :: [DTyVarBndr]
params      = [DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [Name -> DTyVarBndr
DPlainTV Name
tyfun_name]
          con_eq_ct :: DType
con_eq_ct   = Name -> DType
DConT Name
sameKindName DType -> DType -> DType
`DAppT` DType
lhs DType -> DType -> DType
`DAppT` DType
rhs
            where
              lhs :: DType
lhs = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
data_name) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
arg_names) DType -> DType -> DType
`apply` (Name -> DType
DVarT Name
extra_name)
              rhs :: DType
rhs = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
next_name) ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT ([Name]
arg_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
extra_name]))
          con_decl :: DCon
con_decl    = [DTyVarBndr] -> DCxt -> Name -> DConFields -> DType -> DCon
DCon [] [DType
con_eq_ct] Name
con_name (Bool -> [DBangType] -> DConFields
DNormalC Bool
False [])
                             (DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
data_name) [DTyVarBndr]
params)
          data_decl :: DDec
data_decl   = NewOrData
-> DCxt
-> Name
-> [DTyVarBndr]
-> Maybe DType
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD NewOrData
Data [] Name
data_name [DTyVarBndr]
args Maybe DType
m_tyfun [DCon
con_decl] []
            where
              args :: [DTyVarBndr]
args | Maybe DType -> Bool
forall a. Maybe a -> Bool
isJust Maybe DType
m_tyfun = [DTyVarBndr]
arg_tvbs
                   | Bool
otherwise      = [DTyVarBndr]
params
          app_data_ty :: DType
app_data_ty = DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
data_name) [DTyVarBndr]
arg_tvbs
          app_eqn :: DTySynEqn
app_eqn     = Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr]
forall a. Maybe a
Nothing
                                  (Name -> DType
DConT Name
applyName DType -> DType -> DType
`DAppT` DType
app_data_ty
                                                   DType -> DType -> DType
`DAppT` Name -> DType
DVarT Name
tyfun_name)
                                  (DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
next_name)
                                                ([DTyVarBndr]
arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [Name -> DTyVarBndr
DPlainTV Name
tyfun_name]))
          app_decl :: DDec
app_decl    = DTySynEqn -> DDec
DTySynInstD DTySynEqn
app_eqn
          suppress :: DDec
suppress    = Maybe Overlap
-> Maybe [DTyVarBndr] -> DCxt -> DType -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr]
forall a. Maybe a
Nothing []
                          (Name -> DType
DConT Name
suppressClassName DType -> DType -> DType
`DAppT` DType
app_data_ty)
                          [DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
suppressMethodName
                                           [[DPat] -> DExp -> DClause
DClause []
                                                    ((Name -> DExp
DVarE 'snd) DExp -> DExp -> DExp
`DAppE`
                                                     [DExp] -> DExp
mkTupleDExp [Name -> DExp
DConE Name
con_name,
                                                                  [DExp] -> DExp
mkTupleDExp []])]]

          -- See Note [Fixity declarations for defunctionalization symbols]
          fixity_decl :: [DDec]
fixity_decl = Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec]
forall a b. (a -> b) -> a -> b
$ (Fixity -> DDec) -> Maybe Fixity -> Maybe DDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Fixity -> DDec
mk_fix_decl Name
data_name) Maybe Fixity
m_fixity
      in DDec
data_decl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: DDec
app_decl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: DDec
suppress DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: [DDec]
fixity_decl

    -- Generate a "fully saturated" defunction symbol, along with a fixity
    -- declaration (if needed).
    mk_sat_decs :: Options -> Int -> [DTyVarBndr] -> Maybe DKind -> [DDec]
    mk_sat_decs :: Options -> Int -> [DTyVarBndr] -> Maybe DType -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndr]
sat_tvbs Maybe DType
m_sat_res =
      let sat_name :: Name
sat_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n
          sat_dec :: DDec
sat_dec  = Name -> [DTyVarBndr] -> DType -> DDec
DTySynD Name
sat_name [DTyVarBndr]
sat_tvbs (DType -> DDec) -> DType -> DDec
forall a b. (a -> b) -> a -> b
$
                     DType -> [DTyVarBndr] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndr]
sat_tvbs DType -> Maybe DType -> DType
`maybeSigT` Maybe DType
m_sat_res
          sat_fixity_dec :: [DDec]
sat_fixity_dec = Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec]
forall a b. (a -> b) -> a -> b
$ (Fixity -> DDec) -> Maybe Fixity -> Maybe DDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> Fixity -> DDec
mk_fix_decl Name
sat_name) Maybe Fixity
m_fixity
      in DDec
sat_dec DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: [DDec]
sat_fixity_dec

    -- Generate extra kind variable binders corresponding to the number of
    -- arrows in the return kind (if provided). Examples:
    --
    -- >>> eta_expand [(x :: a), (y :: b)] (Just (c -> Type))
    -- ([(x :: a), (y :: b), (e :: c)], Just Type)
    --
    -- >>> eta_expand [(x :: a), (y :: b)] Nothing
    -- ([(x :: a), (y :: b)], Nothing)
    eta_expand :: [DTyVarBndr] -> Maybe DKind -> PrM ([DTyVarBndr], Maybe DKind)
    eta_expand :: [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType)
eta_expand [DTyVarBndr]
m_arg_tvbs Maybe DType
Nothing = ([DTyVarBndr], Maybe DType) -> PrM ([DTyVarBndr], Maybe DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
m_arg_tvbs, Maybe DType
forall a. Maybe a
Nothing)
    eta_expand [DTyVarBndr]
m_arg_tvbs (Just DType
res_kind) = do
        let (DFunArgs
arg_ks, DType
result_k) = DType -> (DFunArgs, DType)
unravelDType DType
res_kind
            vis_arg_ks :: [DVisFunArg]
vis_arg_ks = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
arg_ks
        [DTyVarBndr]
extra_arg_tvbs <- (DVisFunArg -> PrM DTyVarBndr) -> [DVisFunArg] -> PrM [DTyVarBndr]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DVisFunArg -> PrM DTyVarBndr
mk_extra_tvb [DVisFunArg]
vis_arg_ks
        ([DTyVarBndr], Maybe DType) -> PrM ([DTyVarBndr], Maybe DType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndr]
m_arg_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndr]
extra_arg_tvbs, DType -> Maybe DType
forall a. a -> Maybe a
Just DType
result_k)

    -- Convert a DVisFunArg to a DTyVarBndr, generating a fresh type variable
    -- name if the DVisFunArg is an anonymous argument.
    mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndr
    mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndr
mk_extra_tvb DVisFunArg
vfa =
      case DVisFunArg
vfa of
        DVisFADep DTyVarBndr
tvb -> DTyVarBndr -> PrM DTyVarBndr
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTyVarBndr
tvb
        DVisFAAnon DType
k  -> Name -> DType -> DTyVarBndr
DKindedTV (Name -> DType -> DTyVarBndr)
-> PrM Name -> PrM (DType -> DTyVarBndr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"e" PrM (DType -> DTyVarBndr) -> PrM DType -> PrM DTyVarBndr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> DType -> PrM DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
k

    mk_fix_decl :: Name -> Fixity -> DDec
    mk_fix_decl :: Name -> Fixity -> DDec
mk_fix_decl Name
n Fixity
f = DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Fixity -> Name -> DLetDec
DInfixD Fixity
f Name
n

-- Indicates whether the type being defunctionalized has a standalone kind
-- signature. If it does, DefunSAK contains the kind. If not, DefunNoSAK
-- contains whatever information is known about its type variable binders
-- and result kind.
-- See Note [Defunctionalization game plan] for details on how this
-- information is used.
data DefunKindInfo
  = DefunSAK DKind
  | DefunNoSAK [DTyVarBndr] (Maybe DKind)

-- Shorthand for building (k1 ~> k2)
buildTyFunArrow :: DKind -> DKind -> DKind
buildTyFunArrow :: DType -> DType -> DType
buildTyFunArrow DType
k1 DType
k2 = Name -> DType
DConT Name
tyFunArrowName DType -> DType -> DType
`DAppT` DType
k1 DType -> DType -> DType
`DAppT` DType
k2

buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe :: Maybe DType -> Maybe DType -> Maybe DType
buildTyFunArrow_maybe Maybe DType
m_k1 Maybe DType
m_k2 = DType -> DType -> DType
buildTyFunArrow (DType -> DType -> DType) -> Maybe DType -> Maybe (DType -> DType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DType
m_k1 Maybe (DType -> DType) -> Maybe DType -> Maybe DType
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DType
m_k2

{-
Note [Defunctionalization game plan]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generating defunctionalization symbols involves a surprising amount of
complexity. This Note gives a broad overview of what happens during
defunctionalization and highlights various design considerations.
As a working example, we will use the following type family:

  type Foo :: forall c a b. a -> b -> c -> c
  type family Foo x y z where ...

We must generate a defunctionalization symbol for every number of arguments
to which Foo can be partially applied. We do so by generating the following
declarations:

  type FooSym0 :: forall c a b. a ~> b ~> c ~> c
  data FooSym0 f where
   FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg)
                        => FooSym0 f
  type instance Apply FooSym0 x = FooSym1 x

  type FooSym1 :: forall c a b. a -> b ~> c ~> c
  data FooSym1 x f where
    FooSym1KindInference :: SameKind (Apply (FooSym1 a) arg) (FooSym2 a arg)
                         => FooSym1 a f
  type instance Apply (FooSym1 x) y = FooSym2 x y

  type FooSym2 :: forall c a b. a -> b -> c ~> c
  data FooSym2 x y f where
    FooSym2KindInference :: SameKind (Apply (FooSym2 x y) arg) (FooSym3 x y arg)
                         => FooSym2 x y f
  type instance Apply (FooSym2 x y) z = FooSym3 x y z

  type FooSym3 (x :: a) (y :: b) (z :: c) = Foo x y z :: c

Some things to note:

* Each defunctionalization symbol has its own standalone kind signature. The
  number after `Sym` in each symbol indicates the number of leading -> arrows
  in its kind—that is, the number of arguments to which it can be applied
  directly to without the use of the Apply type family.

  See "Wrinkle 1: Partial kinds" below for what happens if the declaration
  being defunctionalized does *not* have a standalone kind signature.

* Each data declaration has a constructor with the suffix `-KindInference`
  in its name. These are redundant in the particular case of Foo, where the
  kind is already known. They play a more vital role when the kind of the
  declaration being defunctionalized is only partially known.
  See "Wrinkle 1: Partial kinds" below for more information.

* FooSym3, the last defunctionalization symbol, is somewhat special in that
  it is a type synonym, not a data type. These sorts of symbols are referred
  to as "fully saturated" defunctionalization symbols. Furthermore, these
  symbols are intentionally *not* given SAKs. See
  Note [No SAKs for fully saturated defunctionalization symbols].

* If Foo had a fixity declaration (e.g., infixl 4 `Foo`), then we would also
  generate fixity declarations for each defunctionalization symbol (e.g.,
  infixl 4 `FooSym0`).
  See Note [Fixity declarations for defunctionalization symbols].

* Foo has a vanilla kind signature. (See
  Note [Vanilla-type validity checking during promotion] in D.S.Promote.Type
  for what "vanilla" means in this context.) Having a vanilla type signature is
  important, as it is a property that makes it much simpler to preserve the
  order of type variables (`forall c a b.`) in each of the defunctionalization
  symbols.

  That being said, it is not strictly required that the kind be vanilla. There
  is another approach that can be used to defunctionalize things with
  non-vanilla types, at the possible expense of having different type variable
  orders between different defunctionalization symbols.
  See "Wrinkle 2: Non-vanilla kinds" below for more information.

-----
-- Wrinkle 1: Partial kinds
-----

The Foo example above has a standalone kind signature, but not everything has
this much kind information. For example, consider this:

  $(singletons [d|
    type family Not x where
      Not False = True
      Not True  = False
    |])

The inferred kind for Not is `Bool -> Bool`, but since Not was declared in TH
quotes, `singletons` has no knowledge of this. Instead, we must rely on kind
inference to give Not's defunctionalization symbols the appropriate kinds.
Here is a naïve first attempt:

  data NotSym0 f
  type instance Apply NotSym0 x = NotSym1 x

  type NotSym1 x = Not x

NotSym1 will have the inferred kind `Bool -> Bool`, but poor NotSym0 will have
the inferred kind `forall k. k -> Type`, which is far more general than we
would like. We can do slightly better by supplying additional kind information
in a data constructor, like so:

  type SameKind :: k -> k -> Constraint
  class SameKind x y = ()

  data NotSym0 f where
    NotSym0KindInference :: SameKind (Apply NotSym0 arg) (NotSym1 arg)
                         => NotSym0 f

NotSym0KindInference is not intended to ever be seen by the user. Its only
reason for existing is its existential
`SameKind (Apply NotSym0 arg) (NotSym1 arg)` context, which allows GHC to
figure out that NotSym0 has kind `Bool ~> Bool`. This is a bit of a hack, but
it works quite nicely. The only problem is that GHC is likely to warn that
NotSym0KindInference is unused, which is annoying. To work around this, we
mention the data constructor in an instance of a dummy class:

  instance SuppressUnusedWarnings NotSym0 where
    suppressUnusedWarnings = snd (NotSym0KindInference, ())

Similarly, this SuppressUnusedWarnings class is not intended to ever be seen
by the user. As its name suggests, it only exists to help suppress "unused
data constructor" warnings.

Some declarations have a mixture of known kinds and unknown kinds, such as in
this example:

  $(singletons [d|
    type family Bar x (y :: Nat) (z :: Nat) :: Nat where ...
    |])

We can use the known kinds to guide kind inference. In this particular example
of Bar, here are the defunctionalization symbols that would be generated:

  data BarSym0 f where ...
  data BarSym1 x :: Nat ~> Nat ~> Nat where ...
  data BarSym2 x (y :: Nat) :: Nat ~> Nat where ...
  type BarSym3 x (y :: Nat) (z :: Nat) = Bar x y z :: Nat

-----
-- Wrinkle 2: Non-vanilla kinds
-----

There is only limited support for defunctionalizing declarations with
non-vanilla kinds. One example of something with a non-vanilla kind is the
following, which uses a nested forall:

  $(singletons [d|
    type Baz :: forall a. a -> forall b. b -> Type
    data Baz x y
    |])

One might envision generating the following defunctionalization symbols for
Baz:

  type BazSym0 :: forall a. a ~> forall b. b ~> Type
  data BazSym0 f where ...

  type BarSym1 :: forall a. a -> forall b. b ~> Type
  data BazSym1 x f where ...

  type family BazSym2 (x :: a) (y :: b) = Baz x y :: Type

Unfortunately, doing so would require impredicativity, since we would have:

    forall a. a ~> forall b. b ~> Type
  = forall a. (~>) a (forall b. b ~> Type)
  = forall a. TyFun a (forall b. b ~> Type) -> Type

Note that TyFun is an ordinary data type, so having its second argument be
(forall b. b ~> Type) is truly impredicative. As a result, trying to preserve
nested or higher-rank foralls is a non-starter.

We need not reject Baz entirely, however. We can still generate perfectly
usable defunctionalization symbols if we are willing to sacrifice the exact
order of foralls. When we encounter a non-vanilla kind such as Baz's, we simply
fall back to the algorithm used when we encounter a partial kind (as described
in "Wrinkle 1: Partial kinds" above.) In other words, we generate the
following symbols:

  data BazSym0 :: a ~> b ~> Type where ...
  data BazSym1 (x :: a) :: b ~> Type where ...
  type BazSym2 (x :: a) (y :: b) = Baz x y :: Type

The kinds of BazSym0 and BazSym1 both start with `forall a b.`,
whereas the `b` is quantified later in Baz itself. For most use cases, however,
this is not a huge concern.

Another way kinds can be non-vanilla is if they contain visible dependent
quantification, like so:

  $(singletons [d|
    type Quux :: forall (k :: Type) -> k -> Type
    data Quux x y
    |])

What should the kind of QuuxSym0 be? Intuitively, it should be this:

  type QuuxSym0 :: forall (k :: Type) ~> k ~> Type

Alas, `forall (k :: Type) ~>` simply doesn't work. See #304. But there is an
acceptable compromise we can make that can give us defunctionalization symbols
for Quux. Once again, we fall back to the partial kind algorithm:

  data QuuxSym0 :: Type ~> k ~> Type where ...
  data QuuxSym1 (k :: Type) :: k ~> Type where ...
  type QuuxSym2 (k :: Type) (x :: k) = Quux k x :: Type

The catch is that the kind of QuuxSym0, `forall k. Type ~> k ~> Type`, is
slightly more general than it ought to be. In practice, however, this is
unlikely to be a problem as long as you apply QuuxSym0 to arguments of the
right kinds.

Note [No SAKs for fully saturated defunctionalization symbols]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When generating defunctionalization symbols, most of the symbols are data
types. The last one, however, is a type synonym. For example, this code:

  $(singletons [d|
    type Const :: a -> b -> a
    type Const x y = x
    |])

Will generate the following symbols:

  type ConstSym0 :: a ~> b ~> a
  data ConstSym0 f where ...

  type ConstSym1 :: a -> b ~> a
  data ConstSym1 x f where ...

  type ConstSym2 (x :: a) (y :: b) = Const x y :: a

ConstSym2, the sole type synonym of the bunch, is what is referred to as a
"fully saturated" defunctionaliztion symbol.

At first glance, ConstSym2 may not seem terribly useful, since it is
effectively a thin wrapper around the original Const type. Indeed, fully
saturated symbols are never appear directly in user-written code. Instead,
they are most valuable in TH-generated code, as singletons often generates code
that directly applies a defunctionalization symbol to some number of arguments
(see, for instance, D.S.Names.promoteTySym). In theory, such code could carve
out a special case for fully saturated applications and apply the original
type instead of a defunctionalization symbol, but determining when an
application is fully saturated is often difficult in practice. As a result, it
is more convenient to just generate code that always applies FuncSymN to N
arguments, and to let fully saturated defunctionalization symbols handle the
case where N equals the number of arguments needed to fully saturate Func.

Another curious thing about fully saturated defunctionalization symbols do
*not* get assigned SAKs, unlike their data type brethren. Why not just give
ConstSym2 a SAK like this?

  type ConstSym2 :: a -> b -> a
  type ConstSym2 x y = Const x y

This would in fact work for most use cases, but there are a handful of corner
cases where this approach would break down. Here is one such corner case:

  $(promote [d|
    class Applicative f where
      pure :: a -> f a
      ...
      (*>) :: f a -> f b -> f b
    |])

  ==>

  class PApplicative f where
    type Pure (x :: a) :: f a
    type (*>) (x :: f a) (y :: f b) :: f b

What would happen if we were to defunctionalize the promoted version of (*>)?
We'd end up with the following defunctionalization symbols:

  type (*>@#@$)   :: f a ~> f b ~> f b
  data (*>@#@$) f where ...

  type (*>@#@$$)  :: f a -> f b ~> f b
  data (*>@#@$$) x f where ...

  type (*>@#@$$$) :: f a -> f b -> f b
  type (*>@#@$$$) x y = (*>) x y

It turns out, however, that (*>@#@$$$) will not kind-check. Because (*>@#@$$$)
has a standalone kind signature, it is kind-generalized *before* kind-checking
the actual definition itself. Therefore, the full kind is:

  type (*>@#@$$$) :: forall {k} (f :: k -> Type) (a :: k) (b :: k).
                     f a -> f b -> f b
  type (*>@#@$$$) x y = (*>) x y

However, the kind of (*>) is
`forall (f :: Type -> Type) (a :: Type) (b :: Type). f a -> f b -> f b`.
This is not general enough for (*>@#@$$$), which expects kind-polymorphic `f`,
`a`, and `b`, leading to a kind error. You might think that we could somehow
infer this information, but note the quoted definition of Applicative (and
PApplicative, as a consequence) omits the kinds of `f`, `a`, and `b` entirely.
Unless we were to implement full-blown kind inference inside of Template
Haskell (which is a tall order), the kind `f a -> f b -> f b` is about as good
as we can get.

Note that (*>@#@$) and (*>@#@$$) are implemented as GADTs, not type synonyms.
This allows them to have kind-polymorphic `f`, `a`, and `b` in their kinds
while equating `k` to be `Type` in their data constructors, which neatly avoids
the issue that (*>@#@$$$) faces.

-----

In one last attempt to salvage the idea of giving SAKs to fully saturated
defunctionalization symbols, I explored an idea where we would add
"dummy constraints" to get the kinds exactly right. The idea was to first
define a type synonym for dummy contexts:

  type Dummy :: Constraint -> Constraint
  type Dummy x = () ~ ()

Dummy simply ignores its argument and returns `() ~ ()`. `() ~ ()` was chosen
because it's one of the few Constraints that can currently be used at the kind
level. Dummy could, in theory, be used like this:

  type (*>@#@$)   :: Dummy (PApplicative f) => f a ~> f b ~> f b
  type (*>@#@$$)  :: Dummy (PApplicative f) => f a -> f b ~> f b
  type (*>@#@$$$) :: Dummy (PApplicative f) => f a -> f b -> f b

The advantage to using `Dummy (PApplicative f)` is that it would constraint `f`
to be of kind `Type -> Type`, which would get the kinds exactly the way we want
them. Sounds great, right? Unfortunately, it doesn't work in practice. Consider
this example:

  $(promoteOnly [d|
    class C a where
      m1 :: a -> a
      m1 = m2

      m2 :: a -> a
      m2 = m1
    |])

  ==>

  class PC a where
    type M1 (x :: a) :: a
    type M1 x = Apply M2Sym1 x

    type M2 (x :: a) :: a
    type M2 x = Apply M1Sym1 x

The generated code would fail to compile, instead throwing this error:

  error:
      • Class ‘PC’ cannot be used here
          (it is defined and used in the same recursive group)
      • In the first argument of ‘Dummy’, namely ‘(PC a)’
        In a standalone kind signature for ‘M2Sym1’:
          forall a. Dummy (PC a) => a -> a
     |
     | type M2Sym1 :: forall a. Dummy (PC a) => a -> a
     |                                 ^^^^

Ugh. I suspect this is a GHC bug (see
https://gitlab.haskell.org/ghc/ghc/issues/15942#note_242075), but it's one
that's unlikely to be fixed any time soon.

A slight variations on idea is to use the original class instead of the
promoted class in `Dummy` contexts, e.g.,

  type M2Sym1 :: forall a. Dummy (C a) => a -> a

This would avoid the recursive group issues, but it would introduce a new
problem: the original class is not guaranteed to exist if
`promoteOnly` or `singletonsOnly` are used to create the promoted class.
(Indeed, this is precisely the case in the `PC` example.)

-----

As an alternative to type synonyms, we might consider using type families to
define fully saturated defunctionalization symbols. For instance, we could try
this:

  type (*>@#@$$$) :: f a -> f b -> f b
  type family (*>@#@$$$) x y where
    (*>@#@$$$) x y = (*>) x y

Like before, the full kind of (*>@#@$$$) is generalized to be
`forall {k} (f :: k -> Type) (a :: k) (b :: k)`. The difference is that the
type family equation *matches* on `k` such that the equation will only trigger
if `k` is equal to `Type`. (This is similar to the trick that (*>@#@$) and
(*>@#@$$) employ, as being GADTs allows them to constrain `k` to be `Type` in
their data constructors.)

Alas, the type family approach is strictly less powerful than the type synonym
approach. Consider the following code:

  $(singletons [d|
    data Nat = Z | S Nat

    natMinus :: Nat -> Nat -> Nat
    natMinus Z     _     = Z
    natMinus (S a) (S b) = natMinus a b
    natMinus a     Z     = a
    |])

Among other things, this will generate the following declarations:

  type ZSym0 :: Nat

  type NatMinus :: Nat -> Nat -> Nat
  type family NatMinus x y where
    NatMinus Z     _     = ZSym0
    NatMinus (S a) (S b) = NatMinus a b
    NatMinus a     Z     = a

  sNatMinus :: SNat x -> SNat y -> SNat (NatMinus x y)
  sNatMinus SZ      _       = SZ
  sNatMinus (SS sA) (SS sB) = sNatMinus sA sB
  sNatMinus sA      SZ      = sA

Shockingly, this will either succeed or fail to compile depending on whether
ZSym0 is a type synonym or a type family. If ZSym0 is a type synonym, then
the first and third equations of NatMinus will be compatible (since GHC will
be able to infer that Z ~ ZSym0), which is what allows the third equation of
sNatMinus to typecheck. If ZSym0 is a type family, however, then the third
equation of NatMinus will be incompatible with the first, which will cause
the third equation of sNatMinus to fail to typecheck:

  error:
      • Could not deduce: NatMinus x 'Z ~ x
        from the context: y ~ 'Z
          bound by a pattern with constructor: SZ :: SNat 'Z,
                   in an equation for ‘sNatMinus’
        ‘x’ is a rigid type variable bound by
          the type signature for:
            sNatMinus :: forall (x :: Nat) (y :: Nat).
                         SNat x -> SNat y -> SNat (NatMinus x y)
        Expected type: SNat (NatMinus x y)
          Actual type: SNat x
      • In the expression: sA
        In an equation for ‘sNatMinus’: sNatMinus sA SZ = sA
      • Relevant bindings include
          sA :: SNat x
          sNatMinus :: SNat x -> SNat y -> SNat (NatMinus x y)

One could work around the issue by tweaking the third equation of natMinus
slightly:

  $(singletons [d|
    ...

    natMinus :: Nat -> Nat -> Nat
    natMinus Z       _     = Z
    natMinus (S a)   (S b) = natMinus a b
    natMinus a@(S _) Z     = a
    |])

But I would generally prefer to avoid having the user add extraneous pattern
matches when possible. Given the choice between expressiveness and SAKs, I give
the edge to expressiveness.

Bottom line: don't give fully saturated defunctionalization symbols SAKs. This
is admittedly not ideal, but it's unlikely to be a sticking point in practice,
given that these symbols are almost exclusively used in autogenerated code
in the first place. If we want to support promoting code that uses visible
type application (see #378), we will need to figure out how to resolve this
issue.

Note [Fixity declarations for defunctionalization symbols]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Just like we promote fixity declarations, we should also generate fixity
declarations for defunctionaliztion symbols. A primary use case is the
following scenario:

  (.) :: (b -> c) -> (a -> b) -> (a -> c)
  (f . g) x = f (g x)
  infixr 9 .

One often writes (f . g . h) at the value level, but because (.) is promoted
to a type family with three arguments, this doesn't directly translate to the
type level. Instead, one must write this:

  f .@#@$$$ g .@#@$$$ h

But in order to ensure that this associates to the right as expected, one must
generate an `infixr 9 .@#@#$$$` declaration. This is why defunctionalize accepts
a Maybe Fixity argument.
-}