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