    {- Data/Singletons/Promote.hs

    (c) Richard Eisenberg 2013
    rae@cs.brynmawr.edu

    This file contains functions to promote term-level constructs to the
    type level. It is an internal module to the singletons package.
    -}

    {-# LANGUAGE TemplateHaskell, MultiWayIf, LambdaCase, TupleSections #-}

    module Data.Singletons.Promote where

    import Language.Haskell.TH hiding ( Q, cxt )
    import Language.Haskell.TH.Syntax ( Quasi(..) )
    import Language.Haskell.TH.Desugar
    import qualified Language.Haskell.TH.Desugar.OMap.Strict as OMap
    import Language.Haskell.TH.Desugar.OMap.Strict (OMap)
    import qualified Language.Haskell.TH.Desugar.OSet as OSet
    import Language.Haskell.TH.Desugar.OSet (OSet)
    import Data.Singletons.Names
    import Data.Singletons.Promote.Monad
    import Data.Singletons.Promote.Eq
    import Data.Singletons.Promote.Defun
    import Data.Singletons.Promote.Type
    import Data.Singletons.Deriving.Ord
    import Data.Singletons.Deriving.Bounded
    import Data.Singletons.Deriving.Enum
    import Data.Singletons.Deriving.Show
    import Data.Singletons.Deriving.Util
    import Data.Singletons.Partition
    import Data.Singletons.Util
    import Data.Singletons.Syntax
    import Prelude hiding (exp)
    import Control.Applicative (Alternative(..))
    import Control.Arrow (second)
    import Control.Monad
    import Control.Monad.Trans.Maybe
    import Control.Monad.Writer
    import qualified Data.Map.Strict as Map
    import Data.Map.Strict ( Map )
    import Data.Maybe
    import qualified GHC.LanguageExtensions.Type as LangExt

    -- | Generate promoted definitions from a type that is already defined.
    -- This is generally only useful with classes.
    genPromotions :: DsMonad q => [Name] -> q [Dec]
    genPromotions :: [Name] -> q [Dec]
    genPromotions names :: [Name]
    names = do
      [Name] -> q ()
    forall (q :: * -> *). Quasi q => [Name] -> q ()
    checkForRep [Name]
    names
      [Info]
    infos <- (Name -> q Info) -> [Name] -> q [Info]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Name -> q Info
    forall (q :: * -> *). DsMonad q => Name -> q Info
    reifyWithLocals [Name]
    names
      [DInfo]
    dinfos <- (Info -> q DInfo) -> [Info] -> q [DInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Info -> q DInfo
    forall (q :: * -> *). DsMonad q => Info -> q DInfo
    dsInfo [Info]
    infos
      [DDec]
    ddecs <- [Dec] -> PrM () -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
    promoteM_ [] (PrM () -> q [DDec]) -> PrM () -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ (DInfo -> PrM ()) -> [DInfo] -> PrM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ DInfo -> PrM ()
    promoteInfo [DInfo]
    dinfos
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH [DDec]
    ddecs

    -- | Promote every declaration given to the type level, retaining the originals.
    promote :: DsMonad q => q [Dec] -> q [Dec]
    promote :: q [Dec] -> q [Dec]
    promote qdec :: q [Dec]
    qdec = do
      [Dec]
    decls <- q [Dec]
    qdec
      [DDec]
    ddecls <- [Dec] -> DsM q [DDec] -> q [DDec]
    forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
    withLocalDeclarations [Dec]
    decls (DsM q [DDec] -> q [DDec]) -> DsM q [DDec] -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ [Dec] -> DsM q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> q [DDec]
    dsDecs [Dec]
    decls
      [DDec]
    promDecls <- [Dec] -> PrM () -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
    promoteM_ [Dec]
    decls (PrM () -> q [DDec]) -> PrM () -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> PrM ()
    promoteDecs [DDec]
    ddecls
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [Dec]
    decls [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec] -> [Dec]
    decsToTH [DDec]
    promDecls

    -- | Promote each declaration, discarding the originals. Note that a promoted
    -- datatype uses the same definition as an original datatype, so this will
    -- not work with datatypes. Classes, instances, and functions are all fine.
    promoteOnly :: DsMonad q => q [Dec] -> q [Dec]
    promoteOnly :: q [Dec] -> q [Dec]
    promoteOnly qdec :: q [Dec]
    qdec = do
      [Dec]
    decls  <- q [Dec]
    qdec
      [DDec]
    ddecls <- [Dec] -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> q [DDec]
    dsDecs [Dec]
    decls
      [DDec]
    promDecls <- [Dec] -> PrM () -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
    promoteM_ [Dec]
    decls (PrM () -> q [DDec]) -> PrM () -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> PrM ()
    promoteDecs [DDec]
    ddecls
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH [DDec]
    promDecls

    -- | Generate defunctionalization symbols for existing type families.
    --
    -- 'genDefunSymbols' has reasonable support for type families that use
    -- dependent quantification. For instance, this:
    --
    -- @
    -- type family MyProxy k (a :: k) :: Type where
    --   MyProxy k (a :: k) = Proxy a
    --
    -- $('genDefunSymbols' [''MyProxy])
    -- @
    --
    -- Will generate the following defunctionalization symbols:
    --
    -- @
    -- data MyProxySym0     :: Type  ~> k ~> Type
    -- data MyProxySym1 (k  :: Type) :: k ~> Type
    -- @
    --
    -- Note that @MyProxySym0@ is a bit more general than it ought to be, since
    -- there is no dependency between the first kind (@Type@) and the second kind
    -- (@k@). But this would require the ability to write something like:
    --
    -- @
    -- data MyProxySym0 :: forall (k :: Type) ~> k ~> Type
    -- @
    --
    -- Which currently isn't possible. So for the time being, the kind of
    -- @MyProxySym0@ will be slightly more general, which means that under rare
    -- circumstances, you may have to provide extra type signatures if you write
    -- code which exploits the dependency in @MyProxy@'s kind.
    genDefunSymbols :: DsMonad q => [Name] -> q [Dec]
    genDefunSymbols :: [Name] -> q [Dec]
    genDefunSymbols names :: [Name]
    names = do
      [Name] -> q ()
    forall (q :: * -> *). Quasi q => [Name] -> q ()
    checkForRep [Name]
    names
      [DInfo]
    infos <- (Name -> q DInfo) -> [Name] -> q [DInfo]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Info -> q DInfo
    forall (q :: * -> *). DsMonad q => Info -> q DInfo
    dsInfo (Info -> q DInfo) -> (Name -> q Info) -> Name -> q DInfo
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< Name -> q Info
    forall (q :: * -> *). DsMonad q => Name -> q Info
    reifyWithLocals) [Name]
    names
      [DDec]
    decs <- [Dec] -> PrM [DDec] -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> PrM [DDec] -> q [DDec]
    promoteMDecs [] (PrM [DDec] -> q [DDec]) -> PrM [DDec] -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ (DInfo -> PrM [DDec]) -> [DInfo] -> PrM [DDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM DInfo -> PrM [DDec]
    defunInfo [DInfo]
    infos
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH [DDec]
    decs

    -- | Produce instances for @(==)@ (type-level equality) from the given types
    promoteEqInstances :: DsMonad q => [Name] -> q [Dec]
    promoteEqInstances :: [Name] -> q [Dec]
    promoteEqInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM Name -> q [Dec]
    forall (q :: * -> *). DsMonad q => Name -> q [Dec]
    promoteEqInstance

    -- | Produce instances for 'POrd' from the given types
    promoteOrdInstances :: DsMonad q => [Name] -> q [Dec]
    promoteOrdInstances :: [Name] -> q [Dec]
    promoteOrdInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM Name -> q [Dec]
    forall (q :: * -> *). DsMonad q => Name -> q [Dec]
    promoteOrdInstance

    -- | Produce an instance for 'POrd' from the given type
    promoteOrdInstance :: DsMonad q => Name -> q [Dec]
    promoteOrdInstance :: Name -> q [Dec]
    promoteOrdInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    promoteInstance DerivDesc q
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkOrdInstance "Ord"

    -- | Produce instances for 'PBounded' from the given types
    promoteBoundedInstances :: DsMonad q => [Name] -> q [Dec]
    promoteBoundedInstances :: [Name] -> q [Dec]
    promoteBoundedInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM Name -> q [Dec]
    forall (q :: * -> *). DsMonad q => Name -> q [Dec]
    promoteBoundedInstance

    -- | Produce an instance for 'PBounded' from the given type
    promoteBoundedInstance :: DsMonad q => Name -> q [Dec]
    promoteBoundedInstance :: Name -> q [Dec]
    promoteBoundedInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    promoteInstance DerivDesc q
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkBoundedInstance "Bounded"

    -- | Produce instances for 'PEnum' from the given types
    promoteEnumInstances :: DsMonad q => [Name] -> q [Dec]
    promoteEnumInstances :: [Name] -> q [Dec]
    promoteEnumInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM Name -> q [Dec]
    forall (q :: * -> *). DsMonad q => Name -> q [Dec]
    promoteEnumInstance

    -- | Produce an instance for 'PEnum' from the given type
    promoteEnumInstance :: DsMonad q => Name -> q [Dec]
    promoteEnumInstance :: Name -> q [Dec]
    promoteEnumInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    promoteInstance DerivDesc q
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkEnumInstance "Enum"

    -- | Produce instances for 'PShow' from the given types
    promoteShowInstances :: DsMonad q => [Name] -> q [Dec]
    promoteShowInstances :: [Name] -> q [Dec]
    promoteShowInstances = (Name -> q [Dec]) -> [Name] -> q [Dec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM Name -> q [Dec]
    forall (q :: * -> *). DsMonad q => Name -> q [Dec]
    promoteShowInstance

    -- | Produce an instance for 'PShow' from the given type
    promoteShowInstance :: DsMonad q => Name -> q [Dec]
    promoteShowInstance :: Name -> q [Dec]
    promoteShowInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    promoteInstance (ShowMode -> DerivDesc q
    forall (q :: * -> *). DsMonad q => ShowMode -> DerivDesc q
    mkShowInstance ShowMode
    ForPromotion) "Show"

    -- | Produce an instance for @(==)@ (type-level equality) from the given type
    promoteEqInstance :: DsMonad q => Name -> q [Dec]
    promoteEqInstance :: Name -> q [Dec]
    promoteEqInstance name :: Name
    name = do
      (tvbs :: [TyVarBndr]
    tvbs, cons :: [Con]
    cons) <- String -> Name -> q ([TyVarBndr], [Con])
    forall (q :: * -> *).
    DsMonad q =>
    String -> Name -> q ([TyVarBndr], [Con])
    getDataD "I cannot make an instance of (==) for it." Name
    name
      [DTyVarBndr]
    tvbs' <- (TyVarBndr -> q DTyVarBndr) -> [TyVarBndr] -> q [DTyVarBndr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TyVarBndr -> q DTyVarBndr
    forall (q :: * -> *). DsMonad q => TyVarBndr -> q DTyVarBndr
    dsTvb [TyVarBndr]
    tvbs
      let data_ty :: DType
    data_ty = DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    name) [DTyVarBndr]
    tvbs'
      [DCon]
    cons' <- (Con -> q [DCon]) -> [Con] -> q [DCon]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM ([DTyVarBndr] -> DType -> Con -> q [DCon]
    forall (q :: * -> *).
    DsMonad q =>
    [DTyVarBndr] -> DType -> Con -> q [DCon]
    dsCon [DTyVarBndr]
    tvbs' DType
    data_ty) [Con]
    cons
      DType
    kind <- DType -> q DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType (DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    name) [DTyVarBndr]
    tvbs')
      [DDec]
    inst_decs <- DType -> [DCon] -> q [DDec]
    forall (q :: * -> *). Quasi q => DType -> [DCon] -> q [DDec]
    mkEqTypeInstance DType
    kind [DCon]
    cons'
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH [DDec]
    inst_decs

    promoteInstance :: DsMonad q => DerivDesc q -> String -> Name -> q [Dec]
    promoteInstance :: DerivDesc q -> String -> Name -> q [Dec]
    promoteInstance mk_inst :: DerivDesc q
    mk_inst class_name :: String
    class_name name :: Name
    name = do
      (tvbs :: [TyVarBndr]
    tvbs, cons :: [Con]
    cons) <- String -> Name -> q ([TyVarBndr], [Con])
    forall (q :: * -> *).
    DsMonad q =>
    String -> Name -> q ([TyVarBndr], [Con])
    getDataD ("I cannot make an instance of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    class_name
                                String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for it.") Name
    name
      [DTyVarBndr]
    tvbs' <- (TyVarBndr -> q DTyVarBndr) -> [TyVarBndr] -> q [DTyVarBndr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TyVarBndr -> q DTyVarBndr
    forall (q :: * -> *). DsMonad q => TyVarBndr -> q DTyVarBndr
    dsTvb [TyVarBndr]
    tvbs
      let data_ty :: DType
    data_ty   = DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    name) [DTyVarBndr]
    tvbs'
      [DCon]
    cons' <- (Con -> q [DCon]) -> [Con] -> q [DCon]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM ([DTyVarBndr] -> DType -> Con -> q [DCon]
    forall (q :: * -> *).
    DsMonad q =>
    [DTyVarBndr] -> DType -> Con -> q [DCon]
    dsCon [DTyVarBndr]
    tvbs' DType
    data_ty) [Con]
    cons
      let data_decl :: DataDecl
    data_decl = Name -> [DTyVarBndr] -> [DCon] -> DataDecl
    DataDecl Name
    name [DTyVarBndr]
    tvbs' [DCon]
    cons'
      UInstDecl
    raw_inst <- DerivDesc q
    mk_inst Maybe DCxt
    forall a. Maybe a
    Nothing DType
    data_ty DataDecl
    data_decl
      [DDec]
    decs <- [Dec] -> PrM () -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> PrM () -> q [DDec]
    promoteM_ [] (PrM () -> q [DDec]) -> PrM () -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ PrM AInstDecl -> PrM ()
    forall (f :: * -> *) a. Functor f => f a -> f ()
    void (PrM AInstDecl -> PrM ()) -> PrM AInstDecl -> PrM ()
    forall a b. (a -> b) -> a -> b
    $ OMap Name DType -> UInstDecl -> PrM AInstDecl
    promoteInstanceDec OMap Name DType
    forall k v. OMap k v
    OMap.empty UInstDecl
    raw_inst
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH [DDec]
    decs

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

    -- Note [Promoting declarations in two stages]
    -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    --
    -- It is necessary to know the types of things when promoting. So,
    -- we promote in two stages: first, we build a LetDecEnv, which allows
    -- for easy lookup. Then, we go through the actual elements of the LetDecEnv,
    -- performing the promotion.
    --
    -- Why do we need the types? For kind annotations on the type family. We also
    -- need to have both the types and the actual function definition at the same
    -- time, because the function definition tells us how many patterns are
    -- matched. Note that an eta-contracted function needs to return a TyFun,
    -- not a proper type-level function.
    --
    -- Consider this example:
    --
    --   foo :: Nat -> Bool -> Bool
    --   foo Zero = id
    --   foo _    = not
    --
    -- Here the first parameter to foo is non-uniform, because it is
    -- inspected in a pattern and can be different in each defining
    -- equation of foo. The second parameter to foo, specified in the type
    -- signature as Bool, is a uniform parameter - it is not inspected and
    -- each defining equation of foo uses it the same way. The foo
    -- function will be promoted to a type familty Foo like this:
    --
    --   type family Foo (n :: Nat) :: Bool ~> Bool where
    --      Foo Zero = Id
    --      Foo a    = Not
    --
    -- To generate type signature for Foo type family we must first learn
    -- what is the actual number of patterns used in defining cequations
    -- of foo. In this case there is only one so we declare Foo to take
    -- one argument and have return type of Bool -> Bool.

    -- Promote a list of top-level declarations.
    promoteDecs :: [DDec] -> PrM ()
    promoteDecs :: [DDec] -> PrM ()
    promoteDecs raw_decls :: [DDec]
    raw_decls = do
      [DDec]
    decls <- [DDec] -> PrM [DDec]
    forall (q :: * -> *) a. (DsMonad q, Data a) => a -> q a
    expand [DDec]
    raw_decls     -- expand type synonyms
      [DDec] -> PrM ()
    forall (q :: * -> *). Quasi q => [DDec] -> q ()
    checkForRepInDecls [DDec]
    decls
      PDecs { pd_let_decs :: PartitionedDecs -> [DLetDec]
    pd_let_decs                = [DLetDec]
    let_decs
            , pd_class_decs :: PartitionedDecs -> [UClassDecl]
    pd_class_decs              = [UClassDecl]
    classes
            , pd_instance_decs :: PartitionedDecs -> [UInstDecl]
    pd_instance_decs           = [UInstDecl]
    insts
            , pd_data_decs :: PartitionedDecs -> [DataDecl]
    pd_data_decs               = [DataDecl]
    datas
            , pd_ty_syn_decs :: PartitionedDecs -> [TySynDecl]
    pd_ty_syn_decs             = [TySynDecl]
    ty_syns
            , pd_open_type_family_decs :: PartitionedDecs -> [OpenTypeFamilyDecl]
    pd_open_type_family_decs   = [OpenTypeFamilyDecl]
    o_tyfams
            , pd_closed_type_family_decs :: PartitionedDecs -> [ClosedTypeFamilyDecl]
    pd_closed_type_family_decs = [ClosedTypeFamilyDecl]
    c_tyfams
            , pd_derived_eq_decs :: PartitionedDecs -> [DerivedEqDecl]
    pd_derived_eq_decs         = [DerivedEqDecl]
    derived_eq_decs } <- [DDec] -> PrM PartitionedDecs
    forall (m :: * -> *). DsMonad m => [DDec] -> m PartitionedDecs
    partitionDecs [DDec]
    decls

      [TySynDecl]
    -> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
    defunTypeDecls [TySynDecl]
    ty_syns [ClosedTypeFamilyDecl]
    c_tyfams [OpenTypeFamilyDecl]
    o_tyfams
        -- promoteLetDecs returns LetBinds, which we don't need at top level
      ([LetBind], ALetDecEnv)
    _ <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
    promoteLetDecs (String, String)
    noPrefix [DLetDec]
    let_decs
      (UClassDecl -> PrM AClassDecl) -> [UClassDecl] -> PrM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ UClassDecl -> PrM AClassDecl
    promoteClassDec [UClassDecl]
    classes
      let orig_meth_sigs :: OMap Name DType
    orig_meth_sigs = (UClassDecl -> OMap Name DType) -> [UClassDecl] -> OMap Name DType
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap (LetDecEnv Unannotated -> OMap Name DType
    forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
    lde_types (LetDecEnv Unannotated -> OMap Name DType)
    -> (UClassDecl -> LetDecEnv Unannotated)
    -> UClassDecl
    -> OMap Name DType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . UClassDecl -> LetDecEnv Unannotated
    forall (ann :: AnnotationFlag). ClassDecl ann -> LetDecEnv ann
    cd_lde) [UClassDecl]
    classes
      (UInstDecl -> PrM AInstDecl) -> [UInstDecl] -> PrM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (OMap Name DType -> UInstDecl -> PrM AInstDecl
    promoteInstanceDec OMap Name DType
    orig_meth_sigs) [UInstDecl]
    insts
      (DerivedEqDecl -> PrM ()) -> [DerivedEqDecl] -> PrM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ DerivedEqDecl -> PrM ()
    promoteDerivedEqDec   [DerivedEqDecl]
    derived_eq_decs
      [DataDecl] -> PrM ()
    promoteDataDecs [DataDecl]
    datas

    promoteDataDecs :: [DataDecl] -> PrM ()
    promoteDataDecs :: [DataDecl] -> PrM ()
    promoteDataDecs data_decs :: [DataDecl]
    data_decs = do
      [DLetDec]
    rec_selectors <- (DataDecl -> PrM [DLetDec]) -> [DataDecl] -> PrM [DLetDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM DataDecl -> PrM [DLetDec]
    extract_rec_selectors [DataDecl]
    data_decs
      ([LetBind], ALetDecEnv)
    _ <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
    promoteLetDecs (String, String)
    noPrefix [DLetDec]
    rec_selectors
      (DataDecl -> PrM ()) -> [DataDecl] -> PrM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ DataDecl -> PrM ()
    promoteDataDec [DataDecl]
    data_decs
      where
        extract_rec_selectors :: DataDecl -> PrM [DLetDec]
        extract_rec_selectors :: DataDecl -> PrM [DLetDec]
    extract_rec_selectors (DataDecl data_name :: Name
    data_name tvbs :: [DTyVarBndr]
    tvbs cons :: [DCon]
    cons) =
          let arg_ty :: DType
    arg_ty = DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    data_name) [DTyVarBndr]
    tvbs
          in
          DType -> [DCon] -> PrM [DLetDec]
    forall (q :: * -> *). DsMonad q => DType -> [DCon] -> q [DLetDec]
    getRecordSelectors DType
    arg_ty [DCon]
    cons

    -- curious about ALetDecEnv? See the LetDecEnv module for an explanation.
    promoteLetDecs :: (String, String) -- (alpha, symb) prefixes to use
                   -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
      -- See Note [Promoting declarations in two stages]
    promoteLetDecs :: (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
    promoteLetDecs prefixes :: (String, String)
    prefixes decls :: [DLetDec]
    decls = do
      LetDecEnv Unannotated
    let_dec_env <- [DLetDec] -> PrM (LetDecEnv Unannotated)
    forall (q :: * -> *).
    Quasi q =>
    [DLetDec] -> q (LetDecEnv Unannotated)
    buildLetDecEnv [DLetDec]
    decls
      [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals
      let binds :: [LetBind]
    binds = [ (Name
    name, DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    sym) ((Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals))
                  | (name :: Name
    name, _) <- OMap Name (LetDecRHS Unannotated)
    -> [(Name, LetDecRHS Unannotated)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs (OMap Name (LetDecRHS Unannotated)
     -> [(Name, LetDecRHS Unannotated)])
    -> OMap Name (LetDecRHS Unannotated)
    -> [(Name, LetDecRHS Unannotated)]
    forall a b. (a -> b) -> a -> b
    $ LetDecEnv Unannotated -> OMap Name (LetDecRHS Unannotated)
    forall (ann :: AnnotationFlag).
    LetDecEnv ann -> OMap Name (LetDecRHS ann)
    lde_defns LetDecEnv Unannotated
    let_dec_env
                  , let proName :: Name
    proName = (String, String) -> Name -> Name
    promoteValNameLhsPrefix (String, String)
    prefixes Name
    name
                        sym :: Name
    sym = Name -> Int -> Name
    promoteTySym Name
    proName ([Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Name]
    all_locals) ]
      (decs :: [DDec]
    decs, let_dec_env' :: ALetDecEnv
    let_dec_env') <- [LetBind] -> PrM ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv)
    forall a. [LetBind] -> PrM a -> PrM a
    letBind [LetBind]
    binds (PrM ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv))
    -> PrM ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv)
    forall a b. (a -> b) -> a -> b
    $ (String, String)
    -> LetDecEnv Unannotated -> PrM ([DDec], ALetDecEnv)
    promoteLetDecEnv (String, String)
    prefixes LetDecEnv Unannotated
    let_dec_env
      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DDec]
    decs
      ([LetBind], ALetDecEnv) -> PrM ([LetBind], ALetDecEnv)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([LetBind]
    binds, ALetDecEnv
    let_dec_env' { lde_proms :: IfAnn Annotated (OMap Name DType) ()
    lde_proms = [LetBind] -> OMap Name DType
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList [LetBind]
    binds })

    -- Promotion of data types to kinds is automatic (see "Giving Haskell a
    -- Promotion" paper for more details). Here we "plug into" the promotion
    -- mechanism to add some extra stuff to the promotion:
    --
    --  * if data type derives Eq we generate a type family that implements the
    --    equality test for the data type.
    --
    --  * for each data constructor with arity greater than 0 we generate type level
    --    symbols for use with Apply type family. In this way promoted data
    --    constructors and promoted functions can be used in a uniform way at the
    --    type level in the same way they can be used uniformly at the type level.
    --
    --  * for each nullary data constructor we generate a type synonym
    promoteDataDec :: DataDecl -> PrM ()
    promoteDataDec :: DataDecl -> PrM ()
    promoteDataDec (DataDecl _name :: Name
    _name _tvbs :: [DTyVarBndr]
    _tvbs ctors :: [DCon]
    ctors) = do
      [DDec]
    ctorSyms <- [DCon] -> PrM [DDec]
    buildDefunSymsDataD [DCon]
    ctors
      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DDec]
    ctorSyms

    -- Note [CUSKification]
    -- ~~~~~~~~~~~~~~~~~~~~
    -- GHC #12928 means that sometimes, this TH code will produce a declaration
    -- that has a kind signature even when we want kind inference to work. There
    -- seems to be no way to avoid this, so we embrace it:
    --
    --   * If a class type variable has no explicit kind, we make no effort to
    --     guess it and default to *. This is OK because before GHC 8.0, we were
    --     limited by KProxy anyway.
    --
    --   * If a class type variable has an explicit kind, it is preserved.
    --
    -- This way, we always get proper CUSKs where we need them.

    promoteClassDec :: UClassDecl
                    -> PrM AClassDecl
    promoteClassDec :: UClassDecl -> PrM AClassDecl
    promoteClassDec decl :: UClassDecl
    decl@(ClassDecl { cd_name :: forall (ann :: AnnotationFlag). ClassDecl ann -> Name
    cd_name = Name
    cls_name
                                    , cd_tvbs :: forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndr]
    cd_tvbs = [DTyVarBndr]
    tvbs'
                                    , cd_fds :: forall (ann :: AnnotationFlag). ClassDecl ann -> [FunDep]
    cd_fds  = [FunDep]
    fundeps
                                    , cd_lde :: forall (ann :: AnnotationFlag). ClassDecl ann -> LetDecEnv ann
    cd_lde  = lde :: LetDecEnv Unannotated
    lde@LetDecEnv
                                        { lde_defns :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> OMap Name (LetDecRHS ann)
    lde_defns = OMap Name (LetDecRHS Unannotated)
    defaults
                                        , lde_types :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
    lde_types = OMap Name DType
    meth_sigs
                                        , lde_infix :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name Fixity
    lde_infix = OMap Name Fixity
    infix_decls } }) = do
      let
        -- a workaround for GHC Trac #12928; see Note [CUSKification]
        tvbs :: [DTyVarBndr]
    tvbs = (DTyVarBndr -> DTyVarBndr) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> DTyVarBndr
    cuskify [DTyVarBndr]
    tvbs'
      let pClsName :: Name
    pClsName = Name -> Name
    promoteClassName Name
    cls_name
      OSet Name -> PrM AClassDecl -> PrM AClassDecl
    forall a. OSet Name -> PrM a -> PrM a
    forallBind OSet Name
    cls_kvs_to_bind (PrM AClassDecl -> PrM AClassDecl)
    -> PrM AClassDecl -> PrM AClassDecl
    forall a b. (a -> b) -> a -> b
    $ do
        [DDec]
    sig_decs <- (LetBind -> PrM DDec) -> [LetBind] -> PrM [DDec]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Name -> DType -> PrM DDec) -> LetBind -> PrM DDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> DType -> PrM DDec
    promote_sig) (OMap Name DType -> [LetBind]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name DType
    meth_sigs)
        let defaults_list :: [(Name, LetDecRHS Unannotated)]
    defaults_list  = OMap Name (LetDecRHS Unannotated)
    -> [(Name, LetDecRHS Unannotated)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name (LetDecRHS Unannotated)
    defaults
            defaults_names :: [Name]
    defaults_names = ((Name, LetDecRHS Unannotated) -> Name)
    -> [(Name, LetDecRHS Unannotated)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, LetDecRHS Unannotated) -> Name
    forall a b. (a, b) -> a
    fst [(Name, LetDecRHS Unannotated)]
    defaults_list
        (default_decs :: [DDec]
    default_decs, ann_rhss :: [ALetDecRHS]
    ann_rhss, prom_rhss :: DCxt
    prom_rhss)
          <- ((Name, LetDecRHS Unannotated) -> PrM (DDec, ALetDecRHS, DType))
    -> [(Name, LetDecRHS Unannotated)]
    -> PrM ([DDec], [ALetDecRHS], DCxt)
    forall (m :: * -> *) a b c d.
    Monad m =>
    (a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
    mapAndUnzip3M (OMap Name DType
    -> Maybe (Map Name DType)
    -> OMap Name DType
    -> (Name, LetDecRHS Unannotated)
    -> PrM (DDec, ALetDecRHS, DType)
    promoteMethod OMap Name DType
    forall k v. OMap k v
    OMap.empty Maybe (Map Name DType)
    forall a. Maybe a
    Nothing OMap Name DType
    meth_sigs) [(Name, LetDecRHS Unannotated)]
    defaults_list

        let infix_decls' :: [DDec]
    infix_decls' = [Maybe DDec] -> [DDec]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe DDec] -> [DDec]) -> [Maybe DDec] -> [DDec]
    forall a b. (a -> b) -> a -> b
    $ ((Name, Fixity) -> Maybe DDec) -> [(Name, Fixity)] -> [Maybe DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name -> Fixity -> Maybe DDec) -> (Name, Fixity) -> Maybe DDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Fixity -> Maybe DDec
    promoteInfixDecl)
                                     ([(Name, Fixity)] -> [Maybe DDec])
    -> [(Name, Fixity)] -> [Maybe DDec]
    forall a b. (a -> b) -> a -> b
    $ OMap Name Fixity -> [(Name, Fixity)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name Fixity
    infix_decls

        -- no need to do anything to the fundeps. They work as is!
        [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DCxt -> Name -> [DTyVarBndr] -> [FunDep] -> [DDec] -> DDec
    DClassD [] Name
    pClsName [DTyVarBndr]
    tvbs [FunDep]
    fundeps
                          ([DDec]
    sig_decs [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    default_decs [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    infix_decls')]
        let defaults_list' :: [(Name, ALetDecRHS)]
    defaults_list'   = [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    defaults_names [ALetDecRHS]
    ann_rhss
            proms :: [LetBind]
    proms            = [Name] -> DCxt -> [LetBind]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    defaults_names DCxt
    prom_rhss
            cls_kvs_to_bind' :: OMap Name (OSet Name)
    cls_kvs_to_bind' = OSet Name
    cls_kvs_to_bind OSet Name -> OMap Name DType -> OMap Name (OSet Name)
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ OMap Name DType
    meth_sigs
        AClassDecl -> PrM AClassDecl
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UClassDecl
    decl { cd_lde :: ALetDecEnv
    cd_lde = LetDecEnv Unannotated
    lde { lde_defns :: OMap Name ALetDecRHS
    lde_defns     = [(Name, ALetDecRHS)] -> OMap Name ALetDecRHS
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList [(Name, ALetDecRHS)]
    defaults_list'
                                    , lde_proms :: IfAnn Annotated (OMap Name DType) ()
    lde_proms     = [LetBind] -> OMap Name DType
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList [LetBind]
    proms
                                    , lde_bound_kvs :: IfAnn Annotated (OMap Name (OSet Name)) ()
    lde_bound_kvs = OMap Name (OSet Name)
    IfAnn Annotated (OMap Name (OSet Name)) ()
    cls_kvs_to_bind' } })
      where
        cls_kvb_names, cls_tvb_names, cls_kvs_to_bind :: OSet Name
        cls_kvb_names :: OSet Name
    cls_kvb_names   = (DTyVarBndr -> OSet Name) -> [DTyVarBndr] -> 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 (Maybe DType -> OSet Name)
    -> (DTyVarBndr -> Maybe DType) -> DTyVarBndr -> OSet Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DTyVarBndr -> Maybe DType
    extractTvbKind) [DTyVarBndr]
    tvbs'
        cls_tvb_names :: OSet Name
    cls_tvb_names   = [Name] -> OSet Name
    forall a. Ord a => [a] -> OSet a
    OSet.fromList ([Name] -> OSet Name) -> [Name] -> OSet Name
    forall a b. (a -> b) -> a -> b
    $ (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    tvbs'
        cls_kvs_to_bind :: OSet Name
    cls_kvs_to_bind = OSet Name
    cls_kvb_names OSet Name -> OSet Name -> OSet Name
    forall a. Ord a => OSet a -> OSet a -> OSet a
    `OSet.union` OSet Name
    cls_tvb_names

        promote_sig :: Name -> DType -> PrM DDec
        promote_sig :: Name -> DType -> PrM DDec
    promote_sig name :: Name
    name ty :: DType
    ty = do
          let proName :: Name
    proName = Name -> Name
    promoteValNameLhs Name
    name
          (argKs :: DCxt
    argKs, resK :: DType
    resK) <- DType -> PrM (DCxt, DType)
    forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
    promoteUnraveled DType
    ty
          [Name]
    args <- (DType -> PrM Name) -> DCxt -> PrM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (PrM Name -> DType -> PrM Name
    forall a b. a -> b -> a
    const (PrM Name -> DType -> PrM Name) -> PrM Name -> DType -> PrM Name
    forall a b. (a -> b) -> a -> b
    $ String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "arg") DCxt
    argKs
          let tvbs :: [DTyVarBndr]
    tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DType -> DTyVarBndr
    DKindedTV [Name]
    args DCxt
    argKs
          PrM [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => m [DDec] -> m ()
    emitDecsM (PrM [DDec] -> PrM ()) -> PrM [DDec] -> PrM ()
    forall a b. (a -> b) -> a -> b
    $ Name -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunReifyFixity Name
    proName [DTyVarBndr]
    tvbs (DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    resK)

          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
    $ DTypeFamilyHead -> DDec
    DOpenTypeFamilyD (Name
    -> [DTyVarBndr]
    -> DFamilyResultSig
    -> Maybe InjectivityAnn
    -> DTypeFamilyHead
    DTypeFamilyHead Name
    proName
                                                     [DTyVarBndr]
    tvbs
                                                     (DType -> DFamilyResultSig
    DKindSig DType
    resK)
                                                     Maybe InjectivityAnn
    forall a. Maybe a
    Nothing)

    -- returns (unpromoted method name, ALetDecRHS) pairs
    promoteInstanceDec :: OMap Name DType -> UInstDecl -> PrM AInstDecl
    promoteInstanceDec :: OMap Name DType -> UInstDecl -> PrM AInstDecl
    promoteInstanceDec orig_meth_sigs :: OMap Name DType
    orig_meth_sigs
                       decl :: UInstDecl
    decl@(InstDecl { id_name :: forall (ann :: AnnotationFlag). InstDecl ann -> Name
    id_name     = Name
    cls_name
                                      , id_arg_tys :: forall (ann :: AnnotationFlag). InstDecl ann -> DCxt
    id_arg_tys  = DCxt
    inst_tys
                                      , id_sigs :: forall (ann :: AnnotationFlag). InstDecl ann -> OMap Name DType
    id_sigs     = OMap Name DType
    inst_sigs
                                      , id_meths :: forall (ann :: AnnotationFlag).
    InstDecl ann -> [(Name, LetDecRHS ann)]
    id_meths    = [(Name, LetDecRHS Unannotated)]
    meths }) = do
      [Name]
    cls_tvb_names <- PrM [Name]
    lookup_cls_tvb_names
      DCxt
    inst_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
    inst_tys
      let kvs_to_bind :: OSet Name
    kvs_to_bind = (DType -> OSet Name) -> DCxt -> OSet Name
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap DType -> OSet Name
    fvDType DCxt
    inst_kis
      OSet Name -> PrM AInstDecl -> PrM AInstDecl
    forall a. OSet Name -> PrM a -> PrM a
    forallBind OSet Name
    kvs_to_bind (PrM AInstDecl -> PrM AInstDecl) -> PrM AInstDecl -> PrM AInstDecl
    forall a b. (a -> b) -> a -> b
    $ do
        let subst :: Map Name DType
    subst = [LetBind] -> Map Name DType
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([LetBind] -> Map Name DType) -> [LetBind] -> Map Name DType
    forall a b. (a -> b) -> a -> b
    $ [Name] -> DCxt -> [LetBind]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    cls_tvb_names DCxt
    inst_kis
        (meths' :: [DDec]
    meths', ann_rhss :: [ALetDecRHS]
    ann_rhss, _) <- ((Name, LetDecRHS Unannotated) -> PrM (DDec, ALetDecRHS, DType))
    -> [(Name, LetDecRHS Unannotated)]
    -> PrM ([DDec], [ALetDecRHS], DCxt)
    forall (m :: * -> *) a b c d.
    Monad m =>
    (a -> m (b, c, d)) -> [a] -> m ([b], [c], [d])
    mapAndUnzip3M (OMap Name DType
    -> Maybe (Map Name DType)
    -> OMap Name DType
    -> (Name, LetDecRHS Unannotated)
    -> PrM (DDec, ALetDecRHS, DType)
    promoteMethod OMap Name DType
    inst_sigs (Map Name DType -> Maybe (Map Name DType)
    forall a. a -> Maybe a
    Just Map Name DType
    subst) OMap Name DType
    orig_meth_sigs) [(Name, LetDecRHS Unannotated)]
    meths
        [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [Maybe Overlap
    -> Maybe [DTyVarBndr] -> DCxt -> DType -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing [] (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    pClsName)
                                                  DCxt
    inst_kis) [DDec]
    meths']
        AInstDecl -> PrM AInstDecl
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UInstDecl
    decl { id_meths :: [(Name, ALetDecRHS)]
    id_meths = [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (((Name, LetDecRHS Unannotated) -> Name)
    -> [(Name, LetDecRHS Unannotated)] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, LetDecRHS Unannotated) -> Name
    forall a b. (a, b) -> a
    fst [(Name, LetDecRHS Unannotated)]
    meths) [ALetDecRHS]
    ann_rhss })
      where
        pClsName :: Name
    pClsName = Name -> Name
    promoteClassName Name
    cls_name

        lookup_cls_tvb_names :: PrM [Name]
        lookup_cls_tvb_names :: PrM [Name]
    lookup_cls_tvb_names = do
          let mk_tvb_names :: MaybeT PrM [Name]
    mk_tvb_names = PrM (Maybe DInfo) -> MaybeT PrM [Name]
    extract_tvb_names (Name -> PrM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReifyTypeNameInfo Name
    pClsName)
                         MaybeT PrM [Name] -> MaybeT PrM [Name] -> MaybeT PrM [Name]
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
    <|> PrM (Maybe DInfo) -> MaybeT PrM [Name]
    extract_tvb_names (Name -> PrM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReifyTypeNameInfo Name
    cls_name)
                          -- See Note [Using dsReifyTypeNameInfo when promoting instances]
          Maybe [Name]
    mb_tvb_names <- MaybeT PrM [Name] -> PrM (Maybe [Name])
    forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
    runMaybeT MaybeT PrM [Name]
    mk_tvb_names
          case Maybe [Name]
    mb_tvb_names of
            Just tvb_names :: [Name]
    tvb_names -> [Name] -> PrM [Name]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Name]
    tvb_names
            Nothing -> String -> PrM [Name]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> PrM [Name]) -> String -> PrM [Name]
    forall a b. (a -> b) -> a -> b
    $ "Cannot find class declaration annotation for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    forall a. Show a => a -> String
    show Name
    cls_name

        extract_tvb_names :: PrM (Maybe DInfo) -> MaybeT PrM [Name]
        extract_tvb_names :: PrM (Maybe DInfo) -> MaybeT PrM [Name]
    extract_tvb_names reify_info :: PrM (Maybe DInfo)
    reify_info = do
          Maybe DInfo
    mb_info <- PrM (Maybe DInfo) -> MaybeT PrM (Maybe DInfo)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift PrM (Maybe DInfo)
    reify_info
          case Maybe DInfo
    mb_info of
            Just (DTyConI (DClassD _ _ tvbs :: [DTyVarBndr]
    tvbs _ _) _)
              -> [Name] -> MaybeT PrM [Name]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Name] -> MaybeT PrM [Name]) -> [Name] -> MaybeT PrM [Name]
    forall a b. (a -> b) -> a -> b
    $ (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    tvbs
            _ -> MaybeT PrM [Name]
    forall (f :: * -> *) a. Alternative f => f a
    empty

    {-
    Note [Using dsReifyTypeNameInfo when promoting instances]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    During the promotion of a class instance, it becomes necessary to reify the
    original promoted class's info to learn various things. It's tempting to think
    that just calling dsReify on the class name will be sufficient, but it's not.
    Consider this class and its promotion:

      class Eq a where
        (==) :: a -> a -> Bool

      class PEq a where
        type (==) (x :: a) (y :: a) :: Bool

    Notice how both of these classes have an identifier named (==), one at the
    value level, and one at the type level. Now imagine what happens when you
    attempt to promote this Template Haskell declaration:

       [d| f :: Bool
           f = () == () |]

    When promoting ==, singletons will come up with its promoted equivalent (which also
    happens to be ==). However, this promoted name is a raw Name, since it is created
    with mkName. This becomes an issue when we call dsReify the raw "==" Name, as
    Template Haskell has to arbitrarily choose between reifying the info for the
    value-level (==) and the type-level (==), and in this case, it happens to pick the
    value-level (==) info. We want the type-level (==) info, however, because we care
    about the promoted version of (==).

    Fortunately, there's a serviceable workaround. Instead of dsReify, we can use
    dsReifyTypeNameInfo, which first calls lookupTypeName (to ensure we can find a Name
    that's in the type namespace) and _then_ reifies it.
    -}

    promoteMethod :: OMap Name DType -- InstanceSigs for methods
                  -> Maybe (Map Name DKind)
                        -- ^ instantiations for class tyvars (Nothing for default decls)
                        --   See Note [Promoted class method kinds]
                  -> OMap Name DType    -- method types
                  -> (Name, ULetDecRHS)
                  -> PrM (DDec, ALetDecRHS, DType)
                     -- returns (type instance, ALetDecRHS, promoted RHS)
    promoteMethod :: OMap Name DType
    -> Maybe (Map Name DType)
    -> OMap Name DType
    -> (Name, LetDecRHS Unannotated)
    -> PrM (DDec, ALetDecRHS, DType)
    promoteMethod inst_sigs_map :: OMap Name DType
    inst_sigs_map m_subst :: Maybe (Map Name DType)
    m_subst orig_sigs_map :: OMap Name DType
    orig_sigs_map (meth_name :: Name
    meth_name, meth_rhs :: LetDecRHS Unannotated
    meth_rhs) = do
      (meth_arg_kis :: DCxt
    meth_arg_kis, meth_res_ki :: DType
    meth_res_ki) <- PrM (DCxt, DType)
    lookup_meth_ty
      [Name]
    meth_arg_tvs <- (DType -> PrM Name) -> DCxt -> PrM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (PrM Name -> DType -> PrM Name
    forall a b. a -> b -> a
    const (PrM Name -> DType -> PrM Name) -> PrM Name -> DType -> PrM Name
    forall a b. (a -> b) -> a -> b
    $ String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "a") DCxt
    meth_arg_kis
      let helperNameBase :: String
    helperNameBase = case Name -> String
    nameBase Name
    proName of
                             first :: Char
    first:_ | Bool -> Bool
    not (Char -> Bool
    isHsLetter Char
    first) -> "TFHelper"
                             alpha :: String
    alpha                            -> String
    alpha

          -- family_args are the type variables in a promoted class's
          -- associated type family instance (or default implementation), e.g.,
          --
          --   class C k where
          --     type T (a :: k) (b :: Bool)
          --     type T a b = THelper1 a b        -- family_args = [a, b]
          --
          --   instance C Bool where
          --     type T a b = THelper2 a b        -- family_args = [a, b]
          --
          -- We could annotate these variables with explicit kinds, but it's not
          -- strictly necessary, as kind inference can figure them out just as well.
          family_args :: DCxt
    family_args = (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    meth_arg_tvs
      Name
    helperName <- String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    newUniqueName String
    helperNameBase
      let proHelperName :: Name
    proHelperName = Name -> Name
    promoteValNameLhs Name
    helperName
      ((_, _, _, eqns :: [DTySynEqn]
    eqns), _defuns :: [DDec]
    _defuns, ann_rhs :: ALetDecRHS
    ann_rhs)
        <- Maybe (DCxt, DType)
    -> OMap Name DType
    -> OMap Name Fixity
    -> (String, String)
    -> Name
    -> LetDecRHS Unannotated
    -> PrM
         ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
          ALetDecRHS)
    promoteLetDecRHS ((DCxt, DType) -> Maybe (DCxt, DType)
    forall a. a -> Maybe a
    Just (DCxt
    meth_arg_kis, DType
    meth_res_ki)) OMap Name DType
    forall k v. OMap k v
    OMap.empty OMap Name Fixity
    forall k v. OMap k v
    OMap.empty
                            (String, String)
    noPrefix Name
    helperName LetDecRHS Unannotated
    meth_rhs
      let tvbs :: [DTyVarBndr]
    tvbs = (Name -> DType -> DTyVarBndr) -> [Name] -> DCxt -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> DType -> DTyVarBndr
    DKindedTV [Name]
    meth_arg_tvs DCxt
    meth_arg_kis
      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DTypeFamilyHead -> [DTySynEqn] -> DDec
    DClosedTypeFamilyD (Name
    -> [DTyVarBndr]
    -> DFamilyResultSig
    -> Maybe InjectivityAnn
    -> DTypeFamilyHead
    DTypeFamilyHead
                                      Name
    proHelperName
                                      [DTyVarBndr]
    tvbs
                                      (DType -> DFamilyResultSig
    DKindSig DType
    meth_res_ki)
                                      Maybe InjectivityAnn
    forall a. Maybe a
    Nothing)
                                   [DTySynEqn]
    eqns]
      PrM [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => m [DDec] -> m ()
    emitDecsM (Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunctionalize Name
    proHelperName Maybe Fixity
    forall a. Maybe a
    Nothing [DTyVarBndr]
    tvbs (DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    meth_res_ki))
      (DDec, ALetDecRHS, DType) -> PrM (DDec, ALetDecRHS, DType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( DTySynEqn -> DDec
    DTySynInstD
                 (Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                            (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    proName) DCxt
    family_args)
                            (DType -> DCxt -> DType
    foldApply (Name -> DType
    promoteValRhs Name
    helperName) ((Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    meth_arg_tvs)))
             , ALetDecRHS
    ann_rhs
             , Name -> DType
    DConT (Name -> Int -> Name
    promoteTySym Name
    helperName 0) )
      where
        proName :: Name
    proName = Name -> Name
    promoteValNameLhs Name
    meth_name

        lookup_meth_ty :: PrM ([DKind], DKind)
        lookup_meth_ty :: PrM (DCxt, DType)
    lookup_meth_ty =
          case Name -> OMap Name DType -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    meth_name OMap Name DType
    inst_sigs_map of
            Just ty :: DType
    ty ->
              -- We have an InstanceSig. These are easy: no substitution for clas
              -- variables is required at all!
              DType -> PrM (DCxt, DType)
    forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
    promoteUnraveled DType
    ty
            Nothing -> do
              -- We don't have an InstanceSig, so we must compute the kind to use
              -- ourselves (possibly substituting for class variables below).
              (arg_kis :: DCxt
    arg_kis, res_ki :: DType
    res_ki) <-
                case Name -> OMap Name DType -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    meth_name OMap Name DType
    orig_sigs_map of
                  Nothing -> do
                    Maybe DInfo
    mb_info <- Name -> PrM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReifyTypeNameInfo Name
    proName
                               -- See Note [Using dsReifyTypeNameInfo when promoting instances]
                    case Maybe DInfo
    mb_info of
                      Just (DTyConI (DOpenTypeFamilyD (DTypeFamilyHead _ tvbs :: [DTyVarBndr]
    tvbs mb_res_ki :: DFamilyResultSig
    mb_res_ki _)) _)
                        -> let arg_kis :: DCxt
    arg_kis = (DTyVarBndr -> DType) -> [DTyVarBndr] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe DType -> DType
    default_to_star (Maybe DType -> DType)
    -> (DTyVarBndr -> Maybe DType) -> DTyVarBndr -> DType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DTyVarBndr -> Maybe DType
    extractTvbKind) [DTyVarBndr]
    tvbs
                               res_ki :: DType
    res_ki  = Maybe DType -> DType
    default_to_star (DFamilyResultSig -> Maybe DType
    resultSigToMaybeKind DFamilyResultSig
    mb_res_ki)
                            in (DCxt, DType) -> PrM (DCxt, DType)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DCxt
    arg_kis, DType
    res_ki)
                      _ -> String -> PrM (DCxt, DType)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> PrM (DCxt, DType)) -> String -> PrM (DCxt, DType)
    forall a b. (a -> b) -> a -> b
    $ "Cannot find type annotation for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    forall a. Show a => a -> String
    show Name
    proName
                  Just ty :: DType
    ty -> DType -> PrM (DCxt, DType)
    forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
    promoteUnraveled DType
    ty
              let -- If we're dealing with an associated type family instance, substitute
                  -- in the kind of the instance for better kind information in the RHS
                  -- helper function. If we're dealing with a default family implementation
                  -- (m_subst = Nothing), there's no need for a substitution.
                  -- See Note [Promoted class method kinds]
                  do_subst :: DType -> DType
    do_subst      = (DType -> DType)
    -> (Map Name DType -> DType -> DType)
    -> Maybe (Map Name DType)
    -> DType
    -> DType
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe DType -> DType
    forall a. a -> a
    id Map Name DType -> DType -> DType
    substKind Maybe (Map Name DType)
    m_subst
                  meth_arg_kis' :: DCxt
    meth_arg_kis' = (DType -> DType) -> DCxt -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map DType -> DType
    do_subst DCxt
    arg_kis
                  meth_res_ki' :: DType
    meth_res_ki'  = DType -> DType
    do_subst DType
    res_ki
              (DCxt, DType) -> PrM (DCxt, DType)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DCxt
    meth_arg_kis', DType
    meth_res_ki')

        default_to_star :: Maybe DType -> DType
    default_to_star Nothing  = Name -> DType
    DConT Name
    typeKindName
        default_to_star (Just k :: DType
    k) = DType
    k

    {-
    Note [Promoted class method kinds]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Consider this example of a type class (and instance):

      class C a where
        m :: a -> Bool -> Bool
        m _ x = x

      instance C [a] where
        m l _ = null l

    The promoted version of these declarations would be:

      class PC a where
        type M (x :: a) (y :: Bool) (z :: Bool)
        type M x y z = MHelper1 x y z

      instance PC [a] where
        type M x y z = MHelper2 x y z

      type family MHelper1 (x :: a)   (y :: Bool) (z :: Bool) where ...
      type family MHelper2 (x :: [a]) (y :: Bool) (z :: Bool) where ...

    Getting the kind signature for MHelper1 (the promoted default implementation of
    M) is quite simple, as it corresponds exactly to the kind of M. We might even
    choose to make that the kind of MHelper2, but then it would be overly general
    (and more difficult to find in -ddump-splices output). For this reason, we
    substitute in the kinds of the instance itself to determine the kinds of
    promoted method implementations like MHelper2.
    -}

    promoteLetDecEnv :: (String, String) -> ULetDecEnv -> PrM ([DDec], ALetDecEnv)
    promoteLetDecEnv :: (String, String)
    -> LetDecEnv Unannotated -> PrM ([DDec], ALetDecEnv)
    promoteLetDecEnv prefixes :: (String, String)
    prefixes (LetDecEnv { lde_defns :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> OMap Name (LetDecRHS ann)
    lde_defns = OMap Name (LetDecRHS Unannotated)
    value_env
                                         , lde_types :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
    lde_types = OMap Name DType
    type_env
                                         , lde_infix :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name Fixity
    lde_infix = OMap Name Fixity
    fix_env }) = do
      let infix_decls :: [DDec]
    infix_decls = [Maybe DDec] -> [DDec]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe DDec] -> [DDec]) -> [Maybe DDec] -> [DDec]
    forall a b. (a -> b) -> a -> b
    $ ((Name, Fixity) -> Maybe DDec) -> [(Name, Fixity)] -> [Maybe DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Name -> Fixity -> Maybe DDec) -> (Name, Fixity) -> Maybe DDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Fixity -> Maybe DDec
    promoteInfixDecl)
                                  ([(Name, Fixity)] -> [Maybe DDec])
    -> [(Name, Fixity)] -> [Maybe DDec]
    forall a b. (a -> b) -> a -> b
    $ OMap Name Fixity -> [(Name, Fixity)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name Fixity
    fix_env

        -- promote all the declarations, producing annotated declarations
      let (names :: [Name]
    names, rhss :: [LetDecRHS Unannotated]
    rhss) = [(Name, LetDecRHS Unannotated)]
    -> ([Name], [LetDecRHS Unannotated])
    forall a b. [(a, b)] -> ([a], [b])
    unzip ([(Name, LetDecRHS Unannotated)]
     -> ([Name], [LetDecRHS Unannotated]))
    -> [(Name, LetDecRHS Unannotated)]
    -> ([Name], [LetDecRHS Unannotated])
    forall a b. (a -> b) -> a -> b
    $ OMap Name (LetDecRHS Unannotated)
    -> [(Name, LetDecRHS Unannotated)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name (LetDecRHS Unannotated)
    value_env
      (payloads :: [(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])]
    payloads, defun_decss :: [[DDec]]
    defun_decss, ann_rhss :: [ALetDecRHS]
    ann_rhss)
        <- ([((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
       ALetDecRHS)]
     -> ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
         [ALetDecRHS]))
    -> PrM
         [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
           ALetDecRHS)]
    -> PrM
         ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
          [ALetDecRHS])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
      ALetDecRHS)]
    -> ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
        [ALetDecRHS])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 (PrM
       [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
         ALetDecRHS)]
     -> PrM
          ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
           [ALetDecRHS]))
    -> PrM
         [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
           ALetDecRHS)]
    -> PrM
         ([(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])], [[DDec]],
          [ALetDecRHS])
    forall a b. (a -> b) -> a -> b
    $ (Name
     -> LetDecRHS Unannotated
     -> PrM
          ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
           ALetDecRHS))
    -> [Name]
    -> [LetDecRHS Unannotated]
    -> PrM
         [((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
           ALetDecRHS)]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (Maybe (DCxt, DType)
    -> OMap Name DType
    -> OMap Name Fixity
    -> (String, String)
    -> Name
    -> LetDecRHS Unannotated
    -> PrM
         ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
          ALetDecRHS)
    promoteLetDecRHS Maybe (DCxt, DType)
    forall a. Maybe a
    Nothing OMap Name DType
    type_env OMap Name Fixity
    fix_env (String, String)
    prefixes) [Name]
    names [LetDecRHS Unannotated]
    rhss

      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs ([DDec] -> PrM ()) -> [DDec] -> PrM ()
    forall a b. (a -> b) -> a -> b
    $ [[DDec]] -> [DDec]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[DDec]]
    defun_decss
      OSet Name
    bound_kvs <- PrM (OSet Name)
    allBoundKindVars
      let decs :: [DDec]
    decs = ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]) -> DDec)
    -> [(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])] -> [DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, [DTyVarBndr], Maybe DType, [DTySynEqn]) -> DDec
    payload_to_dec [(Name, [DTyVarBndr], Maybe DType, [DTySynEqn])]
    payloads [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    infix_decls

        -- build the ALetDecEnv
      let let_dec_env' :: ALetDecEnv
    let_dec_env' = LetDecEnv :: forall (ann :: AnnotationFlag).
    OMap Name (LetDecRHS ann)
    -> OMap Name DType
    -> OMap Name Fixity
    -> IfAnn ann (OMap Name DType) ()
    -> IfAnn ann (OMap Name (OSet Name)) ()
    -> LetDecEnv ann
    LetDecEnv { lde_defns :: OMap Name ALetDecRHS
    lde_defns     = [(Name, ALetDecRHS)] -> OMap Name ALetDecRHS
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList ([(Name, ALetDecRHS)] -> OMap Name ALetDecRHS)
    -> [(Name, ALetDecRHS)] -> OMap Name ALetDecRHS
    forall a b. (a -> b) -> a -> b
    $ [Name] -> [ALetDecRHS] -> [(Name, ALetDecRHS)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    names [ALetDecRHS]
    ann_rhss
                                   , lde_types :: OMap Name DType
    lde_types     = OMap Name DType
    type_env
                                   , lde_infix :: OMap Name Fixity
    lde_infix     = OMap Name Fixity
    fix_env
                                   , lde_proms :: IfAnn Annotated (OMap Name DType) ()
    lde_proms     = IfAnn Annotated (OMap Name DType) ()
    forall k v. OMap k v
    OMap.empty  -- filled in promoteLetDecs
                                   , lde_bound_kvs :: IfAnn Annotated (OMap Name (OSet Name)) ()
    lde_bound_kvs = [(Name, OSet Name)] -> IfAnn Annotated (OMap Name (OSet Name)) ()
    forall k v. Ord k => [(k, v)] -> OMap k v
    OMap.fromList ([(Name, OSet Name)] -> IfAnn Annotated (OMap Name (OSet Name)) ())
    -> [(Name, OSet Name)]
    -> IfAnn Annotated (OMap Name (OSet Name)) ()
    forall a b. (a -> b) -> a -> b
    $ (Name -> (Name, OSet Name)) -> [Name] -> [(Name, OSet Name)]
    forall a b. (a -> b) -> [a] -> [b]
    map (, OSet Name
    bound_kvs) [Name]
    names }

      ([DDec], ALetDecEnv) -> PrM ([DDec], ALetDecEnv)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec]
    decs, ALetDecEnv
    let_dec_env')
      where
        payload_to_dec :: (Name, [DTyVarBndr], Maybe DType, [DTySynEqn]) -> DDec
    payload_to_dec (name :: Name
    name, tvbs :: [DTyVarBndr]
    tvbs, m_ki :: Maybe DType
    m_ki, eqns :: [DTySynEqn]
    eqns) = DTypeFamilyHead -> [DTySynEqn] -> DDec
    DClosedTypeFamilyD
                                                    (Name
    -> [DTyVarBndr]
    -> DFamilyResultSig
    -> Maybe InjectivityAnn
    -> DTypeFamilyHead
    DTypeFamilyHead Name
    name [DTyVarBndr]
    tvbs DFamilyResultSig
    sig Maybe InjectivityAnn
    forall a. Maybe a
    Nothing)
                                                    [DTySynEqn]
    eqns
          where
            sig :: DFamilyResultSig
    sig = DFamilyResultSig
    -> (DType -> DFamilyResultSig) -> Maybe DType -> DFamilyResultSig
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe DFamilyResultSig
    DNoSig DType -> DFamilyResultSig
    DKindSig Maybe DType
    m_ki

    promoteInfixDecl :: Name -> Fixity -> Maybe DDec
    promoteInfixDecl :: Name -> Fixity -> Maybe DDec
    promoteInfixDecl name :: Name
    name fixity :: Fixity
    fixity
     | Name -> String
    nameBase Name
    name String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> String
    nameBase Name
    promoted_name
       -- If a name and its promoted counterpart are the same (modulo module
       -- prefixes), then there's no need to promote a fixity declaration for
       -- that name, since the existing fixity declaration will cover both
       -- the term- and type-level versions of that name. Names that fall into this
       -- category include data constructor names and infix names.
     = Maybe DDec
    forall a. Maybe a
    Nothing
     | Bool
    otherwise
     = DDec -> Maybe DDec
    forall a. a -> Maybe a
    Just (DDec -> Maybe DDec) -> DDec -> Maybe DDec
    forall a b. (a -> b) -> a -> b
    $ DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Fixity -> Name -> DLetDec
    DInfixD Fixity
    fixity Name
    promoted_name
     where
      promoted_name :: Name
    promoted_name = Name -> Name
    promoteValNameLhs Name
    name

    -- This function is used both to promote class method defaults and normal
    -- let bindings. Thus, it can't quite do all the work locally and returns
    -- an intermediate structure. Perhaps a better design is available.
    promoteLetDecRHS :: Maybe ([DKind], DKind)  -- the promoted type of the RHS (if known)
                                                -- needed to fix #136
                     -> OMap Name DType      -- local type env't
                     -> OMap Name Fixity     -- local fixity env't
                     -> (String, String)     -- let-binding prefixes
                     -> Name                 -- name of the thing being promoted
                     -> ULetDecRHS           -- body of the thing
                     -> PrM ( (Name, [DTyVarBndr], Maybe DKind, [DTySynEqn]) -- "type family"
                            , [DDec]        -- defunctionalization
                            , ALetDecRHS )  -- annotated RHS
    promoteLetDecRHS :: Maybe (DCxt, DType)
    -> OMap Name DType
    -> OMap Name Fixity
    -> (String, String)
    -> Name
    -> LetDecRHS Unannotated
    -> PrM
         ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
          ALetDecRHS)
    promoteLetDecRHS m_rhs_ki :: Maybe (DCxt, DType)
    m_rhs_ki type_env :: OMap Name DType
    type_env fix_env :: OMap Name Fixity
    fix_env prefixes :: (String, String)
    prefixes name :: Name
    name (UValue exp) = do
      (res_kind :: Maybe DType
    res_kind, num_arrows :: Int
    num_arrows)
        <- case Maybe (DCxt, DType)
    m_rhs_ki of
             Just (arg_kis :: DCxt
    arg_kis, res_ki :: DType
    res_ki) -> (Maybe DType, Int) -> PrM (Maybe DType, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( DType -> Maybe DType
    forall a. a -> Maybe a
    Just (DCxt -> DType
    ravelTyFun (DCxt
    arg_kis DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ [DType
    res_ki]))
                                              , DCxt -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length DCxt
    arg_kis )
             _ |  Just ty :: DType
    ty <- Name -> OMap Name DType -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name DType
    type_env
               -> do DType
    ki <- DType -> PrM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    ty
                     (Maybe DType, Int) -> PrM (Maybe DType, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    ki, DType -> Int
    countArgs DType
    ty)
               |  Bool
    otherwise
               -> (Maybe DType, Int) -> PrM (Maybe DType, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe DType
    forall a. Maybe a
    Nothing, 0)
      case Int
    num_arrows of
        0 -> do
          [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals
          let lde_kvs_to_bind :: OSet Name
    lde_kvs_to_bind = (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 Maybe DType
    res_kind
          (exp' :: DType
    exp', ann_exp :: ADExp
    ann_exp) <- OSet Name -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. OSet Name -> PrM a -> PrM a
    forallBind OSet Name
    lde_kvs_to_bind (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $ DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
          let proName :: Name
    proName = (String, String) -> Name -> Name
    promoteValNameLhsPrefix (String, String)
    prefixes Name
    name
              m_fixity :: Maybe Fixity
    m_fixity = Name -> OMap Name Fixity -> Maybe Fixity
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name Fixity
    fix_env
              tvbs :: [DTyVarBndr]
    tvbs = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    all_locals
          [DDec]
    defuns <- Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunctionalize Name
    proName Maybe Fixity
    m_fixity [DTyVarBndr]
    tvbs Maybe DType
    res_kind
          ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
     ALetDecRHS)
    -> PrM
         ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
          ALetDecRHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( ( Name
    proName, [DTyVarBndr]
    tvbs, Maybe DType
    res_kind
                   , [Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    proName) (DCxt -> DType) -> DCxt -> DType
    forall a b. (a -> b) -> a -> b
    $ (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals) DType
    exp'] )
                 , [DDec]
    defuns
                 , DType -> Int -> ADExp -> ALetDecRHS
    AValue (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    proName) ((Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals))
                          Int
    num_arrows ADExp
    ann_exp )
        _ -> do
          [Name]
    names <- Int -> PrM Name -> PrM [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    num_arrows (String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    newUniqueName "a")
          let pats :: [DPat]
    pats    = (Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    names
              newArgs :: [DExp]
    newArgs = (Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    names
          Maybe (DCxt, DType)
    -> OMap Name DType
    -> OMap Name Fixity
    -> (String, String)
    -> Name
    -> LetDecRHS Unannotated
    -> PrM
         ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
          ALetDecRHS)
    promoteLetDecRHS Maybe (DCxt, DType)
    m_rhs_ki OMap Name DType
    type_env OMap Name Fixity
    fix_env (String, String)
    prefixes Name
    name
                           ([DClause] -> LetDecRHS Unannotated
    UFunction [[DPat] -> DExp -> DClause
    DClause [DPat]
    pats (DExp -> [DExp] -> DExp
    foldExp DExp
    exp [DExp]
    newArgs)])

    promoteLetDecRHS m_rhs_ki :: Maybe (DCxt, DType)
    m_rhs_ki type_env :: OMap Name DType
    type_env fix_env :: OMap Name Fixity
    fix_env prefixes :: (String, String)
    prefixes name :: Name
    name (UFunction clauses) = do
      Int
    numArgs <- [DClause] -> PrM Int
    forall (m :: * -> *). MonadFail m => [DClause] -> m Int
    count_args [DClause]
    clauses
      (m_argKs :: [Maybe DType]
    m_argKs, m_resK :: Maybe DType
    m_resK, ty_num_args :: Int
    ty_num_args) <- case Maybe (DCxt, DType)
    m_rhs_ki of
        Just (arg_kis :: DCxt
    arg_kis, res_ki :: DType
    res_ki) -> ([Maybe DType], Maybe DType, Int)
    -> PrM ([Maybe DType], Maybe DType, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((DType -> Maybe DType) -> DCxt -> [Maybe DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DType -> Maybe DType
    forall a. a -> Maybe a
    Just DCxt
    arg_kis, DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    res_ki, DCxt -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length DCxt
    arg_kis)
        _ |  Just ty :: DType
    ty <- Name -> OMap Name DType -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name DType
    type_env
          -> do
          -- promoteType turns arrows into TyFun. So, we unravel first to
          -- avoid this behavior. Note the use of ravelTyFun in resultK
          -- to make the return kind work out
          (argKs :: DCxt
    argKs, resultK :: DType
    resultK) <- DType -> PrM (DCxt, DType)
    forall (m :: * -> *). MonadFail m => DType -> m (DCxt, DType)
    promoteUnraveled DType
    ty
          -- invariant: countArgs ty == length argKs
          ([Maybe DType], Maybe DType, Int)
    -> PrM ([Maybe DType], Maybe DType, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((DType -> Maybe DType) -> DCxt -> [Maybe DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DType -> Maybe DType
    forall a. a -> Maybe a
    Just DCxt
    argKs, DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    resultK, DCxt -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length DCxt
    argKs)

          |  Bool
    otherwise
          -> ([Maybe DType], Maybe DType, Int)
    -> PrM ([Maybe DType], Maybe DType, Int)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> Maybe DType -> [Maybe DType]
    forall a. Int -> a -> [a]
    replicate Int
    numArgs Maybe DType
    forall a. Maybe a
    Nothing, Maybe DType
    forall a. Maybe a
    Nothing, Int
    numArgs)
      let proName :: Name
    proName  = (String, String) -> Name -> Name
    promoteValNameLhsPrefix (String, String)
    prefixes Name
    name
          m_fixity :: Maybe Fixity
    m_fixity = Name -> OMap Name Fixity -> Maybe Fixity
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name Fixity
    fix_env
      [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals
      let local_tvbs :: [DTyVarBndr]
    local_tvbs = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    all_locals
      [Name]
    tyvarNames <- (Maybe DType -> PrM Name) -> [Maybe DType] -> PrM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (PrM Name -> Maybe DType -> PrM Name
    forall a b. a -> b -> a
    const (PrM Name -> Maybe DType -> PrM Name)
    -> PrM Name -> Maybe DType -> PrM Name
    forall a b. (a -> b) -> a -> b
    $ String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "a") [Maybe DType]
    m_argKs
      let args :: [DTyVarBndr]
    args     = (Name -> Maybe DType -> DTyVarBndr)
    -> [Name] -> [Maybe DType] -> [DTyVarBndr]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> Maybe DType -> DTyVarBndr
    inferMaybeKindTV [Name]
    tyvarNames [Maybe DType]
    m_argKs
          all_args :: [DTyVarBndr]
    all_args = [DTyVarBndr]
    local_tvbs [DTyVarBndr] -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. [a] -> [a] -> [a]
    ++ [DTyVarBndr]
    args
      [DDec]
    defun_decs <- Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunctionalize Name
    proName Maybe Fixity
    m_fixity [DTyVarBndr]
    all_args Maybe DType
    m_resK
      [DClause]
    expClauses <- (DClause -> PrM DClause) -> [DClause] -> PrM [DClause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Int -> Int -> DClause -> PrM DClause
    etaContractOrExpand Int
    ty_num_args Int
    numArgs) [DClause]
    clauses
      let lde_kvs_to_bind :: OSet Name
    lde_kvs_to_bind = (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) [Maybe DType]
    m_argKs OSet Name -> OSet Name -> OSet Name
    forall a. Semigroup a => a -> a -> a
    <> (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 Maybe DType
    m_resK
      (eqns :: [DTySynEqn]
    eqns, ann_clauses :: [ADClause]
    ann_clauses) <- OSet Name
    -> PrM ([DTySynEqn], [ADClause]) -> PrM ([DTySynEqn], [ADClause])
    forall a. OSet Name -> PrM a -> PrM a
    forallBind OSet Name
    lde_kvs_to_bind (PrM ([DTySynEqn], [ADClause]) -> PrM ([DTySynEqn], [ADClause]))
    -> PrM ([DTySynEqn], [ADClause]) -> PrM ([DTySynEqn], [ADClause])
    forall a b. (a -> b) -> a -> b
    $
                             (DClause -> PrM (DTySynEqn, ADClause))
    -> [DClause] -> PrM ([DTySynEqn], [ADClause])
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> m (b, c)) -> [a] -> m ([b], [c])
    mapAndUnzipM (Name -> DClause -> PrM (DTySynEqn, ADClause)
    promoteClause Name
    proName) [DClause]
    expClauses
      DType
    prom_fun <- Name -> PrM DType
    lookupVarE Name
    name
      ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
     ALetDecRHS)
    -> PrM
         ((Name, [DTyVarBndr], Maybe DType, [DTySynEqn]), [DDec],
          ALetDecRHS)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( (Name
    proName, [DTyVarBndr]
    all_args, Maybe DType
    m_resK, [DTySynEqn]
    eqns)
             , [DDec]
    defun_decs
             , DType -> Int -> [ADClause] -> ALetDecRHS
    AFunction DType
    prom_fun Int
    ty_num_args [ADClause]
    ann_clauses )

      where
        etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause
        etaContractOrExpand :: Int -> Int -> DClause -> PrM DClause
    etaContractOrExpand ty_num_args :: Int
    ty_num_args clause_num_args :: Int
    clause_num_args (DClause pats :: [DPat]
    pats exp :: DExp
    exp)
          | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0 = do -- Eta-expand
              [Name]
    names <- Int -> PrM Name -> PrM [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    n (String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    newUniqueName "a")
              let newPats :: [DPat]
    newPats = (Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DPat
    DVarP [Name]
    names
                  newArgs :: [DExp]
    newArgs = (Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    names
              DClause -> PrM DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> PrM DClause) -> DClause -> PrM DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause ([DPat]
    pats [DPat] -> [DPat] -> [DPat]
    forall a. [a] -> [a] -> [a]
    ++ [DPat]
    newPats) (DExp -> [DExp] -> DExp
    foldExp DExp
    exp [DExp]
    newArgs)
          | Bool
    otherwise = do -- Eta-contract
              let (clausePats :: [DPat]
    clausePats, lamPats :: [DPat]
    lamPats) = Int -> [DPat] -> ([DPat], [DPat])
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    ty_num_args [DPat]
    pats
              DExp
    lamExp <- [DPat] -> DExp -> PrM DExp
    forall (q :: * -> *). DsMonad q => [DPat] -> DExp -> q DExp
    mkDLamEFromDPats [DPat]
    lamPats DExp
    exp
              DClause -> PrM DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> PrM DClause) -> DClause -> PrM DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [DPat]
    clausePats DExp
    lamExp
          where
            n :: Int
    n = Int
    ty_num_args Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    clause_num_args

        count_args :: [DClause] -> m Int
    count_args (DClause pats :: [DPat]
    pats _ : _) = Int -> m Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Int -> m Int) -> Int -> m Int
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [DPat]
    pats
        count_args _ = String -> m Int
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> m Int) -> String -> m Int
    forall a b. (a -> b) -> a -> b
    $ "Impossible! A function without clauses."

    promoteClause :: Name -> DClause -> PrM (DTySynEqn, ADClause)
    promoteClause :: Name -> DClause -> PrM (DTySynEqn, ADClause)
    promoteClause proName :: Name
    proName (DClause pats :: [DPat]
    pats exp :: DExp
    exp) = do
      -- promoting the patterns creates variable bindings. These are passed
      -- to the function promoted the RHS
      ((types :: DCxt
    types, pats' :: [ADPat]
    pats'), prom_pat_infos :: PromDPatInfos
    prom_pat_infos) <- QWithAux PromDPatInfos PrM (DCxt, [ADPat])
    -> PrM ((DCxt, [ADPat]), PromDPatInfos)
    forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
    evalForPair (QWithAux PromDPatInfos PrM (DCxt, [ADPat])
     -> PrM ((DCxt, [ADPat]), PromDPatInfos))
    -> QWithAux PromDPatInfos PrM (DCxt, [ADPat])
    -> PrM ((DCxt, [ADPat]), PromDPatInfos)
    forall a b. (a -> b) -> a -> b
    $ (DPat -> QWithAux PromDPatInfos PrM (DType, ADPat))
    -> [DPat] -> QWithAux PromDPatInfos PrM (DCxt, [ADPat])
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> m (b, c)) -> [a] -> m ([b], [c])
    mapAndUnzipM DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat [DPat]
    pats
      let PromDPatInfos { prom_dpat_vars :: PromDPatInfos -> VarPromotions
    prom_dpat_vars    = VarPromotions
    new_vars
                        , prom_dpat_sig_kvs :: PromDPatInfos -> OSet Name
    prom_dpat_sig_kvs = OSet Name
    sig_kvs } = PromDPatInfos
    prom_pat_infos
      (ty :: DType
    ty, ann_exp :: ADExp
    ann_exp) <- OSet Name -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. OSet Name -> PrM a -> PrM a
    forallBind OSet Name
    sig_kvs (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $
                       VarPromotions -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. VarPromotions -> PrM a -> PrM a
    lambdaBind VarPromotions
    new_vars (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $
                       DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
      [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals   -- these are bound *outside* of this clause
      (DTySynEqn, ADClause) -> PrM (DTySynEqn, ADClause)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    proName) (DCxt -> DType) -> DCxt -> DType
    forall a b. (a -> b) -> a -> b
    $ (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ DCxt
    types) DType
    ty
             , VarPromotions -> [ADPat] -> ADExp -> ADClause
    ADClause VarPromotions
    new_vars [ADPat]
    pats' ADExp
    ann_exp )

    promoteMatch :: Name -> DMatch -> PrM (DTySynEqn, ADMatch)
    promoteMatch :: Name -> DMatch -> PrM (DTySynEqn, ADMatch)
    promoteMatch caseTFName :: Name
    caseTFName (DMatch pat :: DPat
    pat exp :: DExp
    exp) = do
      -- promoting the patterns creates variable bindings. These are passed
      -- to the function promoted the RHS
      ((ty :: DType
    ty, pat' :: ADPat
    pat'), prom_pat_infos :: PromDPatInfos
    prom_pat_infos) <- QWithAux PromDPatInfos PrM (DType, ADPat)
    -> PrM ((DType, ADPat), PromDPatInfos)
    forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
    evalForPair (QWithAux PromDPatInfos PrM (DType, ADPat)
     -> PrM ((DType, ADPat), PromDPatInfos))
    -> QWithAux PromDPatInfos PrM (DType, ADPat)
    -> PrM ((DType, ADPat), PromDPatInfos)
    forall a b. (a -> b) -> a -> b
    $ DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat DPat
    pat
      let PromDPatInfos { prom_dpat_vars :: PromDPatInfos -> VarPromotions
    prom_dpat_vars    = VarPromotions
    new_vars
                        , prom_dpat_sig_kvs :: PromDPatInfos -> OSet Name
    prom_dpat_sig_kvs = OSet Name
    sig_kvs } = PromDPatInfos
    prom_pat_infos
      (rhs :: DType
    rhs, ann_exp :: ADExp
    ann_exp) <- OSet Name -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. OSet Name -> PrM a -> PrM a
    forallBind OSet Name
    sig_kvs (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $
                        VarPromotions -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. VarPromotions -> PrM a -> PrM a
    lambdaBind VarPromotions
    new_vars (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $
                        DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
      [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals
      (DTySynEqn, ADMatch) -> PrM (DTySynEqn, ADMatch)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((DTySynEqn, ADMatch) -> PrM (DTySynEqn, ADMatch))
    -> (DTySynEqn, ADMatch) -> PrM (DTySynEqn, ADMatch)
    forall a b. (a -> b) -> a -> b
    $ ( Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                           (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    caseTFName) (DCxt -> DType) -> DCxt -> DType
    forall a b. (a -> b) -> a -> b
    $ (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals DCxt -> DCxt -> DCxt
    forall a. [a] -> [a] -> [a]
    ++ [DType
    ty])
                           DType
    rhs
               , VarPromotions -> ADPat -> ADExp -> ADMatch
    ADMatch VarPromotions
    new_vars ADPat
    pat' ADExp
    ann_exp)

    -- promotes a term pattern into a type pattern, accumulating bound variable names
    promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat (DLitP lit :: Lit
    lit) = (, Lit -> ADPat
    ADLitP Lit
    lit) (DType -> (DType, ADPat))
    -> QWithAux PromDPatInfos PrM DType
    -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lit -> QWithAux PromDPatInfos PrM DType
    forall (m :: * -> *). MonadFail m => Lit -> m DType
    promoteLitPat Lit
    lit
    promotePat (DVarP name :: Name
    name) = do
          -- term vars can be symbols... type vars can't!
      Name
    tyName <- Name -> QWithAux PromDPatInfos PrM Name
    forall (q :: * -> *). Quasi q => Name -> q Name
    mkTyName Name
    name
      PromDPatInfos -> QWithAux PromDPatInfos PrM ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (PromDPatInfos -> QWithAux PromDPatInfos PrM ())
    -> PromDPatInfos -> QWithAux PromDPatInfos PrM ()
    forall a b. (a -> b) -> a -> b
    $ VarPromotions -> OSet Name -> PromDPatInfos
    PromDPatInfos [(Name
    name, Name
    tyName)] OSet Name
    forall a. OSet a
    OSet.empty
      (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Name -> DType
    DVarT Name
    tyName, Name -> ADPat
    ADVarP Name
    name)
    promotePat (DConP name :: Name
    name pats :: [DPat]
    pats) = do
      (types :: DCxt
    types, pats' :: [ADPat]
    pats') <- (DPat -> QWithAux PromDPatInfos PrM (DType, ADPat))
    -> [DPat] -> QWithAux PromDPatInfos PrM (DCxt, [ADPat])
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> m (b, c)) -> [a] -> m ([b], [c])
    mapAndUnzipM DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat [DPat]
    pats
      let name' :: Name
    name' = Name -> Name
    unboxed_tuple_to_tuple Name
    name
      (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    name') DCxt
    types, Name -> [ADPat] -> ADPat
    ADConP Name
    name [ADPat]
    pats')
      where
        unboxed_tuple_to_tuple :: Name -> Name
    unboxed_tuple_to_tuple n :: Name
    n
          | Just deg :: Int
    deg <- Name -> Maybe Int
    unboxedTupleNameDegree_maybe Name
    n = Int -> Name
    tupleDataName Int
    deg
          | Bool
    otherwise                                  = Name
    n
    promotePat (DTildeP pat :: DPat
    pat) = do
      String -> QWithAux PromDPatInfos PrM ()
    forall (q :: * -> *). Quasi q => String -> q ()
    qReportWarning "Lazy pattern converted into regular pattern in promotion"
      (ADPat -> ADPat) -> (DType, ADPat) -> (DType, ADPat)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ADPat -> ADPat
    ADTildeP ((DType, ADPat) -> (DType, ADPat))
    -> QWithAux PromDPatInfos PrM (DType, ADPat)
    -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat DPat
    pat
    promotePat (DBangP pat :: DPat
    pat) = do
      String -> QWithAux PromDPatInfos PrM ()
    forall (q :: * -> *). Quasi q => String -> q ()
    qReportWarning "Strict pattern converted into regular pattern in promotion"
      (ADPat -> ADPat) -> (DType, ADPat) -> (DType, ADPat)
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second ADPat -> ADPat
    ADBangP ((DType, ADPat) -> (DType, ADPat))
    -> QWithAux PromDPatInfos PrM (DType, ADPat)
    -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat DPat
    pat
    promotePat (DSigP pat :: DPat
    pat ty :: DType
    ty) = do
      -- We must maintain the invariant that any promoted pattern signature must
      -- not have any wildcards in the underlying pattern.
      -- See Note [Singling pattern signatures].
      DPat
    wildless_pat <- DPat -> QWithAux PromDPatInfos PrM DPat
    forall (q :: * -> *). DsMonad q => DPat -> q DPat
    removeWilds DPat
    pat
      (promoted :: DType
    promoted, pat' :: ADPat
    pat') <- DPat -> QWithAux PromDPatInfos PrM (DType, ADPat)
    promotePat DPat
    wildless_pat
      DType
    ki <- DType -> QWithAux PromDPatInfos PrM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    ty
      PromDPatInfos -> QWithAux PromDPatInfos PrM ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell (PromDPatInfos -> QWithAux PromDPatInfos PrM ())
    -> PromDPatInfos -> QWithAux PromDPatInfos PrM ()
    forall a b. (a -> b) -> a -> b
    $ VarPromotions -> OSet Name -> PromDPatInfos
    PromDPatInfos [] (DType -> OSet Name
    fvDType DType
    ki)
      (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> DType -> DType
    DSigT DType
    promoted DType
    ki, DType -> ADPat -> DType -> ADPat
    ADSigP DType
    promoted ADPat
    pat' DType
    ki)
    promotePat DWildP = (DType, ADPat) -> QWithAux PromDPatInfos PrM (DType, ADPat)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType
    DWildCardT, ADPat
    ADWildP)

    promoteExp :: DExp -> PrM (DType, ADExp)
    promoteExp :: DExp -> PrM (DType, ADExp)
    promoteExp (DVarE name :: Name
    name) = (DType -> (DType, ADExp)) -> PrM DType -> PrM (DType, ADExp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (, Name -> ADExp
    ADVarE Name
    name) (PrM DType -> PrM (DType, ADExp))
    -> PrM DType -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $ Name -> PrM DType
    lookupVarE Name
    name
    promoteExp (DConE name :: Name
    name) = (DType, ADExp) -> PrM (DType, ADExp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((DType, ADExp) -> PrM (DType, ADExp))
    -> (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $ (Name -> DType
    promoteValRhs Name
    name, Name -> ADExp
    ADConE Name
    name)
    promoteExp (DLitE lit :: Lit
    lit)  = (DType -> (DType, ADExp)) -> PrM DType -> PrM (DType, ADExp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (, Lit -> ADExp
    ADLitE Lit
    lit) (PrM DType -> PrM (DType, ADExp))
    -> PrM DType -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $ Lit -> PrM DType
    forall (q :: * -> *). Quasi q => Lit -> q DType
    promoteLitExp Lit
    lit
    promoteExp (DAppE exp1 :: DExp
    exp1 exp2 :: DExp
    exp2) = do
      (exp1' :: DType
    exp1', ann_exp1 :: ADExp
    ann_exp1) <- DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp1
      (exp2' :: DType
    exp2', ann_exp2 :: ADExp
    ann_exp2) <- DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp2
      (DType, ADExp) -> PrM (DType, ADExp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> DType -> DType
    apply DType
    exp1' DType
    exp2', ADExp -> ADExp -> ADExp
    ADAppE ADExp
    ann_exp1 ADExp
    ann_exp2)
    -- Until we get visible kind applications, this is the best we can do.
    promoteExp (DAppTypeE exp :: DExp
    exp _) = do
      String -> PrM ()
    forall (q :: * -> *). Quasi q => String -> q ()
    qReportWarning "Visible type applications are ignored by `singletons`."
      DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
    promoteExp (DLamE names :: [Name]
    names exp :: DExp
    exp) = do
      Name
    lambdaName <- String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    newUniqueName "Lambda"
      [Name]
    tyNames <- (Name -> PrM Name) -> [Name] -> PrM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM Name -> PrM Name
    forall (q :: * -> *). Quasi q => Name -> q Name
    mkTyName [Name]
    names
      let var_proms :: VarPromotions
    var_proms = [Name] -> [Name] -> VarPromotions
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    names [Name]
    tyNames
      (rhs :: DType
    rhs, ann_exp :: ADExp
    ann_exp) <- VarPromotions -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. VarPromotions -> PrM a -> PrM a
    lambdaBind VarPromotions
    var_proms (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $ DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
      [Name]
    tyFamLamTypes <- (Name -> PrM Name) -> [Name] -> PrM [Name]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (PrM Name -> Name -> PrM Name
    forall a b. a -> b -> a
    const (PrM Name -> Name -> PrM Name) -> PrM Name -> Name -> PrM Name
    forall a b. (a -> b) -> a -> b
    $ String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "t") [Name]
    names
      [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals
      let all_args :: [Name]
    all_args = [Name]
    all_locals [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name]
    tyFamLamTypes
          tvbs :: [DTyVarBndr]
    tvbs     = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    all_args
      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DTypeFamilyHead -> [DTySynEqn] -> DDec
    DClosedTypeFamilyD (Name
    -> [DTyVarBndr]
    -> DFamilyResultSig
    -> Maybe InjectivityAnn
    -> DTypeFamilyHead
    DTypeFamilyHead
                                     Name
    lambdaName
                                     [DTyVarBndr]
    tvbs
                                     DFamilyResultSig
    DNoSig
                                     Maybe InjectivityAnn
    forall a. Maybe a
    Nothing)
                                   [Maybe [DTyVarBndr] -> DType -> DType -> DTySynEqn
    DTySynEqn Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                                              (DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    lambdaName) (DCxt -> DType) -> DCxt -> DType
    forall a b. (a -> b) -> a -> b
    $
                                               (Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT ([Name]
    all_locals [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name]
    tyNames))
                                              DType
    rhs]]
      PrM [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => m [DDec] -> m ()
    emitDecsM (PrM [DDec] -> PrM ()) -> PrM [DDec] -> PrM ()
    forall a b. (a -> b) -> a -> b
    $ Name -> Maybe Fixity -> [DTyVarBndr] -> Maybe DType -> PrM [DDec]
    defunctionalize Name
    lambdaName Maybe Fixity
    forall a. Maybe a
    Nothing [DTyVarBndr]
    tvbs Maybe DType
    forall a. Maybe a
    Nothing
      let promLambda :: DType
    promLambda = (DType -> DType -> DType) -> DType -> DCxt -> DType
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl DType -> DType -> DType
    apply (Name -> DType
    DConT (Name -> Int -> Name
    promoteTySym Name
    lambdaName 0))
                                   ((Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals)
      (DType, ADExp) -> PrM (DType, ADExp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType
    promLambda, [Name] -> DType -> [Name] -> ADExp -> ADExp
    ADLamE [Name]
    tyNames DType
    promLambda [Name]
    names ADExp
    ann_exp)
    promoteExp (DCaseE exp :: DExp
    exp matches :: [DMatch]
    matches) = do
      Name
    caseTFName <- String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    newUniqueName "Case"
      [Name]
    all_locals <- PrM [Name]
    forall (m :: * -> *). MonadReader PrEnv m => m [Name]
    allLocals
      let prom_case :: DType
    prom_case = DType -> DCxt -> DType
    foldType (Name -> DType
    DConT Name
    caseTFName) ((Name -> DType) -> [Name] -> DCxt
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    all_locals)
      (exp' :: DType
    exp', ann_exp :: ADExp
    ann_exp)     <- DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
      (eqns :: [DTySynEqn]
    eqns, ann_matches :: [ADMatch]
    ann_matches) <- (DMatch -> PrM (DTySynEqn, ADMatch))
    -> [DMatch] -> PrM ([DTySynEqn], [ADMatch])
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> m (b, c)) -> [a] -> m ([b], [c])
    mapAndUnzipM (Name -> DMatch -> PrM (DTySynEqn, ADMatch)
    promoteMatch Name
    caseTFName) [DMatch]
    matches
      Name
    tyvarName  <- String -> PrM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "t"
      let all_args :: [Name]
    all_args = [Name]
    all_locals [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name
    tyvarName]
          tvbs :: [DTyVarBndr]
    tvbs     = (Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    all_args
      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DTypeFamilyHead -> [DTySynEqn] -> DDec
    DClosedTypeFamilyD (Name
    -> [DTyVarBndr]
    -> DFamilyResultSig
    -> Maybe InjectivityAnn
    -> DTypeFamilyHead
    DTypeFamilyHead Name
    caseTFName [DTyVarBndr]
    tvbs DFamilyResultSig
    DNoSig Maybe InjectivityAnn
    forall a. Maybe a
    Nothing) [DTySynEqn]
    eqns]
        -- See Note [Annotate case return type] in Single
      let applied_case :: DType
    applied_case = DType
    prom_case DType -> DType -> DType
    `DAppT` DType
    exp'
      (DType, ADExp) -> PrM (DType, ADExp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( DType
    applied_case
             , ADExp -> [ADMatch] -> DType -> ADExp
    ADCaseE ADExp
    ann_exp [ADMatch]
    ann_matches DType
    applied_case )
    promoteExp (DLetE decs :: [DLetDec]
    decs exp :: DExp
    exp) = do
      Int
    unique <- PrM Int
    forall (q :: * -> *). DsMonad q => q Int
    qNewUnique
      let letPrefixes :: (String, String)
    letPrefixes = String -> String -> Int -> (String, String)
    uniquePrefixes "Let" "<<<" Int
    unique
      (binds :: [LetBind]
    binds, ann_env :: ALetDecEnv
    ann_env) <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
    promoteLetDecs (String, String)
    letPrefixes [DLetDec]
    decs
      (exp' :: DType
    exp', ann_exp :: ADExp
    ann_exp) <- [LetBind] -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a. [LetBind] -> PrM a -> PrM a
    letBind [LetBind]
    binds (PrM (DType, ADExp) -> PrM (DType, ADExp))
    -> PrM (DType, ADExp) -> PrM (DType, ADExp)
    forall a b. (a -> b) -> a -> b
    $ DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
      (DType, ADExp) -> PrM (DType, ADExp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType
    exp', ALetDecEnv -> ADExp -> ADExp
    ADLetE ALetDecEnv
    ann_env ADExp
    ann_exp)
    promoteExp (DSigE exp :: DExp
    exp ty :: DType
    ty) = do
      (exp' :: DType
    exp', ann_exp :: ADExp
    ann_exp) <- DExp -> PrM (DType, ADExp)
    promoteExp DExp
    exp
      DType
    ty' <- DType -> PrM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    ty
      (DType, ADExp) -> PrM (DType, ADExp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> DType -> DType
    DSigT DType
    exp' DType
    ty', DType -> ADExp -> DType -> ADExp
    ADSigE DType
    exp' ADExp
    ann_exp DType
    ty')
    promoteExp e :: DExp
    e@(DStaticE _) = String -> PrM (DType, ADExp)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Static expressions cannot be promoted: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ DExp -> String
    forall a. Show a => a -> String
    show DExp
    e)

    promoteLitExp :: Quasi q => Lit -> q DType
    promoteLitExp :: Lit -> q DType
    promoteLitExp (IntegerL n :: Integer
    n)
      | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0    = DType -> q DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> q DType) -> DType -> q DType
    forall a b. (a -> b) -> a -> b
    $ (Name -> DType
    DConT Name
    tyFromIntegerName DType -> DType -> DType
    `DAppT` TyLit -> DType
    DLitT (Integer -> TyLit
    NumTyLit Integer
    n))
      | Bool
    otherwise = DType -> q DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> q DType) -> DType -> q DType
    forall a b. (a -> b) -> a -> b
    $ (Name -> DType
    DConT Name
    tyNegateName DType -> DType -> DType
    `DAppT`
                              (Name -> DType
    DConT Name
    tyFromIntegerName DType -> DType -> DType
    `DAppT` TyLit -> DType
    DLitT (Integer -> TyLit
    NumTyLit (-Integer
    n))))
    promoteLitExp (StringL str :: String
    str) = do
      let prom_str_lit :: DType
    prom_str_lit = TyLit -> DType
    DLitT (String -> TyLit
    StrTyLit String
    str)
      Bool
    os_enabled <- Extension -> q Bool
    forall (m :: * -> *). Quasi m => Extension -> m Bool
    qIsExtEnabled Extension
    LangExt.OverloadedStrings
      DType -> q DType
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DType -> q DType) -> DType -> q DType
    forall a b. (a -> b) -> a -> b
    $ if Bool
    os_enabled
             then Name -> DType
    DConT Name
    tyFromStringName DType -> DType -> DType
    `DAppT` DType
    prom_str_lit
             else DType
    prom_str_lit
    promoteLitExp lit :: Lit
    lit =
      String -> q DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Only string and natural number literals can be promoted: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Lit -> String
    forall a. Show a => a -> String
    show Lit
    lit)

    promoteLitPat :: MonadFail m => Lit -> m DType
    promoteLitPat :: Lit -> m DType
    promoteLitPat (IntegerL n :: Integer
    n)
      | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0    = DType -> m DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> m DType) -> DType -> m DType
    forall a b. (a -> b) -> a -> b
    $ (TyLit -> DType
    DLitT (Integer -> TyLit
    NumTyLit Integer
    n))
      | Bool
    otherwise =
        String -> m DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> m DType) -> String -> m DType
    forall a b. (a -> b) -> a -> b
    $ "Negative literal patterns are not allowed,\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
               "because literal patterns are promoted to natural numbers."
    promoteLitPat (StringL str :: String
    str) = DType -> m DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> m DType) -> DType -> m DType
    forall a b. (a -> b) -> a -> b
    $ TyLit -> DType
    DLitT (String -> TyLit
    StrTyLit String
    str)
    promoteLitPat lit :: Lit
    lit =
      String -> m DType
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Only string and natural number literals can be promoted: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Lit -> String
    forall a. Show a => a -> String
    show Lit
    lit)

    -- See Note [DerivedDecl]
    promoteDerivedEqDec :: DerivedEqDecl -> PrM ()
    promoteDerivedEqDec :: DerivedEqDecl -> PrM ()
    promoteDerivedEqDec (DerivedDecl { ded_type :: forall (cls :: * -> Constraint). DerivedDecl cls -> DType
    ded_type = DType
    ty
                                     , ded_decl :: forall (cls :: * -> Constraint). DerivedDecl cls -> DataDecl
    ded_decl = DataDecl _ _ cons :: [DCon]
    cons }) = do
      DType
    kind <- DType -> PrM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    ty
      [DDec]
    inst_decs <- DType -> [DCon] -> PrM [DDec]
    forall (q :: * -> *). Quasi q => DType -> [DCon] -> q [DDec]
    mkEqTypeInstance DType
    kind [DCon]
    cons
      [DDec] -> PrM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs [DDec]
    inst_decs