{-# LANGUAGE TemplateHaskellQuotes #-}

{- Data/Singletons/TH/Promote/Defun.hs

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

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

module Data.Singletons.TH.Promote.Defun where

import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Monad
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.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 a. String -> PrM a
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 DKind
_ty Maybe Name
_mdec) =
  String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of values not supported"
defunInfo (DTyVarI Name
_name DKind
_ty) =
  String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of type variables not supported"
defunInfo (DPatSynI {}) =
  String -> PrM [DDec]
forall a. String -> PrM a
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 [DTyVarBndrUnit]
tvbs DKind
rhs) -> Name -> [DTyVarBndrUnit] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
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 ::
     [DTyVarBndrUnit]     -- The type variables bound by the parent class
  -> [OpenTypeFamilyDecl] -- The type families associated with the parent class
  -> PrM ()
defunAssociatedTypeFamilies :: [DTyVarBndrUnit] -> [OpenTypeFamilyDecl] -> PrM ()
defunAssociatedTypeFamilies [DTyVarBndrUnit]
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) =
      (DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
ascribe_tf_tvb_kind Maybe DKind -> Maybe DKind
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 DKind
cls_tvb_kind_map = [(Name, DKind)] -> Map Name DKind
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrUnit
tvb, DKind
tvb_kind)
                                    | DTyVarBndrUnit
tvb <- [DTyVarBndrUnit]
cls_tvbs
                                    , Just DKind
tvb_kind <- [DTyVarBndrUnit -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrUnit
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 :: DTyVarBndrUnit -> DTyVarBndrUnit
    ascribe_tf_tvb_kind :: DTyVarBndrUnit -> DTyVarBndrUnit
ascribe_tf_tvb_kind DTyVarBndrUnit
tvb =
      case DTyVarBndrUnit
tvb of
        DKindedTV{}  -> DTyVarBndrUnit
tvb
        DPlainTV Name
n ()
_ -> DTyVarBndrUnit
-> (DKind -> DTyVarBndrUnit) -> Maybe DKind -> DTyVarBndrUnit
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DTyVarBndrUnit
tvb (Name -> () -> DKind -> DTyVarBndrUnit
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
n ()) (Maybe DKind -> DTyVarBndrUnit) -> Maybe DKind -> DTyVarBndrUnit
forall a b. (a -> b) -> a -> b
$ Name -> Map Name DKind -> Maybe DKind
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name DKind
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 [DTyVarBndrUnit]
_tvbs Maybe DKind
_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 [DTyVarBndrUnit]
tvbs DKind
rhs ->
      Name -> [DTyVarBndrUnit] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
rhs
    DClassD DCxt
_cxt Name
name [DTyVarBndrUnit]
tvbs [FunDep]
_fundeps [DDec]
_members ->
      Name -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
tvbs (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (Name -> DKind
DConT Name
constraintName))
    DDec
_ -> String -> PrM [DDec]
forall a. String -> PrM a
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 = (DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
forall a. a -> a
id Maybe DKind -> Maybe DKind
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 =
  (DTyVarBndrUnit -> DTyVarBndrUnit)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrUnit -> DTyVarBndrUnit
forall flag. DTyVarBndr flag -> DTyVarBndr flag
defaultTvbToTypeKind (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (DKind -> Maybe DKind)
-> (Maybe DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DKind -> DKind
defaultMaybeToTypeKind)

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

buildDefunSymsTySynD :: Name -> [DTyVarBndrUnit] -> DType -> PrM [DDec]
buildDefunSymsTySynD :: Name -> [DTyVarBndrUnit] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrUnit]
tvbs DKind
rhs = Name -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
tvbs Maybe DKind
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 DKind
mb_res_kind = case DKind
rhs of
                    DSigT DKind
_ DKind
k -> DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
k
                    DKind
_         -> Maybe DKind
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 [DTyVarBndrSpec]
tvbs DCxt
_ Name
name DConFields
fields DKind
res_ty) = do
      Options
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      let name' :: Name
name'   = Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
          arg_tys :: DCxt
arg_tys = DConFields -> DCxt
tysOfConFields DConFields
fields
      DCxt
arg_kis <- (DKind -> PrM DKind) -> DCxt -> PrM DCxt
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DKind -> PrM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DCxt
arg_tys
      DKind
res_ki  <- DKind -> PrM DKind
forall (m :: * -> *). OptionsMonad m => DKind -> m DKind
promoteType_NC DKind
res_ty
      let con_ki :: DKind
con_ki = [DTyVarBndrSpec] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndrSpec]
tvbs [] DCxt
arg_kis DKind
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
$ DKind -> DefunKindInfo
DefunSAK DKind
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
           -> [DTyVarBndrUnit] -- 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 -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrUnit]
