    {- 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 qualified Language.Haskell.TH.Desugar.OSet as OSet
    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.Util
    import Control.Monad
    import Data.Foldable
    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 dec :: DDec
    dec _instances :: Maybe [DDec]
    _instances) = DDec -> PrM [DDec]
    buildDefunSyms DDec
    dec
    defunInfo (DPrimTyConI _name :: Name
    _name _numArgs :: Int
    _numArgs _unlifted :: 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
    $ "Building defunctionalization symbols of primitive " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
             "type constructors not supported"
    defunInfo (DVarI _name :: Name
    _name _ty :: DType
    _ty _mdec :: Maybe Name
    _mdec) =
      String -> PrM [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Building defunctionalization symbols of values not supported"
    defunInfo (DTyVarI _name :: Name
    _name _ty :: DType
    _ty) =
      String -> PrM [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Building defunctionalization symbols of type variables not supported"
    defunInfo (DPatSynI {}) =
      String -> PrM [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Building defunctionalization symbols of pattern synonyms not supported"

    defunTypeDecls :: [TySynDecl]
                   -> [ClosedTypeFamilyDecl]
                   -> [OpenTypeFamilyDecl]
                   -> PrM ()
    defunTypeDecls :: [TySynDecl]
    -> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
    defunTypeDecls ty_syns :: [TySynDecl]
    ty_syns c_tyfams :: [ClosedTypeFamilyDecl]
    c_tyfams o_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
    name tvbs :: [DTyVarBndr]
    tvbs rhs :: 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

    buildDefunSyms :: DDec -> PrM [DDec]
    buildDefunSyms :: DDec -> PrM [DDec]
    buildDefunSyms (DDataD _new_or_data :: NewOrData
    _new_or_data _cxt :: DCxt
    _cxt _tyName :: Name
    _tyName _tvbs :: [DTyVarBndr]
    _tvbs _k :: Maybe DType
    _k ctors :: [DCon]
    ctors _derivings :: [DDerivClause]
    _derivings) =
      [DCon] -> PrM [DDec]
    buildDefunSymsDataD [DCon]
    ctors
    buildDefunSyms (DClosedTypeFamilyD tf_head :: DTypeFamilyHead
    tf_head _) =
      DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsClosedTypeFamilyD DTypeFamilyHead
    tf_head
    buildDefunSyms (DOpenTypeFamilyD tf_head :: DTypeFamilyHead
    tf_head) =
      DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsOpenTypeFamilyD DTypeFamilyHead
    tf_head
    buildDefunSyms (DTySynD name :: Name
    name tvbs :: [DTyVarBndr]
    tvbs rhs :: DType
    rhs) =
      Name -> [DTyVarBndr] -> DType -> PrM [DDec]
    buildDefunSymsTySynD Name
    name [DTyVarBndr]
    tvbs DType
    rhs
    buildDefunSyms (DClassD _cxt :: DCxt
    _cxt name :: Name
    name tvbs :: [DTyVarBndr]
    tvbs _fundeps :: [FunDep]
    _fundeps _members :: [DDec]
    _members) = do
      Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunReifyFixity Name
    name [DTyVarBndr]
    tvbs (DType -> Maybe DType
    forall a. a -> Maybe a
    Just (Name -> DType
    DConT Name
    constraintName))
    buildDefunSyms _ = 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
    $ "Defunctionalization symbols can only be built for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
                              "type families and data declarations"

    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

    buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsOpenTypeFamilyD = (DTyVarBndr -> DTyVarBndr)
    -> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsTypeFamilyHead DTyVarBndr -> DTyVarBndr
    cuskify Maybe DType -> Maybe DType
    default_to_star
      where
        default_to_star :: Maybe DKind -> Maybe DKind
        default_to_star :: Maybe DType -> Maybe DType
    default_to_star Nothing  = DType -> Maybe DType
    forall a. a -> Maybe a
    Just (DType -> Maybe DType) -> DType -> Maybe DType
    forall a b. (a -> b) -> a -> b
    $ Name -> DType
    DConT Name
    typeKindName
        default_to_star (Just k :: DType
    k) = DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    k

    buildDefunSymsTypeFamilyHead
      :: (DTyVarBndr -> DTyVarBndr)
      -> (Maybe DKind -> Maybe DKind)
      -> DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsTypeFamilyHead :: (DTyVarBndr -> DTyVarBndr)
    -> (Maybe DType -> Maybe DType) -> DTypeFamilyHead -> PrM [DDec]
    buildDefunSymsTypeFamilyHead default_tvb :: DTyVarBndr -> DTyVarBndr
    default_tvb default_kind :: Maybe DType -> Maybe DType
    default_kind
        (DTypeFamilyHead name :: Name
    name tvbs :: [DTyVarBndr]
    tvbs result_sig :: DFamilyResultSig
    result_sig _) = 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]
    defunReifyFixity Name
    name [DTyVarBndr]
    arg_tvbs Maybe DType
    res_kind

    buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec]
    buildDefunSymsTySynD :: Name -> [DTyVarBndr] -> DType -> PrM [DDec]
    buildDefunSymsTySynD name :: Name
    name tvbs :: [DTyVarBndr]
    tvbs rhs :: DType
    rhs =
      Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunReifyFixity Name
    name [DTyVarBndr]
    tvbs Maybe DType
    mb_res_kind
      where
        -- In order to have a CUSK, a type synonym must annotate its right-hand
        -- side with an explicit kind signature, so we can make use of this
        -- property to determine the result kind when defunctionalizing the
        -- type synonym.
        mb_res_kind :: Maybe DKind
        mb_res_kind :: Maybe DType
    mb_res_kind = case DType
    rhs of
                        DSigT _ k :: DType
    k -> DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    k
                        _         -> Maybe DType
    forall a. Maybe a
    Nothing

    buildDefunSymsDataD :: [DCon] -> PrM [DDec]
    buildDefunSymsDataD :: [DCon] -> PrM [DDec]
    buildDefunSymsDataD ctors :: [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 ctor :: DCon
    ctor@(DCon _ _ _ _ res_ty :: DType
    res_ty) = do
          let (name :: Name
    name, arg_tys :: DCxt
    arg_tys) = DCon -> (Name, DCxt)
    extractNameTypes DCon
    ctor
          [Name]
    tvb_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
    arg_tys) (PrM Name -> PrM [Name]) -> PrM Name -> PrM [Name]
    forall a b. (a -> b) -> a -> b
    $ String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "t"
          DCxt
    arg_kis <- (DType -> PrM DType) -> DCxt -> PrM DCxt
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> PrM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DCxt
    arg_tys
          let arg_tvbs :: [DTyVarBndr]
    arg_tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DType -> DTyVarBndr
    DKindedTV [Name]
    tvb_names DCxt
    arg_kis
          DType
    res_ki <- DType -> PrM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    res_ty
          Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunReifyFixity Name
    name [DTyVarBndr]
    arg_tvbs (DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    res_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]
    defunReifyFixity :: Name -> [DTyVarBndr] -> Maybe DKind -> PrM [DDec]
    defunReifyFixity :: Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunReifyFixity name :: Name
    name tvbs :: [DTyVarBndr]
    tvbs m_res_kind :: 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
      Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunctionalize Name
    name Maybe Fixity
    m_fixity [DTyVarBndr]
    tvbs Maybe DType
    m_res_kind

    -- Generate data declarations and apply instances
    -- required for defunctionalization.
    -- For a type family:
    --
    -- type family Foo (m :: Nat) (n :: Nat) (l :: Nat) :: Nat
    --
    -- we generate data declarations that allow us to talk about partial
    -- application at the type level:
    --
    -- type FooSym3 a b c = Foo a b c
    -- data FooSym2 a b f where
    --   FooSym2KindInference :: SameKind (Apply (FooSym2 a b) arg) (FooSym3 a b arg)
    --                        => FooSym2 a b f
    -- type instance Apply (FooSym2 a b) c = FooSym3 a b c
    -- data FooSym1 a f where
    --   FooSym1KindInference :: SameKind (Apply (FooSym1 a) arg) (FooSym2 a arg)
    --                        => FooSym1 a f
    -- type instance Apply (FooSym1 a) b = FooSym2 a b
    -- data FooSym0 f where
    --  FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg)
    --                       => FooSym0 f
    -- type instance Apply FooSym0 a = FooSym1 a
    --
    -- What's up with all the "KindInference" stuff? In some scenarios, we don't
    -- know the kinds that we should be using in these symbols. But, GHC can figure
    -- it out using the types of the "KindInference" dummy data constructors. A
    -- bit of a hack, but it works quite nicely. The only problem is that GHC will
    -- warn about an unused data constructor. So, we use the data constructor in
    -- an instance of a dummy class. (See Data.Singletons.SuppressUnusedWarnings
    -- for the class, which should never be seen by anyone, ever.)
    --
    -- The defunctionalize function takes Maybe DKinds so that the caller can
    -- indicate which kinds are known and which need to be inferred.
    --
    -- See also Note [Defunctionalization and dependent quantification]
    defunctionalize :: Name
                    -> Maybe Fixity -- The name's fixity, if one was declared.
                    -> [DTyVarBndr] -> Maybe DKind -> PrM [DDec]
    defunctionalize :: Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunctionalize name :: Name
    name m_fixity :: Maybe Fixity
    m_fixity m_arg_tvbs' :: [DTyVarBndr]
    m_arg_tvbs' m_res_kind' :: Maybe DType
    m_res_kind' = do
      (m_arg_tvbs :: [DTyVarBndr]
    m_arg_tvbs, m_res_kind :: Maybe DType
    m_res_kind) <- [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType)
    eta_expand ([DTyVarBndr] -> [DTyVarBndr]
    forall a. Data a => a -> a
    noExactTyVars [DTyVarBndr]
    m_arg_tvbs')
                                             (Maybe DType -> Maybe DType
    forall a. Data a => a -> a
    noExactTyVars Maybe DType
    m_res_kind')

      let -- Implements part (2)(i) from Note [Defunctionalization and dependent quantification]
          tvb_to_type_map :: Map Name DType
          tvb_to_type_map :: Map Name DType
    tvb_to_type_map = [(Name, DType)] -> Map Name DType
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([(Name, DType)] -> Map Name DType)
    -> [(Name, DType)] -> Map Name DType
    forall a b. (a -> b) -> a -> b
    $                   -- (2)(i)(c)
                            (DTyVarBndr -> (Name, DType)) -> [DTyVarBndr] -> [(Name, DType)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\tvb :: DTyVarBndr
    tvb -> (DTyVarBndr -> Name
    extractTvbName DTyVarBndr
    tvb, DTyVarBndr -> DType
    dTyVarBndrToDType DTyVarBndr
    tvb)) ([DTyVarBndr] -> [(Name, DType)])
    -> [DTyVarBndr] -> [(Name, DType)]
    forall a b. (a -> b) -> a -> b
    $
                            DCxt -> [DTyVarBndr]
    toposortTyVarsOf (DCxt -> [DTyVarBndr]) -> DCxt -> [DTyVarBndr]
    forall a b. (a -> b) -> a -> b
    $               -- (2)(i)(b)
                            (DTyVarBndr -> DType) -> [DTyVarBndr] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> DType
    dTyVarBndrToDType [DTyVarBndr]
    m_arg_tvbs
                              DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ Maybe DType -> DCxt
    forall a. Maybe a -> [a]
    maybeToList Maybe DType
    m_res_kind      -- (2)(i)(a)

          go :: Int -> [DTyVarBndr] -> Maybe DKind
             -> ([DTyVarBndr] -> DType)  -- given the argument tyvar binders,
                                         -- produce the RHS of the Apply instance
             -> PrM [DDec]
          go :: Int
    -> [DTyVarBndr]
    -> Maybe DType
    -> ([DTyVarBndr] -> DType)
    -> PrM [DDec]
    go _ [] _ _ = [DDec] -> PrM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          go n :: Int
    n (m_arg :: DTyVarBndr
    m_arg : m_args :: [DTyVarBndr]
    m_args) m_result :: Maybe DType
    m_result mk_rhs :: [DTyVarBndr] -> DType
    mk_rhs = do
            Name
    extra_name <- String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "arg"
            let tyfun_name :: Name
    tyfun_name  = DTyVarBndr -> Name
    extractTvbName DTyVarBndr
    m_arg
                data_name :: Name
    data_name   = Name -> Int -> Name
    promoteTySym Name
    name Int
    n
                next_name :: Name
    next_name   = Name -> Int -> Name
    promoteTySym Name
    name (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1)
                con_name :: Name
    con_name    = String -> String -> Name -> Name
    prefixName "" ":" (Name -> Name) -> Name -> Name
    forall a b. (a -> b) -> a -> b
    $ String -> String -> Name -> Name
    suffixName "KindInference" "###" Name
    data_name
                m_tyfun :: Maybe DType
    m_tyfun     = Maybe DType -> Maybe DType -> Maybe DType
    buildTyFunArrow_maybe (DTyVarBndr -> Maybe DType
    extractTvbKind DTyVarBndr
    m_arg) Maybe DType
    m_result
                arg_params :: [DTyVarBndr]
    arg_params  = -- Implements part (2)(ii) from
                              -- Note [Defunctionalization and dependent quantification]
                              (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map ((DType -> DType) -> DTyVarBndr -> DTyVarBndr
    map_tvb_kind (Map Name DType -> DType -> DType
    substType Map Name DType
    tvb_to_type_map)) ([DTyVarBndr] -> [DTyVarBndr]) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a b. (a -> b) -> a -> b
    $
                              [DTyVarBndr] -> [DTyVarBndr]
    forall a. [a] -> [a]
    reverse [DTyVarBndr]
    m_args
                arg_names :: [Name]
    arg_names   = (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    arg_params
                params :: [DTyVarBndr]
    params      = [DTyVarBndr]
    arg_params [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 ((DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> DTyVarBndr
    dropTvbKind [DTyVarBndr]
    params [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. [a] -> [a] -> [a]
    ++ [Name -> DTyVarBndr
    DPlainTV Name
    extra_name])
                                   [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
    res_ki [DCon
    con_decl] []
                  where
                    (args :: [DTyVarBndr]
    args, res_ki :: Maybe DType
    res_ki)
                      = case Maybe DType
    m_tyfun of
                          Nothing    -> ([DTyVarBndr]
    params, Maybe DType
    forall a. Maybe a
    Nothing)
                                        -- If we cannot infer the return type, don't bother
                                        -- trying to construct an explicit return kind.
                          Just tyfun :: DType
    tyfun ->
                            let bound_tvs :: OSet Name
    bound_tvs = [Name] -> OSet Name
    forall a. Ord a => [a] -> OSet a
    OSet.fromList ((DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    arg_params)
                                            OSet Name -> OSet Name -> OSet Name
    forall a. Ord a => OSet a -> OSet a -> OSet a
    `OSet.union` (Maybe DType -> OSet Name) -> [Maybe DType] -> OSet Name
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((DType -> OSet Name) -> Maybe DType -> OSet Name
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap DType -> OSet Name
    fvDType)
                                                                 ((DTyVarBndr -> Maybe DType) -> [DTyVarBndr] -> [Maybe DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Maybe DType
    extractTvbKind [DTyVarBndr]
    arg_params)
                                not_bound :: DTyVarBndr -> Bool
    not_bound tvb :: DTyVarBndr
    tvb = Bool -> Bool
    not (DTyVarBndr -> Name
    extractTvbName DTyVarBndr
    tvb Name -> OSet Name -> Bool
    forall a. Ord a => a -> OSet a -> Bool
    `OSet.member` OSet Name
    bound_tvs)
                                tvb_to_type :: Name -> DType
    tvb_to_type tvb_name :: Name
    tvb_name = DType -> Maybe DType -> DType
    forall a. a -> Maybe a -> a
    fromMaybe (Name -> DType
    DVarT Name
    tvb_name) (Maybe DType -> DType) -> Maybe DType -> DType
    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
    tvb_name Map Name DType
    tvb_to_type_map
                                -- Implements part (2)(iii) from
                                -- Note [Defunctionalization and dependent quantification]
                                tyfun_tvbs :: [DTyVarBndr]
    tyfun_tvbs = (DTyVarBndr -> Bool) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter DTyVarBndr -> Bool
    not_bound ([DTyVarBndr] -> [DTyVarBndr]) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a b. (a -> b) -> a -> b
    $     -- (2)(iii)(d)
                                             DCxt -> [DTyVarBndr]
    toposortTyVarsOf (DCxt -> [DTyVarBndr]) -> DCxt -> [DTyVarBndr]
    forall a b. (a -> b) -> a -> b
    $     -- (2)(iii)(c)
                                             (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    tvb_to_type ([Name] -> DCxt) -> [Name] -> DCxt
    forall a b. (a -> b) -> a -> b
    $      -- (2)(iii)(b)
                                             OSet Name -> [Name]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    toList (OSet Name -> [Name]) -> OSet Name -> [Name]
    forall a b. (a -> b) -> a -> b
    $ DType -> OSet Name
    fvDType DType
    tyfun -- (2)(iii)(a)
                            in ([DTyVarBndr]
    arg_params, DType -> Maybe DType
    forall a. a -> Maybe a
    Just ([DTyVarBndr] -> DCxt -> DType -> DType
    DForallT [DTyVarBndr]
    tyfun_tvbs [] DType
    tyfun))
                app_data_ty :: DType
    app_data_ty = DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    data_name) [DTyVarBndr]
    m_args
                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)
                                        ([DTyVarBndr] -> DType
    mk_rhs ([DTyVarBndr]
    m_args [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 []])]]

                mk_rhs' :: [DTyVarBndr] -> DType
    mk_rhs'     = DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    data_name)

                -- See Note [Fixity declarations for defunctionalization symbols]
                mk_fix_decl :: Fixity -> DDec
    mk_fix_decl f :: Fixity
    f = DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Fixity -> Name -> DLetDec
    DInfixD Fixity
    f Name
    data_name
                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 Fixity -> DDec
    mk_fix_decl Maybe Fixity
    m_fixity

            [DDec]
    decls <- Int
    -> [DTyVarBndr]
    -> Maybe DType
    -> ([DTyVarBndr] -> DType)
    -> PrM [DDec]
    go (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) [DTyVarBndr]
    m_args Maybe DType
    m_tyfun [DTyVarBndr] -> DType
    mk_rhs'
            [DDec] -> PrM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
    forall a b. (a -> b) -> a -> b
    $ DDec
    suppress DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    : DDec
    data_decl DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    : DDec
    app_decl DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    : [DDec]
    fixity_decl [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    decls

      let num_args :: Int
    num_args = [DTyVarBndr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [DTyVarBndr]
    m_arg_tvbs
          sat_name :: Name
    sat_name = Name -> Int -> Name
    promoteTySym Name
    name Int
    num_args
          mk_rhs :: [DTyVarBndr] -> DType
    mk_rhs   = DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    name)
          sat_dec :: DDec
    sat_dec  = Name -> [DTyVarBndr] -> DType -> DDec
    DTySynD Name
    sat_name [DTyVarBndr]
    m_arg_tvbs ([DTyVarBndr] -> DType
    mk_rhs [DTyVarBndr]
    m_arg_tvbs)

      [DDec]
    other_decs <- Int
    -> [DTyVarBndr]
    -> Maybe DType
    -> ([DTyVarBndr] -> DType)
    -> PrM [DDec]
    go (Int
    num_args Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1) ([DTyVarBndr] -> [DTyVarBndr]
    forall a. [a] -> [a]
    reverse [DTyVarBndr]
    m_arg_tvbs) Maybe DType
    m_res_kind [DTyVarBndr] -> DType
    mk_rhs
      [DDec] -> PrM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> PrM [DDec]) -> [DDec] -> PrM [DDec]
    forall a b. (a -> b) -> a -> b
    $ DDec
    sat_dec DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    : [DDec]
    other_decs
      where
        eta_expand :: [DTyVarBndr] -> Maybe DKind -> PrM ([DTyVarBndr], Maybe DKind)
        eta_expand :: [DTyVarBndr] -> Maybe DType -> PrM ([DTyVarBndr], Maybe DType)
    eta_expand m_arg_tvbs :: [DTyVarBndr]
    m_arg_tvbs 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 m_arg_tvbs :: [DTyVarBndr]
    m_arg_tvbs (Just res_kind :: DType
    res_kind) = do
            let (_, _, argKs :: DCxt
    argKs, resultK :: DType
    resultK) = DType -> ([DTyVarBndr], DCxt, DCxt, DType)
    unravel DType
    res_kind
            [Name]
    tvb_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
    argKs) (PrM Name -> PrM [Name]) -> PrM Name -> PrM [Name]
    forall a b. (a -> b) -> a -> b
    $ String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "e"
            let res_kind_arg_tvbs :: [DTyVarBndr]
    res_kind_arg_tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DType -> DTyVarBndr
    DKindedTV [Name]
    tvb_names DCxt
    argKs
            ([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]
    res_kind_arg_tvbs, DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    resultK)

        map_tvb_kind :: (DKind -> DKind) -> DTyVarBndr -> DTyVarBndr
        map_tvb_kind :: (DType -> DType) -> DTyVarBndr -> DTyVarBndr
    map_tvb_kind _ tvb :: DTyVarBndr
    tvb@DPlainTV{}  = DTyVarBndr
    tvb
        map_tvb_kind f :: DType -> DType
    f (DKindedTV n :: Name
    n k :: DType
    k) = Name -> DType -> DTyVarBndr
    DKindedTV Name
    n (DType -> DType
    f DType
    k)

    {-
    Note [Defunctionalization and dependent quantification]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    The machinery in this module supports defunctionalizing types that use
    dependent quantification, such as in the following example:

      type family Symmetry (a :: Proxy t) (y :: Proxy t)
                           (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k))) :: Type where
        Symmetry a y _ = y :~: a

    Here is what is involved in making this happen:

    1. When defunctionalizing, we must not only know the argument kinds, but rather
       the argument *kind variable binders*. This is essential since, for instance,
       Symmetry dependently quantifies `a` and `y` and uses them in the kind of
       `e`. If we did not track the original kind variable names, then instead of
       generating this defunctionalization symbol for Symmetry:

         data SymmetrySym2 (a :: Proxy t) (y :: Proxy t) :: (a :~: y) ~> Type

       We would generate something more general, like this:

         data SymmetrySym2 (abc1 :: Proxy t) (abc2 :: Proxy t) :: (a :~: y) ~> Type

       Alas, there are times where will have no choice but to write a slightly
       more general kind than we should. For instance, consider this:

         data SymmetrySym0 :: Proxy t ~> Proxy t ~> (a :~: y) ~> Type

       This defunctionalization symbol doesn't capture the dependent quantification
       in the first and second argument kinds. But in order to do that properly,
       you'd need the ability to write something like:

         data SymmetrySym0 :: forall (a :: Proxy t) ~> forall (y :: Proxy t)
                           ~> (a :~: y) ~> Type

       It is my (RGS's) belief that it is not possible to achieve something like
       this in today's GHC (see #304), so we'll just have to live with SymmetrySym0
       being slightly more general than it ought to be. In practice, this is
       unlikely to bite unless you're writing code that specifically exploits this
       dependency in just the right way.

    2. I pulled a fast one earlier by writing:

         data SymmetrySym0 :: Proxy t ~> Proxy t ~> (a :~: y) ~> Type

       GHC will actually reject this, because it does not have a CUSK. There are
       two glaring problems here:

       (a) The kind of `t` is underdetermined.
       (b) `a` and `y` should have kind `Proxy t`, but this is not currently the case.

       Ultimately, the fix is to use explicit kind signatures. A naïve attempt
       would be something like this:

         data SymmetrySym0 :: Proxy (t :: (k :: Type)) ~> Proxy (t :: (k :: Type))
                           ~> ((a :: Proxy (t :: (k :: Type))) :~: (y :: Proxy (t :: (k :: Type))))
                           ~> Type

       While that works, it adds a nontrivial amount of clutter. Plus, it requires
       figuring out (in Template Haskell) which variables have underdetermined
       kinds and substituting for them. Blegh. A much cleaner approach is:

         data SymmetrySym0 :: forall (k :: Type) (t :: k) (a :: Proxy t) (y :: Proxy t).
                              Proxy t ~> Proxy t ~> (a :~: y) ~> Type

       This time, all we have to do is put an explicit `forall` in front, and we
       achieve a CUSK without having to muck up the body of return kind. It also
       has the benefit of looking much nicer in generated code.

       Let's talk about how to achieve this feat, using SymmetrySym1 as the
       guiding example:

       (i) Before we begin defunctionalizing a type, we construct a mapping from
           variable names to their corresponding types, complete with kinds.
           For instance, in Symmetry, we would have the following map:

             { k :-> DVarT k                                         -- k
             , t :-> DSigT (DVarT t) (DVarT k)                       -- (t :: k)
             , a :-> DSigT (DVarT a) (DConT ''Proxy `DAppT` DVarT t) -- (a :: Proxy t)
             , y :-> DSigT (DVarT y) (DConT ''Proxy `DAppT` DVarT y) -- (y :: Proxy t)
             , e :-> DSigT (DVarT e) (DConT ''(:~:)
                                      `DAppT` DSigT (DVarT a) (DConT ''Proxy `DAppT` DSigT (DVarT t) (DVarT k))
                                      `DAppT` DSigT (DVarT y) (DConT ''Proxy `DAppT` DSigT (DVarT t) (DVarT k)))
                                                                     -- (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k)))
             }

           Why do this? Because when constructing the `forall` in the return kind
           of a defunctionalization symbol, it's convenient to be able to know
           the kinds of everything being bound at a glance. It's not always
           possible to recover the kinds of every variable (for instance, if
           we're just given `Proxy t ~> Proxy t ~> (a :~: y) ~> Type`), so having
           this information is handy.

           To construct this map, we:

           (a) Grab the list of type variable binders (this is given as an input
               to defunctionalize, as discussed in part (1)) and turn it into a list
               of types. Also include the return kind (if there is one) in this
               list, as it may also mention type variables with explicit kinds.
           (b) Construct a flat list of all type variables mentioned in this list.
               This may involve looking in the kinds of type variables binders.
               (Note that this part is crucial—the the Singletons/PolyKinds test
               will fail to compile without it!)
           (c) Take the flat list and insert each variable into the map by
               mapping its name to its type (as demonstrated above).

           To continue the Symmetry example:

           (a) We grab the list of type variable binders

                 [ (a :: Proxy t)
                 , (y :: Proxy t)
                 , (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k)))
                 ]

               from the Symmetry declaration. Including the return kind (Type),
               we get:

                 [ (a :: Proxy t)
                 , (y :: Proxy t)
                 , (e :: (a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k)))
                 , Type
                 ]

           (b) We flatten this into a list of well scoped type variables:

                 [ k
                 , (t :: k)
                 , (a :: Proxy t)
                 , (y :: Proxy t)
                 , (e :: (a :: Proxy (t :: k)) :~: (y :~: Proxy (t :: k)))
                 ]

           (c) From this, we construct the map shown at the beginning of (i).

       (ii) Using the map, we will annotate any kind variables in the LHS of the
            declaration with their respective kinds. In this example, the LHS is:

              data SymmetrySym1 (a :: Proxy t) :: ...

            Since `t` maps to simply `(t :: k)` in the map, the LHS becomes:

              data SymmetrySym1 (a :: Proxy (t :: k)) :: ...

            Why do this? Because we need to make it apparent that `k` is bound on
            the LHS. If we don't, we might end up trying to quantify `k` in the
            return kind (see #353 for an example of what goes wrong if you try to
            do this).

            Having to explicitly annotate each occurrence of every kind variable on
            the LHS like this is a bit tiresome, especially since we don't have to
            do this in the return kind. If GHC had syntax for visible dependent
            quantification, we could avoid this step entirely and simply write:

              data SymmetrySym1 :: forall k (t :: k). forall (a :: Proxy t) -> ...

            Until GHC gains this syntax, this is the best alternative.

       (iii) When constructing each defunctionalization symbol, we will end up with
             some remaining type variable binders and a return kind. For instance:

               data SymmetrySym1 (a :: Proxy (t :: k))
                 :: forall ???. Proxy t
                             ~> ((a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k)))
                             ~> Type

             We must fill in the ??? part. Here is how we do so:

             (a) Collect all of the type variables mentioned in the return kind.
             (b) Look up each type variable's corresponding type in the map (from
                 part (i)) to learn as much kind information as possible.
             (c) Perform a reverse topological sort on these types to put the
                 types (and kind) variables in proper dependency order.
             (d) Filter out any variables that are already bound by the type
                 variable binders that precede the return kind.

             After doing these steps, what remains goes in place of ???. Let's
             explain this with the example above:

               data SymmetrySym1 (a :: Proxy (t :: k))
                 :: forall ???. Proxy t
                             ~> ((a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k)))
                             ~> Type

             (a) [t, a, k, y]
             (b) [(t :: k), (a :: Proxy t), k, (y :: Proxy t)]
             (c) [k, (t :: k), (a :: Proxy t), (y :: Proxy t)]
             (d) [(y :: Proxy t)] (`k`, `t` and `a` were already bound)

             Therefore, we end up with:

               data SymmetrySym1 (a :: Proxy (t :: k))
                 :: forall (y :: Proxy t).
                                Proxy t
                             ~> ((a :: Proxy (t :: k)) :~: (y :: Proxy (t :: k)))
                             ~> Type
    -}

    -- This is a small function with large importance. When generating
    -- defunctionalization data types, we often need to fill in the blank in the
    -- sort of code exemplified below:
    --
    -- @
    -- data FooSym2 a (b :: x) (c :: TyFun y z) where
    --   FooSym2KindInference :: _
    -- @
    --
    -- Where the kind of @a@ is not known. It's extremely tempting to just
    -- copy-and-paste the type variable binders from the data type itself to the
    -- constructor, like so:
    --
    -- @
    -- data FooSym2 a (b :: x) (c :: TyFun y z) where
    --   FooSym2KindInference :: forall a (b :: x) (c :: TyFun y z).
    --                           SameKind (...) (...).
    --                           FooSym2KindInference a b c
    -- @
    --
    -- But this ends up being an untenable approach. Because @a@ lacks a kind
    -- signature, @FooSym2@ does not have a complete, user-specified kind signature
    -- (or CUSK), so GHC will fail to typecheck @FooSym2KindInference@.
    --
    -- Thankfully, there's a workaround—just don't give any of the constructor's
    -- type variable binders any kinds:
    --
    -- @
    -- data FooSym2 a (b :: x) (c :: TyFun y z) where
    --   FooSym2KindInference :: forall a b c
    --                           SameKind (...) (...).
    --                           FooSym2KindInference a b c
    -- @
    --
    -- GHC may be moody when it comes to CUSKs, but it's at least understanding
    -- enough to typecheck this without issue. The 'dropTvbKind' function is
    -- what removes the kinds used in the kind inference constructor.
    dropTvbKind :: DTyVarBndr -> DTyVarBndr
    dropTvbKind :: DTyVarBndr -> DTyVarBndr
    dropTvbKind tvb :: DTyVarBndr
    tvb@(DPlainTV {}) = DTyVarBndr
    tvb
    dropTvbKind (DKindedTV n :: Name
    n _)   = Name -> DTyVarBndr
    DPlainTV Name
    n

    -- Shorthand for building (k1 ~> k2)
    buildTyFunArrow :: DKind -> DKind -> DKind
    buildTyFunArrow :: DType -> DType -> DType
    buildTyFunArrow k1 :: DType
    k1 k2 :: 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 m_k1 :: Maybe DType
    m_k1 m_k2 :: Maybe DType
    m_k2 = do
      DType
    k1 <- Maybe DType
    m_k1
      DType
    k2 <- Maybe DType
    m_k2
      DType -> Maybe DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> Maybe DType) -> DType -> Maybe DType
    forall a b. (a -> b) -> a -> b
    $ Name -> DType
    DConT Name
    tyFunArrowName DType -> DType -> DType
    `DAppT` DType
    k1 DType -> DType -> DType
    `DAppT` DType
    k2

    -- Build (~>) kind from the list of kinds
    ravelTyFun :: [DKind] -> DKind
    ravelTyFun :: DCxt -> DType
    ravelTyFun []    = String -> DType
    forall a. HasCallStack => String -> a
    error "Internal error: TyFun raveling nil"
    ravelTyFun [k :: DType
    k]   = DType
    k
    ravelTyFun kinds :: DCxt
    kinds = DCxt -> DType -> DType
    go DCxt
    tailK (DType -> DType -> DType
    buildTyFunArrow DType
    k2 DType
    k1)
        where (k1 :: DType
    k1 : k2 :: DType
    k2 : tailK :: DCxt
    tailK) = DCxt -> DCxt
    forall a. [a] -> [a]
    reverse DCxt
    kinds
              go :: DCxt -> DType -> DType
    go []     acc :: DType
    acc = DType
    acc
              go (k :: DType
    k:ks :: DCxt
    ks) acc :: DType
    acc = DCxt -> DType -> DType
    go DCxt
    ks (DType -> DType -> DType
    buildTyFunArrow DType
    k DType
    acc)

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