tvbs Maybe DKind
m_res_kind = do
  Maybe Fixity
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
  Maybe DKind
m_sak    <- Name -> PrM (Maybe DKind)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DKind)
dsReifyType Name
name
  let defun :: DefunKindInfo -> PrM [DDec]
defun = Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity
  case Maybe DKind
m_sak of
    Just DKind
sak -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DKind -> DefunKindInfo
DefunSAK DKind
sak
    Maybe DKind
Nothing  -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndrUnit] -> Maybe DKind -> DefunKindInfo
DefunNoSAK [DTyVarBndrUnit]
tvbs Maybe DKind
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 DKind
sak ->
      -- Even if a declaration has a SAK, its kind may not be vanilla.
      case DKind -> Either String ([DTyVarBndrSpec], DCxt, DCxt, DKind)
unravelVanillaDType_either DKind
sak of
        -- If the kind isn't vanilla, use the fallback approach.
        -- See Note [Defunctionalization game plan],
        -- Wrinkle 2: Non-vanilla kinds.
        Left String
_ -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sak)
        -- Otherwise, proceed with defun_vanilla_sak.
        Right ([DTyVarBndrSpec]
sak_tvbs, DCxt
_sak_cxt, DCxt
sak_arg_kis, DKind
sak_res_ki)
               -> [DTyVarBndrSpec] -> DCxt -> DKind -> PrM [DDec]
defun_vanilla_sak [DTyVarBndrSpec]
sak_tvbs DCxt
sak_arg_kis DKind
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 [DTyVarBndrUnit]
tvbs Maybe DKind
m_res -> [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback [DTyVarBndrUnit]
tvbs Maybe DKind
m_res
  where
    -- Generate defunctionalization symbols for things with vanilla SAKs.
    -- The symbols themselves will also be given SAKs.
    defun_vanilla_sak :: [DTyVarBndrSpec] -> [DKind] -> DKind -> PrM [DDec]
    defun_vanilla_sak :: [DTyVarBndrSpec] -> DCxt -> DKind -> PrM [DDec]
defun_vanilla_sak [DTyVarBndrSpec]
sak_tvbs DCxt
sak_arg_kis DKind
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"
      let sak_arg_n :: Int
sak_arg_n = DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
sak_arg_kis
      -- Use noExactName below to avoid GHC#17537.
      [Name]
arg_names <- Int -> PrM Name -> PrM [Name]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
sak_arg_n (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 :: a) (y :: b) :: c ~> d ~> Type 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.
          --
          -- Note that the body of ExampleSym2 redundantly includes the
          -- argument kinds and result kind, which are already stated in the
          -- standalone kind signature. This is a deliberate choice.
          -- See Note [Keep redundant kind information for Haddocks]
          -- in D.S.TH.Promote.
          --
          -- 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, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go Int
n [(Name, DKind)]
arg_nks [(Name, DKind)]
res_nkss =
            let arg_tvbs :: [DTyVarBndrUnit]
                arg_tvbs :: [DTyVarBndrUnit]
arg_tvbs = ((Name, DKind) -> DTyVarBndrUnit)
-> [(Name, DKind)] -> [DTyVarBndrUnit]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
na, DKind
ki) -> Name -> () -> DKind -> DTyVarBndrUnit
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
na () DKind
ki) [(Name, DKind)]
arg_nks

                mk_sak_dec :: DKind -> DDec
                mk_sak_dec :: DKind -> DDec
mk_sak_dec DKind
res_ki =
                  Name -> DKind -> DDec
DKiSigD (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n) (DKind -> DDec) -> DKind -> DDec
forall a b. (a -> b) -> a -> b
$
                  [DTyVarBndrSpec] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndrSpec]
sak_tvbs [] (((Name, DKind) -> DKind) -> [(Name, DKind)] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name, DKind) -> DKind
forall a b. (a, b) -> b
snd [(Name, DKind)]
arg_nks) DKind
res_ki in
            case [(Name, DKind)]
res_nkss of
              [] ->
                let sat_sak_dec :: DDec
sat_sak_dec = DKind -> DDec
mk_sak_dec DKind
sak_res_ki
                    sat_decs :: [DDec]
sat_decs    = Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrUnit]
arg_tvbs (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sak_res_ki)
                in (DKind
sak_res_ki, DDec
sat_sak_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
sat_decs)
              (Name, DKind)
res_nk:[(Name, DKind)]
res_nks ->
                let (DKind
res_ki, [DDec]
decs)   = Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([(Name, DKind)]
arg_nks [(Name, DKind)] -> [(Name, DKind)] -> [(Name, DKind)]
forall a. [a] -> [a] -> [a]
++ [(Name, DKind)
res_nk]) [(Name, DKind)]
res_nks
                    tyfun :: DKind
tyfun            = DKind -> DKind -> DKind
buildTyFunArrow ((Name, DKind) -> DKind
forall a b. (a, b) -> b
snd (Name, DKind)
res_nk) DKind
res_ki
                    defun_sak_dec :: DDec
defun_sak_dec    = DKind -> DDec
mk_sak_dec DKind
tyfun
                    defun_other_decs :: [DDec]
defun_other_decs = Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
sak_arg_n
                                                     [DTyVarBndrUnit]
arg_tvbs ((Name, DKind) -> Name
forall a b. (a, b) -> a
fst (Name, DKind)
res_nk)
                                                     Name
extra_name (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
tyfun)
                in (DKind
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 a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ (DKind, [DDec]) -> [DDec]
forall a b. (a, b) -> b
snd ((DKind, [DDec]) -> [DDec]) -> (DKind, [DDec]) -> [DDec]
forall a b. (a -> b) -> a -> b
$ Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go Int
0 [] ([(Name, DKind)] -> (DKind, [DDec]))
-> [(Name, DKind)] -> (DKind, [DDec])
forall a b. (a -> b) -> a -> b
$ [Name] -> DCxt -> [(Name, DKind)]
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 :: [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
    defun_fallback :: [DTyVarBndrUnit] -> Maybe DKind -> PrM [DDec]
defun_fallback [DTyVarBndrUnit]
tvbs' Maybe DKind
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 GHC#11812.
      ([DTyVarBndrUnit]
tvbs, Maybe DKind
m_res) <- [DTyVarBndrUnit]
-> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)
eta_expand ([DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. Data a => a -> a
noExactTyVars [DTyVarBndrUnit]
tvbs') (Maybe DKind -> Maybe DKind
forall a. Data a => a -> a
noExactTyVars Maybe DKind
m_res')

      let tvbs_n :: Int
tvbs_n = [DTyVarBndrUnit] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrUnit]
tvbs

          -- 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 -> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
          go :: Int
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
go Int
n [DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit]
res_tvbss =
            case [DTyVarBndrUnit]
res_tvbss of
              [] ->
                let sat_decs :: [DDec]
sat_decs = Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrUnit]
arg_tvbs Maybe DKind
m_res
                in (Maybe DKind
m_res, [DDec]
sat_decs)
              DTyVarBndrUnit
res_tvb:[DTyVarBndrUnit]
res_tvbs ->
                let (Maybe DKind
m_res_ki, [DDec]
decs) = Int
-> [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> (Maybe DKind, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrUnit
res_tvb]) [DTyVarBndrUnit]
res_tvbs
                    m_tyfun :: Maybe DKind
m_tyfun          = Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe (DTyVarBndrUnit -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrUnit
res_tvb)
                                                             Maybe DKind
m_res_ki
                    defun_decs' :: [DDec]
defun_decs'      = Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
tvbs_n [DTyVarBndrUnit]
arg_tvbs
                                                     (DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrUnit
res_tvb)
                                                     Name
extra_name Maybe DKind
m_tyfun
                in (Maybe DKind
m_tyfun, [DDec]
defun_decs' [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)

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

    mk_defun_decs :: Options
                  -> Int
                  -> Int
                  -> [DTyVarBndrUnit]
                  -> Name
                  -> Name
                  -> Maybe DKind
                  -> [DDec]
    mk_defun_decs :: Options
-> Int
-> Int
-> [DTyVarBndrUnit]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
fully_sat_n [DTyVarBndrUnit]
arg_tvbs Name
tyfun_name Name
extra_name Maybe DKind
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   = (DTyVarBndrUnit -> Name) -> [DTyVarBndrUnit] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrUnit -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndrUnit]
arg_tvbs
          params :: [DTyVarBndrUnit]
params      = [DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [Name -> () -> DTyVarBndrUnit
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
tyfun_name ()]
          con_eq_ct :: DKind
con_eq_ct   = Name -> DKind
DConT Name
sameKindName DKind -> DKind -> DKind
`DAppT` DKind
lhs DKind -> DKind -> DKind
`DAppT` DKind
rhs
            where
              lhs :: DKind
lhs = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
data_name) ((Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT [Name]
arg_names) DKind -> DKind -> DKind
`apply` (Name -> DKind
DVarT Name
extra_name)
              rhs :: DKind
rhs = DKind -> DCxt -> DKind
foldType (Name -> DKind
DConT Name
next_name) ((Name -> DKind) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DKind
DVarT ([Name]
arg_names [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name
extra_name]))
          con_decl :: DCon
con_decl    = [DTyVarBndrSpec] -> DCxt -> Name -> DConFields -> DKind -> DCon
DCon [] [DKind
con_eq_ct] Name
con_name (Bool -> [DBangType] -> DConFields
DNormalC Bool
False [])
                             (DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
data_name) [DTyVarBndrUnit]
params)
          data_decl :: DDec
data_decl   = NewOrData
-> DCxt
-> Name
-> [DTyVarBndrUnit]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD NewOrData
Data [] Name
data_name [DTyVarBndrUnit]
args Maybe DKind
m_tyfun [DCon
con_decl] []
            where
              args :: [DTyVarBndrUnit]
args | Maybe DKind -> Bool
forall a. Maybe a -> Bool
isJust Maybe DKind
m_tyfun = [DTyVarBndrUnit]
arg_tvbs
                   | Bool
otherwise      = [DTyVarBndrUnit]
params
          app_data_ty :: DKind
app_data_ty = DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
data_name) [DTyVarBndrUnit]
arg_tvbs
          app_eqn :: DTySynEqn
app_eqn     = Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                                  (Name -> DKind
DConT Name
applyName DKind -> DKind -> DKind
`DAppT` DKind
app_data_ty
                                                   DKind -> DKind -> DKind
`DAppT` Name -> DKind
DVarT Name
tyfun_name)
                                  (DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
app_eqn_rhs_name)
                                                ([DTyVarBndrUnit]
arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [Name -> () -> DTyVarBndrUnit
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
tyfun_name ()]))
          -- If the next defunctionalization symbol is fully saturated, then
          -- use the original declaration name instead.
          -- See Note [Fully saturated defunctionalization symbols]
          -- (Wrinkle: avoiding reduction stack overflows).
          app_eqn_rhs_name :: Name
app_eqn_rhs_name | Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
fully_sat_n = Name
name
                           | Bool
otherwise          = Name
next_name
          app_decl :: DDec
app_decl    = DTySynEqn -> DDec
DTySynInstD DTySynEqn
app_eqn
          suppress :: DDec
suppress    = Maybe Overlap
-> Maybe [DTyVarBndrUnit] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing []
                          (Name -> DKind
DConT Name
suppressClassName DKind -> DKind -> DKind
`DAppT` DKind
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 a b. (a -> b) -> Maybe a -> Maybe b
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).
    -- See Note [Fully saturated defunctionalization symbols].
    mk_sat_decs :: Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
    mk_sat_decs :: Options -> Int -> [DTyVarBndrUnit] -> Maybe DKind -> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrUnit]
sat_tvbs Maybe DKind
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  = DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD
                       (Name
-> [DTyVarBndrUnit]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
sat_name [DTyVarBndrUnit]
sat_tvbs
                                        (Maybe DKind -> DFamilyResultSig
maybeKindToResultSig Maybe DKind
m_sat_res) Maybe InjectivityAnn
forall a. Maybe a
Nothing)
                       [Maybe [DTyVarBndrUnit] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing
                                  (DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
sat_name) [DTyVarBndrUnit]
sat_tvbs)
                                  (DKind -> [DTyVarBndrUnit] -> DKind
forall flag. DKind -> [DTyVarBndr flag] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
name)     [DTyVarBndrUnit]
sat_tvbs)]
          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 a b. (a -> b) -> Maybe a -> Maybe b
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 :: [DTyVarBndrUnit] -> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)
    eta_expand :: [DTyVarBndrUnit]
-> Maybe DKind -> PrM ([DTyVarBndrUnit], Maybe DKind)
eta_expand [DTyVarBndrUnit]
m_arg_tvbs Maybe DKind
Nothing = ([DTyVarBndrUnit], Maybe DKind)
-> PrM ([DTyVarBndrUnit], Maybe DKind)
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrUnit]
m_arg_tvbs, Maybe DKind
forall a. Maybe a
Nothing)
    eta_expand [DTyVarBndrUnit]
m_arg_tvbs (Just DKind
res_kind) = do
        let (DFunArgs
arg_ks, DKind
result_k) = DKind -> (DFunArgs, DKind)
unravelDType DKind
res_kind
            vis_arg_ks :: [DVisFunArg]
vis_arg_ks = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
arg_ks
        [DTyVarBndrUnit]
extra_arg_tvbs <- (DVisFunArg -> PrM DTyVarBndrUnit)
-> [DVisFunArg] -> PrM [DTyVarBndrUnit]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DVisFunArg -> PrM DTyVarBndrUnit
mk_extra_tvb [DVisFunArg]
vis_arg_ks
        ([DTyVarBndrUnit], Maybe DKind)
-> PrM ([DTyVarBndrUnit], Maybe DKind)
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrUnit]
m_arg_tvbs [DTyVarBndrUnit] -> [DTyVarBndrUnit] -> [DTyVarBndrUnit]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrUnit]
extra_arg_tvbs, DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
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 DTyVarBndrUnit
    mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrUnit
mk_extra_tvb DVisFunArg
vfa =
      case DVisFunArg
vfa of
        DVisFADep DTyVarBndrUnit
tvb -> DTyVarBndrUnit -> PrM DTyVarBndrUnit
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTyVarBndrUnit
tvb
        DVisFAAnon DKind
k  -> (\Name
n -> Name -> () -> DKind -> DTyVarBndrUnit
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
n () DKind
k) (Name -> DTyVarBndrUnit) -> PrM Name -> PrM DTyVarBndrUnit
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                           -- Use noExactName below to avoid GHC#19743.
                           (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
"e")

    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 [DTyVarBndrUnit] (Maybe DKind)

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

buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe Maybe DKind
m_k1 Maybe DKind
m_k2 = DKind -> DKind -> DKind
buildTyFunArrow (DKind -> DKind -> DKind) -> Maybe DKind -> Maybe (DKind -> DKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DKind
m_k1 Maybe (DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DKind
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 = Foo x y z

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

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 family, not a data type. These sorts of symbols are referred
  to as "fully saturated" defunctionalization symbols.
  See Note [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.TH.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-th` 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 = Not x

  type family NotSym1 x where
    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 family BarSym3 x (y :: Nat) (z :: Nat) :: Nat where ...

-----
-- 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 BazSym1 :: forall a. a -> forall b. b ~> Type
  data BazSym1 x f where ...

  type BazSym2 :: forall a. a -> forall b. b -> Type
  type family BazSym2 x y where
    BazSym2 x y = Baz x y

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 family BazSym2 (x :: a) (y :: b) :: Type where ...

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 family QuuxSym2 (k :: Type) (x :: k) :: Type where ...

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 [Fully saturated defunctionalization symbols]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When generating defunctionalization symbols, most of the symbols are data
types. The last one, however, is a type family. 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 :: a -> b -> a
  type family ConstSym2 x y where
    ConstSym2 x y = Const x y

ConstSym2, the sole type family 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 almost never appear directly in user-written code. Instead,
they are most valuable in TH-generated code, as singletons-th often generates code
that directly applies a defunctionalization symbol to some number of arguments
(see, for instance, D.S.TH.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.

One might wonder if, instead of using a closed type family with a single
equation, we could use a type synonym to define ConstSym2:

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

This approach has various downsides which make it impractical:

* Type synonyms are often not expanded in the output of GHCi's :kind! command.
  As issue #445 chronicles, this can significantly impact the readability of
  even simple :kind! queries. It can be the difference between this:

    λ> :kind! Map IdSym0 '[1,2,3]
    Map IdSym0 '[1,2,3] :: [Nat]
    = 1 :@#@$$$ '[2, 3]

  And this:

    λ> :kind! Map IdSym0 '[1,2,3]
    Map IdSym0 '[1,2,3] :: [Nat]
    = '[1, 2, 3]

  Making fully saturated defunctionalization symbols like (:@#@$$$) type
  families makes this issue moot, since :kind! always expands type families.
* There are a handful of corner cases where using type synonyms can actually
  make fully saturated defunctionalization symbols fail to typecheck.
  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.

  Making (*>@#@$$$) a type family rather than a type synonym avoids this issue
  since type family equations are allowed to match on kind arguments. In this
  example, (*>@#@$$$) would have kind-polymorphic `f`, `a`, and `b` in its kind
  signature, but its equation would implicitly equate `k` with `Type`. Note
  that (*>@#@$) and (*>@#@$$), which are GADTs, also use a similar trick by
  equating `k` with `Type` in their GADT constructors.

-----
-- Wrinkle: avoiding reduction stack overflows
-----

A naïve attempt at declaring all fully saturated defunctionalization symbols
as type families can make certain programs overflow the reduction stack, such
as the T445 test case. This is because when evaluating
`FSym0 `Apply` x_1 `Apply` ... `Apply` x_N`, (where F is a promoted function
that requires N arguments), we will eventually bottom out by evaluating
`FSymN x_1 ... x_N`, where FSymN is a fully saturated defunctionalization
symbol. Since FSymN is a type family, this is yet another type family
reduction that contributes to the overall reduction limit. This might not
seem like a lot, but it can add up if F is invoked several times in a single
type-level computation!

Fortunately, we can bypass evaluating FSymN entirely by just making a slight
tweak to the TH machinery. Instead of generating this Apply instance:

  type instance Apply (FSym{N-1} x_1 ... x_{N-1}) x_N =
    FSymN x_1 ... x_{N-1} x_N

Generate this instance, which jumps straight to F:

  type instance Apply (FSym{N-1} x_1 ... x_{N-1}) x_N =
    F x_1 ... x_{N-1} x_N

Now evaluating `FSym0 `Apply` x_1 `Apply` ... `Apply` x_N` will require one
less type family reduction. In practice, this is usually enough to keep the
reduction limit at bay in most situations.

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.
-}