    {- Data/Singletons/Single.hs

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

    This file contains functions to refine constructs to work with singleton
    types. It is an internal module to the singletons package.
    -}
    {-# LANGUAGE TemplateHaskell, TupleSections, ParallelListComp, CPP #-}

    module Data.Singletons.Single where

    import Prelude hiding ( exp )
    import Language.Haskell.TH hiding ( cxt )
    import Language.Haskell.TH.Syntax (NameSpace(..), Quasi(..))
    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.Util
    import Data.Singletons.Promote
    import Data.Singletons.Promote.Defun
    import Data.Singletons.Promote.Monad ( promoteM )
    import Data.Singletons.Promote.Type
    import Data.Singletons.Names
    import Data.Singletons.Single.Monad
    import Data.Singletons.Single.Type
    import Data.Singletons.Single.Data
    import Data.Singletons.Single.Defun
    import Data.Singletons.Single.Fixity
    import Data.Singletons.Single.Eq
    import Data.Singletons.Syntax
    import Data.Singletons.Partition
    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 qualified Data.Map.Strict as Map
    import Data.Map.Strict ( Map )
    import Data.Maybe
    import qualified Data.Set as Set
    import Control.Monad
    import Data.List
    import qualified GHC.LanguageExtensions.Type as LangExt

    {-
    How singletons works
    ~~~~~~~~~~~~~~~~~~~~

    Singling, on the surface, doesn't seem all that complicated. Promote the type,
    and singletonize all the terms. That's essentially what was done singletons < 1.0.
    But, now we want to deal with higher-order singletons. So, things are a little
    more complicated.

    The way to understand all of this is that *every* variable maps to something
    of type (Sing t), for an appropriately-kinded t. This includes functions, which
    use the "SLambda" instance of Sing. To apply singleton functions, we use the
    applySing function.

    That, in and of itself, wouldn't be too hard, but it's really annoying from
    the user standpoint. After dutifully singling `map`, a user doesn't want to
    have to use two `applySing`s to actually use it. So, any let-bound identifier
    is eta-expanded so that the singled type has the same number of arrows as
    the original type. (If there is no original type signature, then it has as
    many arrows as the original had patterns.) Then, we store a use of one of the
    singFunX functions in the SgM environment so that every use of a let-bound
    identifier has a proper type (Sing t).

    It would be consistent to avoid this eta-expansion for local lets (as opposed
    to top-level lets), but that seemed like more bother than it was worth. It
    may also be possible to be cleverer about nested eta-expansions and contractions,
    but that also seemed not to be worth it. Though I haven't tested it, my hope
    is that the eta-expansions and contractions have no runtime effect, especially
    because SLambda is a *newtype* instance, not a *data* instance.

    Note that to maintain the desired invariant, we must also be careful to eta-
    contract constructors. This is the point of buildDataLets.
    -}

    -- | Generate singleton definitions from a type that is already defined.
    -- For example, the singletons package itself uses
    --
    -- > $(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
    --
    -- to generate singletons for Prelude types.
    genSingletons :: DsMonad q => [Name] -> q [Dec]
    genSingletons :: [Name] -> q [Dec]
    genSingletons names :: [Name]
    names = do
      [Name] -> q ()
    forall (q :: * -> *). Quasi q => [Name] -> q ()
    checkForRep [Name]
    names
      [DDec]
    ddecs <- (Name -> q [DDec]) -> [Name] -> q [DDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM (DInfo -> q [DDec]
    forall (q :: * -> *). DsMonad q => DInfo -> q [DDec]
    singInfo (DInfo -> q [DDec]) -> (Name -> q DInfo) -> Name -> q [DDec]
    forall (m :: * -> *) b c a.
    Monad m =>
    (b -> m c) -> (a -> m b) -> a -> m c
    <=< 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
      [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

    -- | Make promoted and singleton versions of all declarations given, retaining
    -- the original declarations.
    -- See <https://github.com/goldfirere/singletons/blob/master/README.md> for
    -- further explanation.
    singletons :: DsMonad q => q [Dec] -> q [Dec]
    singletons :: q [Dec] -> q [Dec]
    singletons qdecs :: q [Dec]
    qdecs = do
      [Dec]
    decs <- q [Dec]
    qdecs
      [DDec]
    ddecs <- [Dec] -> DsM q [DDec] -> q [DDec]
    forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
    withLocalDeclarations [Dec]
    decs (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]
    decs
      [DDec]
    singDecs <- [Dec] -> [DDec] -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> [DDec] -> q [DDec]
    singTopLevelDecs [Dec]
    decs [DDec]
    ddecs
      [Dec] -> q [Dec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Dec]
    decs [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec] -> [Dec]
    decsToTH [DDec]
    singDecs)

    -- | Make promoted and singleton versions of all declarations given, discarding
    -- the original declarations. Note that a singleton based on a datatype needs
    -- the original datatype, so this will fail if it sees any datatype declarations.
    -- Classes, instances, and functions are all fine.
    singletonsOnly :: DsMonad q => q [Dec] -> q [Dec]
    singletonsOnly :: q [Dec] -> q [Dec]
    singletonsOnly = (q [Dec] -> ([Dec] -> q [Dec]) -> q [Dec]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ([Dec] -> [DDec] -> q [DDec]) -> [Dec] -> q [Dec]
    forall th ds (q :: * -> *).
    (Desugar th ds, DsMonad q) =>
    (th -> ds -> q ds) -> th -> q th
    wrapDesugar [Dec] -> [DDec] -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> [DDec] -> q [DDec]
    singTopLevelDecs)

    -- | Create instances of 'SEq' and type-level @(==)@ for each type in the list
    singEqInstances :: DsMonad q => [Name] -> q [Dec]
    singEqInstances :: [Name] -> q [Dec]
    singEqInstances = (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]
    singEqInstance

    -- | Create instance of 'SEq' and type-level @(==)@ for the given type
    singEqInstance :: DsMonad q => Name -> q [Dec]
    singEqInstance :: Name -> q [Dec]
    singEqInstance name :: Name
    name = do
      [Dec]
    promotion <- Name -> q [Dec]
    forall (q :: * -> *). DsMonad q => Name -> q [Dec]
    promoteEqInstance Name
    name
      [Dec]
    dec <- EqualityClassDesc q -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    EqualityClassDesc q -> Name -> q [Dec]
    singEqualityInstance EqualityClassDesc q
    forall (q :: * -> *). Quasi q => EqualityClassDesc q
    sEqClassDesc Name
    name
      [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]
    dec [Dec] -> [Dec] -> [Dec]
    forall a. [a] -> [a] -> [a]
    ++ [Dec]
    promotion

    -- | Create instances of 'SEq' (only -- no instance for @(==)@, which 'SEq' generally
    -- relies on) for each type in the list
    singEqInstancesOnly :: DsMonad q => [Name] -> q [Dec]
    singEqInstancesOnly :: [Name] -> q [Dec]
    singEqInstancesOnly = (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]
    singEqInstanceOnly

    -- | Create instances of 'SEq' (only -- no instance for @(==)@, which 'SEq' generally
    -- relies on) for the given type
    singEqInstanceOnly :: DsMonad q => Name -> q [Dec]
    singEqInstanceOnly :: Name -> q [Dec]
    singEqInstanceOnly name :: Name
    name = EqualityClassDesc q -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    EqualityClassDesc q -> Name -> q [Dec]
    singEqualityInstance EqualityClassDesc q
    forall (q :: * -> *). Quasi q => EqualityClassDesc q
    sEqClassDesc Name
    name

    -- | Create instances of 'SDecide', 'TestEquality', and 'TestCoercion' for each
    -- type in the list.
    singDecideInstances :: DsMonad q => [Name] -> q [Dec]
    singDecideInstances :: [Name] -> q [Dec]
    singDecideInstances = (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]
    singDecideInstance

    -- | Create instance of 'SDecide', 'TestEquality', and 'TestCoercion' for the
    -- given type.
    singDecideInstance :: DsMonad q => Name -> q [Dec]
    singDecideInstance :: Name -> q [Dec]
    singDecideInstance name :: Name
    name = EqualityClassDesc q -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    EqualityClassDesc q -> Name -> q [Dec]
    singEqualityInstance EqualityClassDesc q
    forall (q :: * -> *). Quasi q => EqualityClassDesc q
    sDecideClassDesc Name
    name

    -- generalized function for creating equality instances
    singEqualityInstance :: DsMonad q => EqualityClassDesc q -> Name -> q [Dec]
    singEqualityInstance :: EqualityClassDesc q -> Name -> q [Dec]
    singEqualityInstance desc :: EqualityClassDesc q
    desc@(_, _, className :: Name
    className, _) 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]
    ++
                                Name -> String
    forall a. Show a => a -> String
    show Name
    className String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for it.") Name
    name
      [DTyVarBndr]
    dtvbs <- (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]
    dtvbs
      [DCon]
    dcons <- (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]
    dtvbs DType
    data_ty) [Con]
    cons
      let tyvars :: [DType]
    tyvars = (DTyVarBndr -> DType) -> [DTyVarBndr] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> DType
    DVarT (Name -> DType) -> (DTyVarBndr -> Name) -> DTyVarBndr -> DType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DTyVarBndr -> Name
    extractTvbName) [DTyVarBndr]
    dtvbs
          kind :: DType
    kind = DType -> [DType] -> DType
    foldType (Name -> DType
    DConT Name
    name) [DType]
    tyvars
      (scons :: [DCon]
    scons, _) <- [Dec] -> SgM [DCon] -> q ([DCon], [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> SgM a -> q (a, [DDec])
    singM [] (SgM [DCon] -> q ([DCon], [DDec]))
    -> SgM [DCon] -> q ([DCon], [DDec])
    forall a b. (a -> b) -> a -> b
    $ (DCon -> SgM DCon) -> [DCon] -> SgM [DCon]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name -> DCon -> SgM DCon
    singCtor Name
    name) [DCon]
    dcons
      DDec
    eqInstance <- Maybe [DType]
    -> DType -> [DCon] -> [DCon] -> EqualityClassDesc q -> q DDec
    forall (q :: * -> *).
    DsMonad q =>
    Maybe [DType]
    -> DType -> [DCon] -> [DCon] -> EqualityClassDesc q -> q DDec
    mkEqualityInstance Maybe [DType]
    forall a. Maybe a
    Nothing DType
    kind [DCon]
    dcons [DCon]
    scons EqualityClassDesc q
    desc
      [DDec]
    testInstances <-
        if Name
    className Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    sDecideClassName
           then (TestInstance -> q DDec) -> [TestInstance] -> q [DDec]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Maybe [DType] -> DType -> Name -> [DCon] -> TestInstance -> q DDec
    forall (q :: * -> *).
    DsMonad q =>
    Maybe [DType] -> DType -> Name -> [DCon] -> TestInstance -> q DDec
    mkTestInstance Maybe [DType]
    forall a. Maybe a
    Nothing DType
    kind Name
    name [DCon]
    dcons)
                         [TestInstance
    TestEquality, TestInstance
    TestCoercion]
           else [DDec] -> q [DDec]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure []
      [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
    eqInstanceDDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :[DDec]
    testInstances)

    -- | Create instances of 'SOrd' for the given types
    singOrdInstances :: DsMonad q => [Name] -> q [Dec]
    singOrdInstances :: [Name] -> q [Dec]
    singOrdInstances = (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]
    singOrdInstance

    -- | Create instance of 'SOrd' for the given type
    singOrdInstance :: DsMonad q => Name -> q [Dec]
    singOrdInstance :: Name -> q [Dec]
    singOrdInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    singInstance DerivDesc q
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkOrdInstance "Ord"

    -- | Create instances of 'SBounded' for the given types
    singBoundedInstances :: DsMonad q => [Name] -> q [Dec]
    singBoundedInstances :: [Name] -> q [Dec]
    singBoundedInstances = (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]
    singBoundedInstance

    -- | Create instance of 'SBounded' for the given type
    singBoundedInstance :: DsMonad q => Name -> q [Dec]
    singBoundedInstance :: Name -> q [Dec]
    singBoundedInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    singInstance DerivDesc q
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkBoundedInstance "Bounded"

    -- | Create instances of 'SEnum' for the given types
    singEnumInstances :: DsMonad q => [Name] -> q [Dec]
    singEnumInstances :: [Name] -> q [Dec]
    singEnumInstances = (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]
    singEnumInstance

    -- | Create instance of 'SEnum' for the given type
    singEnumInstance :: DsMonad q => Name -> q [Dec]
    singEnumInstance :: Name -> q [Dec]
    singEnumInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    singInstance DerivDesc q
    forall (q :: * -> *). DsMonad q => DerivDesc q
    mkEnumInstance "Enum"

    -- | Create instance of 'SShow' for the given type
    --
    -- (Not to be confused with 'showShowInstance'.)
    singShowInstance :: DsMonad q => Name -> q [Dec]
    singShowInstance :: Name -> q [Dec]
    singShowInstance = DerivDesc q -> String -> Name -> q [Dec]
    forall (q :: * -> *).
    DsMonad q =>
    DerivDesc q -> String -> Name -> q [Dec]
    singInstance (ShowMode -> DerivDesc q
    forall (q :: * -> *). DsMonad q => ShowMode -> DerivDesc q
    mkShowInstance ShowMode
    ForPromotion) "Show"

    -- | Create instances of 'SShow' for the given types
    --
    -- (Not to be confused with 'showSingInstances'.)
    singShowInstances :: DsMonad q => [Name] -> q [Dec]
    singShowInstances :: [Name] -> q [Dec]
    singShowInstances = (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]
    singShowInstance

    -- | Create instance of 'Show' for the given singleton type
    --
    -- (Not to be confused with 'singShowInstance'.)
    showSingInstance :: DsMonad q => Name -> q [Dec]
    showSingInstance :: Name -> q [Dec]
    showSingInstance 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 Show for it.") Name
    name
      [DTyVarBndr]
    dtvbs <- (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]
    dtvbs
      [DCon]
    dcons <- (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]
    dtvbs DType
    data_ty) [Con]
    cons
      let tyvars :: [DType]
    tyvars    = (DTyVarBndr -> DType) -> [DTyVarBndr] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> DType
    DVarT (Name -> DType) -> (DTyVarBndr -> Name) -> DTyVarBndr -> DType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DTyVarBndr -> Name
    extractTvbName) [DTyVarBndr]
    dtvbs
          kind :: DType
    kind      = DType -> [DType] -> DType
    foldType (Name -> DType
    DConT Name
    name) [DType]
    tyvars
          data_decl :: DataDecl
    data_decl = Name -> [DTyVarBndr] -> [DCon] -> DataDecl
    DataDecl Name
    name [DTyVarBndr]
    dtvbs [DCon]
    dcons
          deriv_show_decl :: DerivedDecl cls
    deriv_show_decl = DerivedDecl :: forall (cls :: * -> Constraint).
    Maybe [DType] -> DType -> Name -> DataDecl -> DerivedDecl cls
    DerivedDecl { ded_mb_cxt :: Maybe [DType]
    ded_mb_cxt     = Maybe [DType]
    forall a. Maybe a
    Nothing
                                        , ded_type :: DType
    ded_type       = DType
    kind
                                        , ded_type_tycon :: Name
    ded_type_tycon = Name
    name
                                        , ded_decl :: DataDecl
    ded_decl       = DataDecl
    data_decl }
      (show_insts :: [DDec]
    show_insts, _) <- [Dec] -> SgM [DDec] -> q ([DDec], [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> SgM a -> q (a, [DDec])
    singM [] (SgM [DDec] -> q ([DDec], [DDec]))
    -> SgM [DDec] -> q ([DDec], [DDec])
    forall a b. (a -> b) -> a -> b
    $ DerivedShowDecl -> SgM [DDec]
    singDerivedShowDecs DerivedShowDecl
    forall (cls :: * -> Constraint). DerivedDecl cls
    deriv_show_decl
      [Dec] -> q [Dec]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ [DDec] -> [Dec]
    decsToTH [DDec]
    show_insts

    -- | Create instances of 'Show' for the given singleton types
    --
    -- (Not to be confused with 'singShowInstances'.)
    showSingInstances :: DsMonad q => [Name] -> q [Dec]
    showSingInstances :: [Name] -> q [Dec]
    showSingInstances = (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]
    showSingInstance

    -- | Create an instance for @'SingI' TyCon{N}@, where @N@ is the positive
    -- number provided as an argument.
    --
    -- Note that the generated code requires the use of the @QuantifiedConstraints@
    -- language extension.
    singITyConInstances :: DsMonad q => [Int] -> q [Dec]
    singITyConInstances :: [Int] -> q [Dec]
    singITyConInstances = (Int -> q [Dec]) -> [Int] -> q [Dec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM Int -> q [Dec]
    forall (q :: * -> *). DsMonad q => Int -> q [Dec]
    singITyConInstance

    -- | Create an instance for @'SingI' TyCon{N}@, where @N@ is the positive
    -- number provided as an argument.
    --
    -- Note that the generated code requires the use of the @QuantifiedConstraints@
    -- language extension.
    singITyConInstance :: DsMonad q => Int -> q [Dec]
    singITyConInstance :: Int -> q [Dec]
    singITyConInstance n :: Int
    n
      | Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= 0
      = String -> q [Dec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> q [Dec]) -> String -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ "Argument must be a positive number (given " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
      | Bool
    otherwise
      = do [Name]
    as <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    n (String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "a")
           [Name]
    ks <- Int -> q Name -> q [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    n (String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "k")
           Name
    k_last <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "k_last"
           Name
    f      <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "f"
           Name
    x      <- String -> q Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "x"
           let k_penult :: Name
    k_penult = [Name] -> Name
    forall a. [a] -> a
    last [Name]
    ks
               k_fun :: DType
    k_fun = [DType] -> DType -> DType
    ravel ((Name -> DType) -> [Name] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    ks) (Name -> DType
    DVarT Name
    k_last)
               f_ty :: DType
    f_ty  = Name -> DType
    DVarT Name
    f
               a_tys :: [DType]
    a_tys = (Name -> DType) -> [Name] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    as
               mk_fun :: DType -> DType -> DType -> DType
    mk_fun arrow :: DType
    arrow t1 :: DType
    t1 t2 :: DType
    t2 = DType
    arrow DType -> DType -> DType
    `DAppT` DType
    t1 DType -> DType -> DType
    `DAppT` DType
    t2
               matchable_apply_fun :: DType
    matchable_apply_fun   = DType -> DType -> DType -> DType
    mk_fun DType
    DArrowT                (Name -> DType
    DVarT Name
    k_penult) (Name -> DType
    DVarT Name
    k_last)
               unmatchable_apply_fun :: DType
    unmatchable_apply_fun = DType -> DType -> DType -> DType
    mk_fun (Name -> DType
    DConT Name
    tyFunArrowName) (Name -> DType
    DVarT Name
    k_penult) (Name -> DType
    DVarT Name
    k_last)
               ctxt :: [DType]
    ctxt = [ [DTyVarBndr] -> [DType] -> DType -> DType
    DForallT ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    as)
                                 ((DType -> DType) -> [DType] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (DType -> DType -> DType
    DAppT (Name -> DType
    DConT Name
    singIName)) [DType]
    a_tys)
                                 (Name -> DType
    DConT Name
    singIName DType -> DType -> DType
    `DAppT` DType -> [DType] -> DType
    foldType DType
    f_ty [DType]
    a_tys)
                      , Name -> DType
    DConT Name
    equalityName
                          DType -> DType -> DType
    `DAppT` (Name -> DType
    DConT Name
    applyTyConName DType -> DType -> DType
    `DSigT`
                                    DType -> DType -> DType -> DType
    mk_fun DType
    DArrowT DType
    matchable_apply_fun DType
    unmatchable_apply_fun)
                          DType -> DType -> DType
    `DAppT` Name -> DType
    DConT Name
    applyTyConAux1Name
                      ]
           [Dec] -> q [Dec]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ([Dec] -> q [Dec]) -> [Dec] -> q [Dec]
    forall a b. (a -> b) -> a -> b
    $ DDec -> [Dec]
    decToTH
                (DDec -> [Dec]) -> DDec -> [Dec]
    forall a b. (a -> b) -> a -> b
    $ Maybe Overlap
    -> Maybe [DTyVarBndr] -> [DType] -> DType -> [DDec] -> DDec
    DInstanceD
                    Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing [DType]
    ctxt
                    (Name -> DType
    DConT Name
    singIName DType -> DType -> DType
    `DAppT` (Name -> DType
    DConT (Int -> Name
    mkTyConName Int
    n) DType -> DType -> DType
    `DAppT` (DType
    f_ty DType -> DType -> DType
    `DSigT` DType
    k_fun)))
                    [DLetDec -> DDec
    DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
    forall a b. (a -> b) -> a -> b
    $ Name -> [DClause] -> DLetDec
    DFunD Name
    singMethName
                               [[DPat] -> DExp -> DClause
    DClause [] (DExp -> DClause) -> DExp -> DClause
    forall a b. (a -> b) -> a -> b
    $
                                Int -> DType -> DExp -> DExp
    wrapSingFun 1 DType
    DWildCardT (DExp -> DExp) -> DExp -> DExp
    forall a b. (a -> b) -> a -> b
    $
                                [Name] -> DExp -> DExp
    DLamE [Name
    x] (DExp -> DExp) -> DExp -> DExp
    forall a b. (a -> b) -> a -> b
    $
                                Name -> DExp
    DVarE Name
    withSingIName DExp -> DExp -> DExp
    `DAppE` Name -> DExp
    DVarE Name
    x
                                                    DExp -> DExp -> DExp
    `DAppE` Name -> DExp
    DVarE Name
    singMethName]]

    singInstance :: DsMonad q => DerivDesc q -> String -> Name -> q [Dec]
    singInstance :: DerivDesc q -> String -> Name -> q [Dec]
    singInstance mk_inst :: DerivDesc q
    mk_inst inst_name :: String
    inst_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
    inst_name
                                String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " for it.") Name
    name
      [DTyVarBndr]
    dtvbs <- (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]
    dtvbs
      [DCon]
    dcons <- (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]
    dtvbs DType
    data_ty) [Con]
    cons
      let data_decl :: DataDecl
    data_decl = Name -> [DTyVarBndr] -> [DCon] -> DataDecl
    DataDecl Name
    name [DTyVarBndr]
    dtvbs [DCon]
    dcons
      UInstDecl
    raw_inst <- DerivDesc q
    mk_inst Maybe [DType]
    forall a. Maybe a
    Nothing DType
    data_ty DataDecl
    data_decl
      (a_inst :: AInstDecl
    a_inst, decs :: [DDec]
    decs) <- [Dec] -> PrM AInstDecl -> q (AInstDecl, [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> PrM a -> q (a, [DDec])
    promoteM [] (PrM AInstDecl -> q (AInstDecl, [DDec]))
    -> PrM AInstDecl -> q (AInstDecl, [DDec])
    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
      [DDec]
    decs' <- [Dec] -> SgM [DDec] -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> SgM [DDec] -> q [DDec]
    singDecsM [] (SgM [DDec] -> q [DDec]) -> SgM [DDec] -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ (DDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :[]) (DDec -> [DDec]) -> SgM DDec -> SgM [DDec]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> AInstDecl -> SgM DDec
    singInstD AInstDecl
    a_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 [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    decs')

    singInfo :: DsMonad q => DInfo -> q [DDec]
    singInfo :: DInfo -> q [DDec]
    singInfo (DTyConI dec :: DDec
    dec _) =
      [Dec] -> [DDec] -> q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> [DDec] -> q [DDec]
    singTopLevelDecs [] [DDec
    dec]
    singInfo (DPrimTyConI _name :: Name
    _name _numArgs :: Int
    _numArgs _unlifted :: Bool
    _unlifted) =
      String -> q [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of primitive type constructors not supported"
    singInfo (DVarI _name :: Name
    _name _ty :: DType
    _ty _mdec :: Maybe Name
    _mdec) =
      String -> q [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of value info not supported"
    singInfo (DTyVarI _name :: Name
    _name _ty :: DType
    _ty) =
      String -> q [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of type variable info not supported"
    singInfo (DPatSynI {}) =
      String -> q [DDec]
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of pattern synonym info not supported"

    singTopLevelDecs :: DsMonad q => [Dec] -> [DDec] -> q [DDec]
    singTopLevelDecs :: [Dec] -> [DDec] -> q [DDec]
    singTopLevelDecs locals :: [Dec]
    locals raw_decls :: [DDec]
    raw_decls = [Dec] -> DsM q [DDec] -> q [DDec]
    forall (q :: * -> *) a. DsMonad q => [Dec] -> DsM q a -> q a
    withLocalDeclarations [Dec]
    locals (DsM q [DDec] -> q [DDec]) -> DsM q [DDec] -> q [DDec]
    forall a b. (a -> b) -> a -> b
    $ do
      [DDec]
    decls <- [DDec] -> DsM q [DDec]
    forall (q :: * -> *) a. (DsMonad q, Data a) => a -> q a
    expand [DDec]
    raw_decls     -- expand type synonyms
      PDecs { pd_let_decs :: PartitionedDecs -> [DLetDec]
    pd_let_decs                = [DLetDec]
    letDecls
            , 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]
    derivedEqDecs
            , pd_derived_show_decs :: PartitionedDecs -> [DerivedShowDecl]
    pd_derived_show_decs       = [DerivedShowDecl]
    derivedShowDecs } <- [DDec] -> DsM q PartitionedDecs
    forall (m :: * -> *). DsMonad m => [DDec] -> m PartitionedDecs
    partitionDecs [DDec]
    decls

      ((letDecEnv :: ALetDecEnv
    letDecEnv, classes' :: [AClassDecl]
    classes', insts' :: [AInstDecl]
    insts'), promDecls :: [DDec]
    promDecls) <- [Dec]
    -> PrM (ALetDecEnv, [AClassDecl], [AInstDecl])
    -> DsM q ((ALetDecEnv, [AClassDecl], [AInstDecl]), [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> PrM a -> q (a, [DDec])
    promoteM [Dec]
    locals (PrM (ALetDecEnv, [AClassDecl], [AInstDecl])
     -> DsM q ((ALetDecEnv, [AClassDecl], [AInstDecl]), [DDec]))
    -> PrM (ALetDecEnv, [AClassDecl], [AInstDecl])
    -> DsM q ((ALetDecEnv, [AClassDecl], [AInstDecl]), [DDec])
    forall a b. (a -> b) -> a -> b
    $ do
        [TySynDecl]
    -> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
    defunTypeDecls [TySynDecl]
    ty_syns [ClosedTypeFamilyDecl]
    c_tyfams [OpenTypeFamilyDecl]
    o_tyfams
        [DataDecl] -> PrM ()
    promoteDataDecs [DataDecl]
    datas
        (_, letDecEnv :: ALetDecEnv
    letDecEnv) <- (String, String) -> [DLetDec] -> PrM ([LetBind], ALetDecEnv)
    promoteLetDecs (String, String)
    noPrefix [DLetDec]
    letDecls
        [AClassDecl]
    classes' <- (UClassDecl -> PrM AClassDecl) -> [UClassDecl] -> PrM [AClassDecl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM UClassDecl -> PrM AClassDecl
    promoteClassDec [UClassDecl]
    classes
        let meth_sigs :: OMap Name DType
    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
        [AInstDecl]
    insts' <- (UInstDecl -> PrM AInstDecl) -> [UInstDecl] -> PrM [AInstDecl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (OMap Name DType -> UInstDecl -> PrM AInstDecl
    promoteInstanceDec OMap Name DType
    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]
    derivedEqDecs
        (ALetDecEnv, [AClassDecl], [AInstDecl])
    -> PrM (ALetDecEnv, [AClassDecl], [AInstDecl])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ALetDecEnv
    letDecEnv, [AClassDecl]
    classes', [AInstDecl]
    insts')

      [Dec] -> SgM [DDec] -> DsM q [DDec]
    forall (q :: * -> *). DsMonad q => [Dec] -> SgM [DDec] -> q [DDec]
    singDecsM [Dec]
    locals (SgM [DDec] -> DsM q [DDec]) -> SgM [DDec] -> DsM q [DDec]
    forall a b. (a -> b) -> a -> b
    $ do
        let letBinds :: [(Name, DExp)]
    letBinds = (DataDecl -> [(Name, DExp)]) -> [DataDecl] -> [(Name, DExp)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap DataDecl -> [(Name, DExp)]
    buildDataLets [DataDecl]
    datas
                    [(Name, DExp)] -> [(Name, DExp)] -> [(Name, DExp)]
    forall a. [a] -> [a] -> [a]
    ++ (UClassDecl -> [(Name, DExp)]) -> [UClassDecl] -> [(Name, DExp)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap UClassDecl -> [(Name, DExp)]
    buildMethLets [UClassDecl]
    classes
        (newLetDecls :: [DLetDec]
    newLetDecls, singIDefunDecls :: [DDec]
    singIDefunDecls, newDecls :: [DDec]
    newDecls)
                                <- [(Name, DExp)]
    -> SgM ([DLetDec], [DDec], [DDec])
    -> SgM ([DLetDec], [DDec], [DDec])
    forall a. [(Name, DExp)] -> SgM a -> SgM a
    bindLets [(Name, DExp)]
    letBinds (SgM ([DLetDec], [DDec], [DDec])
     -> SgM ([DLetDec], [DDec], [DDec]))
    -> SgM ([DLetDec], [DDec], [DDec])
    -> SgM ([DLetDec], [DDec], [DDec])
    forall a b. (a -> b) -> a -> b
    $
                                   ALetDecEnv -> SgM [DDec] -> SgM ([DLetDec], [DDec], [DDec])
    forall a. ALetDecEnv -> SgM a -> SgM ([DLetDec], [DDec], a)
    singLetDecEnv ALetDecEnv
    letDecEnv (SgM [DDec] -> SgM ([DLetDec], [DDec], [DDec]))
    -> SgM [DDec] -> SgM ([DLetDec], [DDec], [DDec])
    forall a b. (a -> b) -> a -> b
    $ do
                                     [DDec]
    newDataDecls <- (DataDecl -> SgM [DDec]) -> [DataDecl] -> SgM [DDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM DataDecl -> SgM [DDec]
    singDataD [DataDecl]
    datas
                                     [DDec]
    newClassDecls <- (AClassDecl -> SgM DDec) -> [AClassDecl] -> SgM [DDec]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM AClassDecl -> SgM DDec
    singClassD [AClassDecl]
    classes'
                                     [DDec]
    newInstDecls <- (AInstDecl -> SgM DDec) -> [AInstDecl] -> SgM [DDec]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM AInstDecl -> SgM DDec
    singInstD [AInstDecl]
    insts'
                                     [DDec]
    newDerivedEqDecs <- (DerivedEqDecl -> SgM [DDec]) -> [DerivedEqDecl] -> SgM [DDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM DerivedEqDecl -> SgM [DDec]
    singDerivedEqDecs [DerivedEqDecl]
    derivedEqDecs
                                     [DDec]
    newDerivedShowDecs <- (DerivedShowDecl -> SgM [DDec]) -> [DerivedShowDecl] -> SgM [DDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM DerivedShowDecl -> SgM [DDec]
    singDerivedShowDecs [DerivedShowDecl]
    derivedShowDecs
                                     [DDec] -> SgM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
    forall a b. (a -> b) -> a -> b
    $ [DDec]
    newDataDecls [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    newClassDecls
                                                           [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    newInstDecls
                                                           [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    newDerivedEqDecs
                                                           [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    newDerivedShowDecs
        [DDec] -> SgM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
    forall a b. (a -> b) -> a -> b
    $ [DDec]
    promDecls [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ ((DLetDec -> DDec) -> [DLetDec] -> [DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map DLetDec -> DDec
    DLetDec [DLetDec]
    newLetDecls) [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    singIDefunDecls [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    newDecls

    -- see comment at top of file
    buildDataLets :: DataDecl -> [(Name, DExp)]
    buildDataLets :: DataDecl -> [(Name, DExp)]
    buildDataLets (DataDecl _name :: Name
    _name _tvbs :: [DTyVarBndr]
    _tvbs cons :: [DCon]
    cons) =
      (DCon -> [(Name, DExp)]) -> [DCon] -> [(Name, DExp)]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap DCon -> [(Name, DExp)]
    con_num_args [DCon]
    cons
      where
        con_num_args :: DCon -> [(Name, DExp)]
        con_num_args :: DCon -> [(Name, DExp)]
    con_num_args (DCon _tvbs :: [DTyVarBndr]
    _tvbs _cxt :: [DType]
    _cxt name :: Name
    name fields :: DConFields
    fields _rty :: DType
    _rty) =
          (Name
    name, Int -> DType -> DExp -> DExp
    wrapSingFun ([DType] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (DConFields -> [DType]
    tysOfConFields DConFields
    fields))
                             (Name -> DType
    promoteValRhs Name
    name) (Name -> DExp
    DConE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    singDataConName Name
    name))
          (Name, DExp) -> [(Name, DExp)] -> [(Name, DExp)]
    forall a. a -> [a] -> [a]
    : DConFields -> [(Name, DExp)]
    rec_selectors DConFields
    fields

        rec_selectors :: DConFields -> [(Name, DExp)]
        rec_selectors :: DConFields -> [(Name, DExp)]
    rec_selectors (DNormalC {}) = []
        rec_selectors (DRecC fields :: [DVarBangType]
    fields) =
          let names :: [Name]
    names = (DVarBangType -> Name) -> [DVarBangType] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DVarBangType -> Name
    forall a b c. (a, b, c) -> a
    fstOf3 [DVarBangType]
    fields in
          [ (Name
    name, Int -> DType -> DExp -> DExp
    wrapSingFun 1 (Name -> DType
    promoteValRhs Name
    name) (Name -> DExp
    DVarE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    singValName Name
    name))
          | Name
    name <- [Name]
    names ]

    -- see comment at top of file
    buildMethLets :: UClassDecl -> [(Name, DExp)]
    buildMethLets :: UClassDecl -> [(Name, DExp)]
    buildMethLets (ClassDecl { cd_lde :: forall (ann :: AnnotationFlag). ClassDecl ann -> LetDecEnv ann
    cd_lde = LetDecEnv { lde_types :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
    lde_types = OMap Name DType
    meth_sigs } }) =
      (LetBind -> (Name, DExp)) -> [LetBind] -> [(Name, DExp)]
    forall a b. (a -> b) -> [a] -> [b]
    map LetBind -> (Name, DExp)
    mk_bind (OMap Name DType -> [LetBind]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name DType
    meth_sigs)
      where
        mk_bind :: LetBind -> (Name, DExp)
    mk_bind (meth_name :: Name
    meth_name, meth_ty :: DType
    meth_ty) =
          ( Name
    meth_name
          , Int -> DType -> DExp -> DExp
    wrapSingFun (DType -> Int
    countArgs DType
    meth_ty) (Name -> DType
    promoteValRhs Name
    meth_name)
                                            (Name -> DExp
    DVarE (Name -> DExp) -> Name -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> Name
    singValName Name
    meth_name) )

    singClassD :: AClassDecl -> SgM DDec
    singClassD :: AClassDecl -> SgM DDec
    singClassD (ClassDecl { cd_cxt :: forall (ann :: AnnotationFlag). ClassDecl ann -> [DType]
    cd_cxt  = [DType]
    cls_cxt
                          , cd_name :: forall (ann :: AnnotationFlag). ClassDecl ann -> Name
    cd_name = Name
    cls_name
                          , cd_tvbs :: forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndr]
    cd_tvbs = [DTyVarBndr]
    cls_tvbs
                          , cd_fds :: forall (ann :: AnnotationFlag). ClassDecl ann -> [FunDep]
    cd_fds  = [FunDep]
    cls_fundeps
                          , cd_lde :: forall (ann :: AnnotationFlag). ClassDecl ann -> LetDecEnv ann
    cd_lde  = LetDecEnv { lde_defns :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> OMap Name (LetDecRHS ann)
    lde_defns     = OMap Name (LetDecRHS Annotated)
    default_defns
                                                , 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
    fixities
                                                , lde_proms :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> IfAnn ann (OMap Name DType) ()
    lde_proms     = IfAnn Annotated (OMap Name DType) ()
    promoted_defaults
                                                , lde_bound_kvs :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> IfAnn ann (OMap Name (OSet Name)) ()
    lde_bound_kvs = IfAnn Annotated (OMap Name (OSet Name)) ()
    meth_bound_kvs } }) =
      [DType] -> SgM DDec -> SgM DDec
    forall a. [DType] -> SgM a -> SgM a
    bindContext [DType -> [DTyVarBndr] -> DType
    foldTypeTvbs (Name -> DType
    DConT Name
    cls_name) [DTyVarBndr]
    cls_tvbs] (SgM DDec -> SgM DDec) -> SgM DDec -> SgM DDec
    forall a b. (a -> b) -> a -> b
    $ do
        (sing_sigs :: [DLetDec]
    sing_sigs, _, tyvar_names :: [(Name, [Name])]
    tyvar_names, cxts :: [(Name, [DType])]
    cxts, res_kis :: [Maybe DType]
    res_kis, singIDefunss :: [[DDec]]
    singIDefunss)
          <- [(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
      Maybe DType, [DDec])]
    -> ([DLetDec], [(Name, DExp)], [(Name, [Name])], [(Name, [DType])],
        [Maybe DType], [[DDec]])
    forall a b c d e f.
    [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])
    unzip6 ([(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
       Maybe DType, [DDec])]
     -> ([DLetDec], [(Name, DExp)], [(Name, [Name])], [(Name, [DType])],
         [Maybe DType], [[DDec]]))
    -> SgM
         [(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec])]
    -> SgM
         ([DLetDec], [(Name, DExp)], [(Name, [Name])], [(Name, [DType])],
          [Maybe DType], [[DDec]])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Name
     -> DType
     -> SgM
          (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec]))
    -> [Name]
    -> [DType]
    -> SgM
         [(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec])]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM (OMap Name (LetDecRHS Annotated)
    -> OMap Name DType
    -> OMap Name (OSet Name)
    -> Name
    -> DType
    -> SgM
         (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
          Maybe DType, [DDec])
    singTySig OMap Name (LetDecRHS Annotated)
    forall a. a
    no_meth_defns OMap Name DType
    meth_sigs OMap Name (OSet Name)
    IfAnn Annotated (OMap Name (OSet Name)) ()
    meth_bound_kvs)
                                 [Name]
    meth_names ((Name -> DType) -> [Name] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    promoteValRhs [Name]
    meth_names)
        [DDec] -> SgM ()
    forall (m :: * -> *). MonadWriter [DDec] m => [DDec] -> m ()
    emitDecs ([DDec] -> SgM ()) -> [DDec] -> SgM ()
    forall a b. (a -> b) -> a -> b
    $ [[DDec]] -> [DDec]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[DDec]]
    singIDefunss
        let default_sigs :: [DDec]
    default_sigs = [Maybe DDec] -> [DDec]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe DDec] -> [DDec]) -> [Maybe DDec] -> [DDec]
    forall a b. (a -> b) -> a -> b
    $
                           (Name -> DLetDec -> (Name, [Name]) -> Maybe DType -> Maybe DDec)
    -> [Name]
    -> [DLetDec]
    -> [(Name, [Name])]
    -> [Maybe DType]
    -> [Maybe DDec]
    forall a b c d e.
    (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]
    zipWith4 Name -> DLetDec -> (Name, [Name]) -> Maybe DType -> Maybe DDec
    forall a.
    Name -> DLetDec -> (a, [Name]) -> Maybe DType -> Maybe DDec
    mk_default_sig [Name]
    meth_names [DLetDec]
    sing_sigs [(Name, [Name])]
    tyvar_names [Maybe DType]
    res_kis
            res_ki_map :: Map Name DType
    res_ki_map   = [LetBind] -> Map Name DType
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([Name] -> [DType] -> [LetBind]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    meth_names
                                             ((Maybe DType -> DType) -> [Maybe DType] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (DType -> Maybe DType -> DType
    forall a. a -> Maybe a -> a
    fromMaybe DType
    forall a. a
    always_sig) [Maybe DType]
    res_kis))
        [DLetDec]
    sing_meths <- ((Name, LetDecRHS Annotated) -> SgM DLetDec)
    -> [(Name, LetDecRHS Annotated)] -> SgM [DLetDec]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Name -> LetDecRHS Annotated -> SgM DLetDec)
    -> (Name, LetDecRHS Annotated) -> SgM DLetDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Map Name [Name]
    -> Map Name [DType]
    -> Map Name DType
    -> Name
    -> LetDecRHS Annotated
    -> SgM DLetDec
    singLetDecRHS ([(Name, [Name])] -> Map Name [Name]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, [Name])]
    tyvar_names)
                                                   ([(Name, [DType])] -> Map Name [DType]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, [DType])]
    cxts)
                                                   Map Name DType
    res_ki_map))
                           (OMap Name (LetDecRHS Annotated) -> [(Name, LetDecRHS Annotated)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name (LetDecRHS Annotated)
    default_defns)
        [DLetDec]
    fixities' <- ((Name, Fixity) -> SgM DLetDec)
    -> [(Name, Fixity)] -> SgM [DLetDec]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Name -> Fixity -> SgM DLetDec) -> (Name, Fixity) -> SgM DLetDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Fixity -> SgM DLetDec
    forall (q :: * -> *). DsMonad q => Name -> Fixity -> q DLetDec
    singInfixDecl) ([(Name, Fixity)] -> SgM [DLetDec])
    -> [(Name, Fixity)] -> SgM [DLetDec]
    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
    fixities
        [DType]
    cls_cxt' <- (DType -> SgM DType) -> [DType] -> SgM [DType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    singPred [DType]
    cls_cxt
        DDec -> SgM DDec
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DDec -> SgM DDec) -> DDec -> SgM DDec
    forall a b. (a -> b) -> a -> b
    $ [DType] -> Name -> [DTyVarBndr] -> [FunDep] -> [DDec] -> DDec
    DClassD [DType]
    cls_cxt'
                         (Name -> Name
    singClassName Name
    cls_name)
                         [DTyVarBndr]
    cls_tvbs
                         [FunDep]
    cls_fundeps   -- they are fine without modification
                         ((DLetDec -> DDec) -> [DLetDec] -> [DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map DLetDec -> DDec
    DLetDec ([DLetDec]
    sing_sigs [DLetDec] -> [DLetDec] -> [DLetDec]
    forall a. [a] -> [a] -> [a]
    ++ [DLetDec]
    sing_meths [DLetDec] -> [DLetDec] -> [DLetDec]
    forall a. [a] -> [a] -> [a]
    ++ [DLetDec]
    fixities') [DDec] -> [DDec] -> [DDec]
    forall a. [a] -> [a] -> [a]
    ++ [DDec]
    default_sigs)
      where
        no_meth_defns :: a
    no_meth_defns = String -> a
    forall a. HasCallStack => String -> a
    error "Internal error: can't find declared method type"
        always_sig :: a
    always_sig    = String -> a
    forall a. HasCallStack => String -> a
    error "Internal error: no signature for default method"
        meth_names :: [Name]
    meth_names    = (LetBind -> Name) -> [LetBind] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map LetBind -> Name
    forall a b. (a, b) -> a
    fst ([LetBind] -> [Name]) -> [LetBind] -> [Name]
    forall a b. (a -> b) -> a -> b
    $ OMap Name DType -> [LetBind]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name DType
    meth_sigs

        mk_default_sig :: Name -> DLetDec -> (a, [Name]) -> Maybe DType -> Maybe DDec
    mk_default_sig meth_name :: Name
    meth_name (DSigD s_name :: Name
    s_name sty :: DType
    sty) bound_kvs :: (a, [Name])
    bound_kvs (Just res_ki :: DType
    res_ki) =
          Name -> DType -> DDec
    DDefaultSigD Name
    s_name (DType -> DDec) -> Maybe DType -> Maybe DDec
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Name -> DType -> (a, [Name]) -> DType -> Maybe DType
    forall a. Name -> DType -> (a, [Name]) -> DType -> Maybe DType
    add_constraints Name
    meth_name DType
    sty (a, [Name])
    bound_kvs DType
    res_ki
        mk_default_sig _ _ _ _ = String -> Maybe DDec
    forall a. HasCallStack => String -> a
    error "Internal error: a singled signature isn't a signature."

        add_constraints :: Name -> DType -> (a, [Name]) -> DType -> Maybe DType
    add_constraints meth_name :: Name
    meth_name sty :: DType
    sty (_, bound_kvs :: [Name]
    bound_kvs) res_ki :: DType
    res_ki = do  -- Maybe monad
          DType
    prom_dflt <- 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
    IfAnn Annotated (OMap Name DType) ()
    promoted_defaults
          let default_pred :: DType
    default_pred = DType -> [DType] -> DType
    foldType (Name -> DType
    DConT Name
    equalityName)
                                    -- NB: Need the res_ki here to prevent ambiguous
                                    -- kinds in result-inferred default methods.
                                    -- See #175
                                   [ DType -> [DType] -> DType
    foldApply (Name -> DType
    promoteValRhs Name
    meth_name) [DType]
    tvs DType -> DType -> DType
    `DSigT` DType
    res_ki
                                   , DType -> [DType] -> DType
    foldApply DType
    prom_dflt [DType]
    tvs ]
          DType -> Maybe DType
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DType -> Maybe DType) -> DType -> Maybe DType
    forall a b. (a -> b) -> a -> b
    $ [DTyVarBndr] -> [DType] -> DType -> DType
    DForallT [DTyVarBndr]
    tvbs (DType
    default_pred DType -> [DType] -> [DType]
    forall a. a -> [a] -> [a]
    : [DType]
    cxt) ([DType] -> DType -> DType
    ravel [DType]
    args DType
    res)
          where
            (tvbs :: [DTyVarBndr]
    tvbs, cxt :: [DType]
    cxt, args :: [DType]
    args, res :: DType
    res) = DType -> ([DTyVarBndr], [DType], [DType], DType)
    unravel DType
    sty
            bound_kv_set :: Set Name
    bound_kv_set = [Name] -> Set Name
    forall a. Ord a => [a] -> Set a
    Set.fromList [Name]
    bound_kvs
            -- Filter out explicitly bound kind variables. Otherwise, if you had
            -- the following class (#312):
            --
            --  class Foo a where
            --    bar :: a -> b -> b
            --    bar _ x = x
            --
            -- Then it would be singled to:
            --
            --  class SFoo a where
            --    sBar :: forall b (x :: a) (y :: b). Sing x -> Sing y -> Sing (sBar x y)
            --    default :: forall b (x :: a) (y :: b).
            --               (Bar b x y) ~ (BarDefault b x y) => ...
            --
            -- Which applies Bar/BarDefault to b, which shouldn't happen.
            tvs :: [DType]
    tvs = (DTyVarBndr -> DType) -> [DTyVarBndr] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> DType
    tvbToType ([DTyVarBndr] -> [DType]) -> [DTyVarBndr] -> [DType]
    forall a b. (a -> b) -> a -> b
    $
                  (DTyVarBndr -> Bool) -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (\tvb :: DTyVarBndr
    tvb -> DTyVarBndr -> Name
    extractTvbName DTyVarBndr
    tvb Name -> Set Name -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set Name
    bound_kv_set) [DTyVarBndr]
    tvbs

    singInstD :: AInstDecl -> SgM DDec
    singInstD :: AInstDecl -> SgM DDec
    singInstD (InstDecl { id_cxt :: forall (ann :: AnnotationFlag). InstDecl ann -> [DType]
    id_cxt = [DType]
    cxt, id_name :: forall (ann :: AnnotationFlag). InstDecl ann -> Name
    id_name = Name
    inst_name, id_arg_tys :: forall (ann :: AnnotationFlag). InstDecl ann -> [DType]
    id_arg_tys = [DType]
    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 Annotated)]
    ann_meths }) = do
      [DType] -> SgM DDec -> SgM DDec
    forall a. [DType] -> SgM a -> SgM a
    bindContext [DType]
    cxt (SgM DDec -> SgM DDec) -> SgM DDec -> SgM DDec
    forall a b. (a -> b) -> a -> b
    $ do
        [DType]
    cxt' <- (DType -> SgM DType) -> [DType] -> SgM [DType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    singPred [DType]
    cxt
        [DType]
    inst_kis <- (DType -> SgM DType) -> [DType] -> SgM [DType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType [DType]
    inst_tys
        [DDec]
    meths <- ((Name, LetDecRHS Annotated) -> SgM [DDec])
    -> [(Name, LetDecRHS Annotated)] -> SgM [DDec]
    forall (monad :: * -> *) monoid (t :: * -> *) a.
    (Monad monad, Monoid monoid, Traversable t) =>
    (a -> monad monoid) -> t a -> monad monoid
    concatMapM ((Name -> LetDecRHS Annotated -> SgM [DDec])
    -> (Name, LetDecRHS Annotated) -> SgM [DDec]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> LetDecRHS Annotated -> SgM [DDec]
    sing_meth) [(Name, LetDecRHS Annotated)]
    ann_meths
        DDec -> SgM DDec
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Overlap
    -> Maybe [DTyVarBndr] -> [DType] -> DType -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing
                           Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing
                           [DType]
    cxt'
                           ((DType -> DType -> DType) -> DType -> [DType] -> DType
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl DType -> DType -> DType
    DAppT (Name -> DType
    DConT Name
    s_inst_name) [DType]
    inst_kis)
                           [DDec]
    meths)

      where
        s_inst_name :: Name
    s_inst_name = Name -> Name
    singClassName Name
    inst_name

        sing_meth :: Name -> ALetDecRHS -> SgM [DDec]
        sing_meth :: Name -> LetDecRHS Annotated -> SgM [DDec]
    sing_meth name :: Name
    name rhs :: LetDecRHS Annotated
    rhs = do
          Maybe DInfo
    mb_s_info <- Name -> SgM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReify (Name -> Name
    singValName Name
    name)
          [DType]
    inst_kis <- (DType -> SgM DType) -> [DType] -> SgM [DType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType [DType]
    inst_tys
          let mk_subst :: [DTyVarBndr] -> Map Name DType
    mk_subst cls_tvbs :: [DTyVarBndr]
    cls_tvbs = [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] -> [DType] -> [LetBind]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    vis_cls_tvbs) [DType]
    inst_kis
                where
                  -- This is a half-hearted attempt to address the underlying problem
                  -- in #358, where we can sometimes have more class type variables
                  -- (due to implicit kind arguments) than class arguments. This just
                  -- ensures that the explicit type variables are properly mapped
                  -- to the class arguments, leaving the implicit kind variables
                  -- unmapped. That could potentially cause *other* problems, but
                  -- those are perhaps best avoided by using InstanceSigs. At the
                  -- very least, this workaround will make error messages slightly
                  -- less confusing.
                  vis_cls_tvbs :: [DTyVarBndr]
    vis_cls_tvbs = Int -> [DTyVarBndr] -> [DTyVarBndr]
    forall a. Int -> [a] -> [a]
    drop ([DTyVarBndr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [DTyVarBndr]
    cls_tvbs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [DType] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [DType]
    inst_kis) [DTyVarBndr]
    cls_tvbs

              sing_meth_ty :: OSet Name -> DType
                           -> SgM (DType, [Name], DCxt, DKind)
              sing_meth_ty :: OSet Name -> DType -> SgM (DType, [Name], [DType], DType)
    sing_meth_ty bound_kvs :: OSet Name
    bound_kvs inner_ty :: DType
    inner_ty = do
                -- Make sure to expand through type synonyms here! Not doing so
                -- resulted in #167.
                DType
    raw_ty <- DType -> SgM DType
    forall (q :: * -> *) a. (DsMonad q, Data a) => a -> q a
    expand DType
    inner_ty
                (s_ty :: DType
    s_ty, _num_args :: Int
    _num_args, tyvar_names :: [Name]
    tyvar_names, ctxt :: [DType]
    ctxt, _arg_kis :: [DType]
    _arg_kis, res_ki :: DType
    res_ki)
                  <- OSet Name
    -> DType
    -> DType
    -> SgM (DType, Int, [Name], [DType], [DType], DType)
    singType OSet Name
    bound_kvs (Name -> DType
    promoteValRhs Name
    name) DType
    raw_ty
                (DType, [Name], [DType], DType)
    -> SgM (DType, [Name], [DType], DType)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DType
    s_ty, [Name]
    tyvar_names, [DType]
    ctxt, DType
    res_ki)

          (s_ty :: DType
    s_ty, tyvar_names :: [Name]
    tyvar_names, ctxt :: [DType]
    ctxt, m_res_ki :: Maybe DType
    m_res_ki) <- case Name -> OMap Name DType -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name DType
    inst_sigs of
            Just inst_sig :: DType
    inst_sig -> do
              -- We have an InstanceSig, so just single that type. Take care to
              -- avoid binding the variables bound by the instance head as well.
              let inst_bound :: OSet Name
    inst_bound = (DType -> OSet Name) -> [DType] -> OSet Name
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap DType -> OSet Name
    fvDType ([DType]
    cxt [DType] -> [DType] -> [DType]
    forall a. [a] -> [a] -> [a]
    ++ [DType]
    inst_kis)
              (s_ty :: DType
    s_ty, tyvar_names :: [Name]
    tyvar_names, ctxt :: [DType]
    ctxt, res_ki :: DType
    res_ki) <- OSet Name -> DType -> SgM (DType, [Name], [DType], DType)
    sing_meth_ty OSet Name
    inst_bound DType
    inst_sig
              (DType, [Name], [DType], Maybe DType)
    -> SgM (DType, [Name], [DType], Maybe DType)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DType
    s_ty, [Name]
    tyvar_names, [DType]
    ctxt, DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    res_ki)
            Nothing -> case Maybe DInfo
    mb_s_info of
              -- We don't have an InstanceSig, so we must compute the type to use
              -- in the singled instance ourselves through reification.
              Just (DVarI _ (DForallT cls_tvbs :: [DTyVarBndr]
    cls_tvbs _cls_pred :: [DType]
    _cls_pred s_ty :: DType
    s_ty) _) -> do
                let subst :: Map Name DType
    subst = [DTyVarBndr] -> Map Name DType
    mk_subst [DTyVarBndr]
    cls_tvbs
                    (sing_tvbs :: [DTyVarBndr]
    sing_tvbs, ctxt :: [DType]
    ctxt, _args :: [DType]
    _args, res_ty :: DType
    res_ty) = DType -> ([DTyVarBndr], [DType], [DType], DType)
    unravel DType
    s_ty
                    m_res_ki :: Maybe DType
    m_res_ki = case DType
    res_ty of
                      _sing :: DType
    _sing `DAppT` (_prom_func :: DType
    _prom_func `DSigT` res_ki :: DType
    res_ki) -> DType -> Maybe DType
    forall a. a -> Maybe a
    Just (Map Name DType -> DType -> DType
    substKind Map Name DType
    subst DType
    res_ki)
                      _                                         -> Maybe DType
    forall a. Maybe a
    Nothing

                (DType, [Name], [DType], Maybe DType)
    -> SgM (DType, [Name], [DType], Maybe DType)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ( Map Name DType -> DType -> DType
    substType Map Name DType
    subst DType
    s_ty
                     , (DTyVarBndr -> Name) -> [DTyVarBndr] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map DTyVarBndr -> Name
    extractTvbName [DTyVarBndr]
    sing_tvbs
                     , (DType -> DType) -> [DType] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (Map Name DType -> DType -> DType
    substType Map Name DType
    subst) [DType]
    ctxt
                     , Maybe DType
    m_res_ki )
              _ -> do
                Maybe DInfo
    mb_info <- Name -> SgM (Maybe DInfo)
    forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
    dsReify Name
    name
                case Maybe DInfo
    mb_info of
                  Just (DVarI _ (DForallT cls_tvbs :: [DTyVarBndr]
    cls_tvbs _cls_pred :: [DType]
    _cls_pred inner_ty :: DType
    inner_ty) _) -> do
                    let subst :: Map Name DType
    subst = [DTyVarBndr] -> Map Name DType
    mk_subst [DTyVarBndr]
    cls_tvbs
                        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]
    cls_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]
    cls_tvbs
                        cls_bound :: OSet Name
    cls_bound     = 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
                    (s_ty :: DType
    s_ty, tyvar_names :: [Name]
    tyvar_names, ctxt :: [DType]
    ctxt, res_ki :: DType
    res_ki) <- OSet Name -> DType -> SgM (DType, [Name], [DType], DType)
    sing_meth_ty OSet Name
    cls_bound DType
    inner_ty
                    (DType, [Name], [DType], Maybe DType)
    -> SgM (DType, [Name], [DType], Maybe DType)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ( Map Name DType -> DType -> DType
    substType Map Name DType
    subst DType
    s_ty
                         , [Name]
    tyvar_names
                         , [DType]
    ctxt
                         , DType -> Maybe DType
    forall a. a -> Maybe a
    Just (Map Name DType -> DType -> DType
    substKind Map Name DType
    subst DType
    res_ki) )
                  _ -> String -> SgM (DType, [Name], [DType], Maybe DType)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> SgM (DType, [Name], [DType], Maybe DType))
    -> String -> SgM (DType, [Name], [DType], Maybe DType)
    forall a b. (a -> b) -> a -> b
    $ "Cannot find type of method " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    forall a. Show a => a -> String
    show Name
    name

          let kind_map :: Map Name DType
    kind_map = Map Name DType
    -> (DType -> Map Name DType) -> Maybe DType -> Map Name DType
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Map Name DType
    forall k a. Map k a
    Map.empty (Name -> DType -> Map Name DType
    forall k a. k -> a -> Map k a
    Map.singleton Name
    name) Maybe DType
    m_res_ki
          DLetDec
    meth' <- Map Name [Name]
    -> Map Name [DType]
    -> Map Name DType
    -> Name
    -> LetDecRHS Annotated
    -> SgM DLetDec
    singLetDecRHS (Name -> [Name] -> Map Name [Name]
    forall k a. k -> a -> Map k a
    Map.singleton Name
    name [Name]
    tyvar_names)
                                 (Name -> [DType] -> Map Name [DType]
    forall k a. k -> a -> Map k a
    Map.singleton Name
    name [DType]
    ctxt)
                                 Map Name DType
    kind_map Name
    name LetDecRHS Annotated
    rhs
          [DDec] -> SgM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DDec] -> SgM [DDec]) -> [DDec] -> SgM [DDec]
    forall a b. (a -> b) -> a -> b
    $ (DLetDec -> DDec) -> [DLetDec] -> [DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map DLetDec -> DDec
    DLetDec [Name -> DType -> DLetDec
    DSigD (Name -> Name
    singValName Name
    name) DType
    s_ty, DLetDec
    meth']

    singLetDecEnv :: ALetDecEnv
                  -> SgM a
                  -> SgM ([DLetDec], [DDec], a)
                     -- Return:
                     --
                     -- 1. The singled let-decs
                     -- 2. SingI instances for any defunctionalization symbols
                     --    (see Data.Singletons.Single.Defun)
                     -- 3. The result of running the `SgM a` action
    singLetDecEnv :: ALetDecEnv -> SgM a -> SgM ([DLetDec], [DDec], a)
    singLetDecEnv (LetDecEnv { lde_defns :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> OMap Name (LetDecRHS ann)
    lde_defns     = OMap Name (LetDecRHS Annotated)
    defns
                             , lde_types :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name DType
    lde_types     = OMap Name DType
    types
                             , lde_infix :: forall (ann :: AnnotationFlag). LetDecEnv ann -> OMap Name Fixity
    lde_infix     = OMap Name Fixity
    infix_decls
                             , lde_proms :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> IfAnn ann (OMap Name DType) ()
    lde_proms     = IfAnn Annotated (OMap Name DType) ()
    proms
                             , lde_bound_kvs :: forall (ann :: AnnotationFlag).
    LetDecEnv ann -> IfAnn ann (OMap Name (OSet Name)) ()
    lde_bound_kvs = IfAnn Annotated (OMap Name (OSet Name)) ()
    bound_kvs })
                  thing_inside :: SgM a
    thing_inside = do
      let prom_list :: [LetBind]
    prom_list = OMap Name DType -> [LetBind]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name DType
    IfAnn Annotated (OMap Name DType) ()
    proms
      (typeSigs :: [DLetDec]
    typeSigs, letBinds :: [(Name, DExp)]
    letBinds, tyvarNames :: [(Name, [Name])]
    tyvarNames, cxts :: [(Name, [DType])]
    cxts, res_kis :: [Maybe DType]
    res_kis, singIDefunss :: [[DDec]]
    singIDefunss)
        <- [(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
      Maybe DType, [DDec])]
    -> ([DLetDec], [(Name, DExp)], [(Name, [Name])], [(Name, [DType])],
        [Maybe DType], [[DDec]])
    forall a b c d e f.
    [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])
    unzip6 ([(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
       Maybe DType, [DDec])]
     -> ([DLetDec], [(Name, DExp)], [(Name, [Name])], [(Name, [DType])],
         [Maybe DType], [[DDec]]))
    -> SgM
         [(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec])]
    -> SgM
         ([DLetDec], [(Name, DExp)], [(Name, [Name])], [(Name, [DType])],
          [Maybe DType], [[DDec]])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (LetBind
     -> SgM
          (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec]))
    -> [LetBind]
    -> SgM
         [(DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec])]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Name
     -> DType
     -> SgM
          (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
           Maybe DType, [DDec]))
    -> LetBind
    -> SgM
         (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
          Maybe DType, [DDec])
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (OMap Name (LetDecRHS Annotated)
    -> OMap Name DType
    -> OMap Name (OSet Name)
    -> Name
    -> DType
    -> SgM
         (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
          Maybe DType, [DDec])
    singTySig OMap Name (LetDecRHS Annotated)
    defns OMap Name DType
    types OMap Name (OSet Name)
    IfAnn Annotated (OMap Name (OSet Name)) ()
    bound_kvs)) [LetBind]
    prom_list
      [DLetDec]
    infix_decls' <- ((Name, Fixity) -> SgM DLetDec)
    -> [(Name, Fixity)] -> SgM [DLetDec]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Name -> Fixity -> SgM DLetDec) -> (Name, Fixity) -> SgM DLetDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Fixity -> SgM DLetDec
    forall (q :: * -> *). DsMonad q => Name -> Fixity -> q DLetDec
    singInfixDecl) ([(Name, Fixity)] -> SgM [DLetDec])
    -> [(Name, Fixity)] -> SgM [DLetDec]
    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
      let res_ki_map :: Map Name DType
    res_ki_map = [LetBind] -> Map Name DType
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Name
    name, DType
    res_ki) | ((name :: Name
    name, _), Just res_ki :: DType
    res_ki)
                                                         <- [LetBind] -> [Maybe DType] -> [(LetBind, Maybe DType)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [LetBind]
    prom_list [Maybe DType]
    res_kis ]
      [(Name, DExp)]
    -> SgM ([DLetDec], [DDec], a) -> SgM ([DLetDec], [DDec], a)
    forall a. [(Name, DExp)] -> SgM a -> SgM a
    bindLets [(Name, DExp)]
    letBinds (SgM ([DLetDec], [DDec], a) -> SgM ([DLetDec], [DDec], a))
    -> SgM ([DLetDec], [DDec], a) -> SgM ([DLetDec], [DDec], a)
    forall a b. (a -> b) -> a -> b
    $ do
        [DLetDec]
    let_decs <- ((Name, LetDecRHS Annotated) -> SgM DLetDec)
    -> [(Name, LetDecRHS Annotated)] -> SgM [DLetDec]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((Name -> LetDecRHS Annotated -> SgM DLetDec)
    -> (Name, LetDecRHS Annotated) -> SgM DLetDec
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (Map Name [Name]
    -> Map Name [DType]
    -> Map Name DType
    -> Name
    -> LetDecRHS Annotated
    -> SgM DLetDec
    singLetDecRHS ([(Name, [Name])] -> Map Name [Name]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, [Name])]
    tyvarNames)
                                                 ([(Name, [DType])] -> Map Name [DType]
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [(Name, [DType])]
    cxts)
                                                 Map Name DType
    res_ki_map))
                         (OMap Name (LetDecRHS Annotated) -> [(Name, LetDecRHS Annotated)]
    forall k v. OMap k v -> [(k, v)]
    OMap.assocs OMap Name (LetDecRHS Annotated)
    defns)
        a
    thing <- SgM a
    thing_inside
        ([DLetDec], [DDec], a) -> SgM ([DLetDec], [DDec], a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([DLetDec]
    infix_decls' [DLetDec] -> [DLetDec] -> [DLetDec]
    forall a. [a] -> [a] -> [a]
    ++ [DLetDec]
    typeSigs [DLetDec] -> [DLetDec] -> [DLetDec]
    forall a. [a] -> [a] -> [a]
    ++ [DLetDec]
    let_decs, [[DDec]] -> [DDec]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[DDec]]
    singIDefunss, a
    thing)

    singTySig :: OMap Name ALetDecRHS  -- definitions
              -> OMap Name DType       -- type signatures
              -> OMap Name (OSet Name) -- bound kind variables
              -> Name -> DType   -- the type is the promoted type, not the type sig!
              -> SgM ( DLetDec               -- the new type signature
                     , (Name, DExp)          -- the let-bind entry
                     , (Name, [Name])        -- the scoped tyvar names in the tysig
                     , (Name, DCxt)          -- the context of the type signature
                     , Maybe DKind           -- the result kind in the tysig
                     , [DDec]                -- SingI instances for defun symbols
                     )
    singTySig :: OMap Name (LetDecRHS Annotated)
    -> OMap Name DType
    -> OMap Name (OSet Name)
    -> Name
    -> DType
    -> SgM
         (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
          Maybe DType, [DDec])
    singTySig defns :: OMap Name (LetDecRHS Annotated)
    defns types :: OMap Name DType
    types bound_kvs :: OMap Name (OSet Name)
    bound_kvs name :: Name
    name prom_ty :: DType
    prom_ty =
      let sName :: Name
    sName = Name -> Name
    singValName Name
    name in
      case Name -> OMap Name DType -> Maybe DType
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name DType
    types of
        Nothing -> do
          Int
    num_args <- SgM Int
    guess_num_args
          (sty :: DType
    sty, tyvar_names :: [Name]
    tyvar_names) <- Int -> SgM (DType, [Name])
    mk_sing_ty Int
    num_args
          [DDec]
    singIDefuns <- Name
    -> NameSpace
    -> [DType]
    -> [Maybe DType]
    -> Maybe DType
    -> SgM [DDec]
    singDefuns Name
    name NameSpace
    VarName []
                                    ((Name -> Maybe DType) -> [Name] -> [Maybe DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe DType -> Name -> Maybe DType
    forall a b. a -> b -> a
    const Maybe DType
    forall a. Maybe a
    Nothing) [Name]
    tyvar_names) Maybe DType
    forall a. Maybe a
    Nothing
          (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
     Maybe DType, [DDec])
    -> SgM
         (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
          Maybe DType, [DDec])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( Name -> DType -> DLetDec
    DSigD Name
    sName DType
    sty
                 , (Name
    name, Int -> DType -> DExp -> DExp
    wrapSingFun Int
    num_args DType
    prom_ty (Name -> DExp
    DVarE Name
    sName))
                 , (Name
    name, [Name]
    tyvar_names)
                 , (Name
    name, [])
                 , Maybe DType
    forall a. Maybe a
    Nothing
                 , [DDec]
    singIDefuns )
        Just ty :: DType
    ty -> do
          OSet Name
    all_bound_kvs <- SgM (OSet Name)
    lookup_bound_kvs
          (sty :: DType
    sty, num_args :: Int
    num_args, tyvar_names :: [Name]
    tyvar_names, ctxt :: [DType]
    ctxt, arg_kis :: [DType]
    arg_kis, res_ki :: DType
    res_ki)
            <- OSet Name
    -> DType
    -> DType
    -> SgM (DType, Int, [Name], [DType], [DType], DType)
    singType OSet Name
    all_bound_kvs DType
    prom_ty DType
    ty
          [DType]
    bound_cxt <- SgM [DType]
    askContext
          [DDec]
    singIDefuns <- Name
    -> NameSpace
    -> [DType]
    -> [Maybe DType]
    -> Maybe DType
    -> SgM [DDec]
    singDefuns Name
    name NameSpace
    VarName ([DType]
    bound_cxt [DType] -> [DType] -> [DType]
    forall a. [a] -> [a] -> [a]
    ++ [DType]
    ctxt)
                                    ((DType -> Maybe DType) -> [DType] -> [Maybe DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DType -> Maybe DType
    forall a. a -> Maybe a
    Just [DType]
    arg_kis) (DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    res_ki)
          (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
     Maybe DType, [DDec])
    -> SgM
         (DLetDec, (Name, DExp), (Name, [Name]), (Name, [DType]),
          Maybe DType, [DDec])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( Name -> DType -> DLetDec
    DSigD Name
    sName DType
    sty
                 , (Name
    name, Int -> DType -> DExp -> DExp
    wrapSingFun Int
    num_args DType
    prom_ty (Name -> DExp
    DVarE Name
    sName))
                 , (Name
    name, [Name]
    tyvar_names)
                 , (Name
    name, [DType]
    ctxt)
                 , DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    res_ki
                 , [DDec]
    singIDefuns )
      where
        guess_num_args :: SgM Int
        guess_num_args :: SgM Int
    guess_num_args =
          case Name
    -> OMap Name (LetDecRHS Annotated) -> Maybe (LetDecRHS Annotated)
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name (LetDecRHS Annotated)
    defns of
            Nothing -> String -> SgM Int
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Internal error: promotion known for something not let-bound."
            Just (AValue _ n _) -> Int -> SgM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    n
            Just (AFunction _ n _) -> Int -> SgM Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    n

        lookup_bound_kvs :: SgM (OSet Name)
        lookup_bound_kvs :: SgM (OSet Name)
    lookup_bound_kvs =
          case Name -> OMap Name (OSet Name) -> Maybe (OSet Name)
    forall k v. Ord k => k -> OMap k v -> Maybe v
    OMap.lookup Name
    name OMap Name (OSet Name)
    bound_kvs of
            Nothing -> String -> SgM (OSet Name)
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> SgM (OSet Name)) -> String -> SgM (OSet Name)
    forall a b. (a -> b) -> a -> b
    $ "Internal error: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Name -> String
    nameBase Name
    name String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " has no type variable "
                              String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "bindings, despite having a type signature"
            Just kvs :: OSet Name
    kvs -> OSet Name -> SgM (OSet Name)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure OSet Name
    kvs

          -- create a Sing t1 -> Sing t2 -> ... type of a given arity and result type
        mk_sing_ty :: Int -> SgM (DType, [Name])
        mk_sing_ty :: Int -> SgM (DType, [Name])
    mk_sing_ty n :: Int
    n = do
          [Name]
    arg_names <- Int -> SgM Name -> SgM [Name]
    forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
    replicateM Int
    n (String -> SgM Name
    forall (m :: * -> *). Quasi m => String -> m Name
    qNewName "arg")
          (DType, [Name]) -> SgM (DType, [Name])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ( [DTyVarBndr] -> [DType] -> DType -> DType
    DForallT ((Name -> DTyVarBndr) -> [Name] -> [DTyVarBndr]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DTyVarBndr
    DPlainTV [Name]
    arg_names) []
                            ([DType] -> DType -> DType
    ravel ((Name -> DType) -> [Name] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map (\nm :: Name
    nm -> DType
    singFamily DType -> DType -> DType
    `DAppT` Name -> DType
    DVarT Name
    nm) [Name]
    arg_names)
                                   (DType
    singFamily DType -> DType -> DType
    `DAppT`
                                        ((DType -> DType -> DType) -> DType -> [DType] -> DType
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl DType -> DType -> DType
    apply DType
    prom_ty ((Name -> DType) -> [Name] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    arg_names))))
                 , [Name]
    arg_names )

    singLetDecRHS :: Map Name [Name]
                  -> Map Name DCxt    -- the context of the type signature
                                      -- (might not be known)
                  -> Map Name DKind   -- result kind (might not be known)
                  -> Name -> ALetDecRHS -> SgM DLetDec
    singLetDecRHS :: Map Name [Name]
    -> Map Name [DType]
    -> Map Name DType
    -> Name
    -> LetDecRHS Annotated
    -> SgM DLetDec
    singLetDecRHS bound_names :: Map Name [Name]
    bound_names cxts :: Map Name [DType]
    cxts res_kis :: Map Name DType
    res_kis name :: Name
    name ld_rhs :: LetDecRHS Annotated
    ld_rhs =
      [DType] -> SgM DLetDec -> SgM DLetDec
    forall a. [DType] -> SgM a -> SgM a
    bindContext ([DType] -> Name -> Map Name [DType] -> [DType]
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault [] Name
    name Map Name [DType]
    cxts) (SgM DLetDec -> SgM DLetDec) -> SgM DLetDec -> SgM DLetDec
    forall a b. (a -> b) -> a -> b
    $
        case LetDecRHS Annotated
    ld_rhs of
          AValue prom num_arrows exp ->
            DPat -> DExp -> DLetDec
    DValD (Name -> DPat
    DVarP (Name -> Name
    singValName Name
    name)) (DExp -> DLetDec) -> SgM DExp -> SgM DLetDec
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
            (Int -> DType -> DExp -> DExp
    wrapUnSingFun Int
    num_arrows DType
    prom (DExp -> DExp) -> SgM DExp -> SgM DExp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp (Name -> Map Name DType -> Maybe DType
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    name Map Name DType
    res_kis))
          AFunction prom_fun num_arrows clauses ->
            let tyvar_names :: [Name]
    tyvar_names = case Name -> Map Name [Name] -> Maybe [Name]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    name Map Name [Name]
    bound_names of
                                Nothing -> []
                                Just ns :: [Name]
    ns -> [Name]
    ns
                res_ki :: Maybe DType
    res_ki = Name -> Map Name DType -> Maybe DType
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    name Map Name DType
    res_kis
            in
            Name -> [DClause] -> DLetDec
    DFunD (Name -> Name
    singValName Name
    name) ([DClause] -> DLetDec) -> SgM [DClause] -> SgM DLetDec
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                  (ADClause -> SgM DClause) -> [ADClause] -> SgM [DClause]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (DType -> Int -> [Name] -> Maybe DType -> ADClause -> SgM DClause
    singClause DType
    prom_fun Int
    num_arrows [Name]
    tyvar_names Maybe DType
    res_ki) [ADClause]
    clauses

    singClause :: DType   -- the promoted function
               -> Int     -- the number of arrows in the type. If this is more
                          -- than the number of patterns, we need to eta-expand
                          -- with unSingFun.
               -> [Name]  -- the names of the forall'd vars in the type sig of this
                          -- function. This list should have at least the length as the
                          -- number of patterns in the clause
               -> Maybe DKind   -- result kind, if known
               -> ADClause -> SgM DClause
    singClause :: DType -> Int -> [Name] -> Maybe DType -> ADClause -> SgM DClause
    singClause prom_fun :: DType
    prom_fun num_arrows :: Int
    num_arrows bound_names :: [Name]
    bound_names res_ki :: Maybe DType
    res_ki
               (ADClause var_proms :: VarPromotions
    var_proms pats :: [ADPat]
    pats exp :: ADExp
    exp) = do

      -- Fix #166:
      Bool -> SgM () -> SgM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Int
    num_arrows Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [ADPat] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ADPat]
    pats Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < 0) (SgM () -> SgM ()) -> SgM () -> SgM ()
    forall a b. (a -> b) -> a -> b
    $
        String -> SgM ()
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail (String -> SgM ()) -> String -> SgM ()
    forall a b. (a -> b) -> a -> b
    $ "Function being promoted to " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Type -> String
    forall a. Ppr a => a -> String
    pprint (DType -> Type
    typeToTH DType
    prom_fun)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++
               " has too many arguments."

      (sPats :: [DPat]
    sPats, sigPaExpsSigs :: SingDSigPaInfos
    sigPaExpsSigs) <- QWithAux SingDSigPaInfos SgM [DPat]
    -> SgM ([DPat], SingDSigPaInfos)
    forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
    evalForPair (QWithAux SingDSigPaInfos SgM [DPat]
     -> SgM ([DPat], SingDSigPaInfos))
    -> QWithAux SingDSigPaInfos SgM [DPat]
    -> SgM ([DPat], SingDSigPaInfos)
    forall a b. (a -> b) -> a -> b
    $ (ADPat -> QWithAux SingDSigPaInfos SgM DPat)
    -> [ADPat] -> QWithAux SingDSigPaInfos SgM [DPat]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Map Name Name -> ADPat -> QWithAux SingDSigPaInfos SgM DPat
    singPat (VarPromotions -> Map Name Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList VarPromotions
    var_proms)) [ADPat]
    pats
      DExp
    sBody <- ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp Maybe DType
    res_ki
        -- when calling unSingFun, the promoted pats aren't in scope, so we use the
        -- bound_names instead
      let pattern_bound_names :: [Name]
    pattern_bound_names = (Name -> ADPat -> Name) -> [Name] -> [ADPat] -> [Name]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith Name -> ADPat -> Name
    forall a b. a -> b -> a
    const [Name]
    bound_names [ADPat]
    pats
           -- this does eta-expansion. See comment at top of file.
          sBody' :: DExp
    sBody' = Int -> DType -> DExp -> DExp
    wrapUnSingFun (Int
    num_arrows Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [ADPat] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ADPat]
    pats)
                     ((DType -> DType -> DType) -> DType -> [DType] -> DType
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl DType -> DType -> DType
    apply DType
    prom_fun ((Name -> DType) -> [Name] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DType
    DVarT [Name]
    pattern_bound_names)) DExp
    sBody
      DClause -> SgM DClause
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DClause -> SgM DClause) -> DClause -> SgM DClause
    forall a b. (a -> b) -> a -> b
    $ [DPat] -> DExp -> DClause
    DClause [DPat]
    sPats (DExp -> DClause) -> DExp -> DClause
    forall a b. (a -> b) -> a -> b
    $ SingDSigPaInfos -> DExp -> DExp
    mkSigPaCaseE SingDSigPaInfos
    sigPaExpsSigs DExp
    sBody'

    singPat :: Map Name Name   -- from term-level names to type-level names
            -> ADPat
            -> QWithAux SingDSigPaInfos SgM DPat
    singPat :: Map Name Name -> ADPat -> QWithAux SingDSigPaInfos SgM DPat
    singPat var_proms :: Map Name Name
    var_proms = ADPat -> QWithAux SingDSigPaInfos SgM DPat
    go
      where
        go :: ADPat -> QWithAux SingDSigPaInfos SgM DPat
        go :: ADPat -> QWithAux SingDSigPaInfos SgM DPat
    go (ADLitP _lit :: Lit
    _lit) =
          String -> QWithAux SingDSigPaInfos SgM DPat
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Singling of literal patterns not yet supported"
        go (ADVarP name :: Name
    name) = do
          Name
    tyname <- case Name -> Map Name Name -> Maybe Name
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    name Map Name Name
    var_proms of
                      Nothing     ->
                        String -> QWithAux SingDSigPaInfos SgM Name
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail "Internal error: unknown variable when singling pattern"
                      Just tyname :: Name
    tyname -> Name -> QWithAux SingDSigPaInfos SgM Name
    forall (m :: * -> *) a. Monad m => a -> m a
    return Name
    tyname
          DPat -> QWithAux SingDSigPaInfos SgM DPat
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DPat -> QWithAux SingDSigPaInfos SgM DPat)
    -> DPat -> QWithAux SingDSigPaInfos SgM DPat
    forall a b. (a -> b) -> a -> b
    $ Name -> DPat
    DVarP (Name -> Name
    singValName Name
    name) DPat -> DType -> DPat
    `DSigP` (DType
    singFamily DType -> DType -> DType
    `DAppT` Name -> DType
    DVarT Name
    tyname)
        go (ADConP name :: Name
    name pats :: [ADPat]
    pats) = Name -> [DPat] -> DPat
    DConP (Name -> Name
    singDataConName Name
    name) ([DPat] -> DPat)
    -> QWithAux SingDSigPaInfos SgM [DPat]
    -> QWithAux SingDSigPaInfos SgM DPat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (ADPat -> QWithAux SingDSigPaInfos SgM DPat)
    -> [ADPat] -> QWithAux SingDSigPaInfos SgM [DPat]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ADPat -> QWithAux SingDSigPaInfos SgM DPat
    go [ADPat]
    pats
        go (ADTildeP pat :: ADPat
    pat) = do
          String -> QWithAux SingDSigPaInfos SgM ()
    forall (q :: * -> *). Quasi q => String -> q ()
    qReportWarning
            "Lazy pattern converted into regular pattern during singleton generation."
          ADPat -> QWithAux SingDSigPaInfos SgM DPat
    go ADPat
    pat
        go (ADBangP pat :: ADPat
    pat) = DPat -> DPat
    DBangP (DPat -> DPat)
    -> QWithAux SingDSigPaInfos SgM DPat
    -> QWithAux SingDSigPaInfos SgM DPat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ADPat -> QWithAux SingDSigPaInfos SgM DPat
    go ADPat
    pat
        go (ADSigP prom_pat :: DType
    prom_pat pat :: ADPat
    pat ty :: DType
    ty) = do
          DPat
    pat' <- ADPat -> QWithAux SingDSigPaInfos SgM DPat
    go ADPat
    pat
          -- Normally, calling dPatToDExp would be dangerous, since it fails if the
          -- supplied pattern contains any wildcard patterns. However, promotePat
          -- (which produced the pattern we're passing into dPatToDExp) maintains
          -- an invariant that any promoted pattern signatures will be free of
          -- wildcard patterns in the underlying pattern.
          -- See Note [Singling pattern signatures].
          (DExp, DType) -> QWithAux SingDSigPaInfos SgM ()
    forall (q :: * -> *) elt. Quasi q => elt -> QWithAux [elt] q ()
    addElement (DPat -> DExp
    dPatToDExp DPat
    pat', DType -> DType -> DType
    DSigT DType
    prom_pat DType
    ty)
          DPat -> QWithAux SingDSigPaInfos SgM DPat
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure DPat
    pat'
        go ADWildP = DPat -> QWithAux SingDSigPaInfos SgM DPat
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure DPat
    DWildP

    -- | If given a non-empty list of 'SingDSigPaInfos', construct a case expression
    -- that brings singleton equality constraints into scope via pattern-matching.
    -- See @Note [Singling pattern signatures]@.
    mkSigPaCaseE :: SingDSigPaInfos -> DExp -> DExp
    mkSigPaCaseE :: SingDSigPaInfos -> DExp -> DExp
    mkSigPaCaseE exps_with_sigs :: SingDSigPaInfos
    exps_with_sigs exp :: DExp
    exp
      | SingDSigPaInfos -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null SingDSigPaInfos
    exps_with_sigs = DExp
    exp
      | Bool
    otherwise =
          let (exps :: [DExp]
    exps, sigs :: [DType]
    sigs) = SingDSigPaInfos -> ([DExp], [DType])
    forall a b. [(a, b)] -> ([a], [b])
    unzip SingDSigPaInfos
    exps_with_sigs
              scrutinee :: DExp
    scrutinee = [DExp] -> DExp
    mkTupleDExp [DExp]
    exps
              pats :: [DPat]
    pats = (DType -> DPat) -> [DType] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map (DPat -> DType -> DPat
    DSigP DPat
    DWildP (DType -> DPat) -> (DType -> DType) -> DType -> DPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . DType -> DType -> DType
    DAppT (Name -> DType
    DConT Name
    singFamilyName)) [DType]
    sigs
          in DExp -> [DMatch] -> DExp
    DCaseE DExp
    scrutinee [DPat -> DExp -> DMatch
    DMatch ([DPat] -> DPat
    mkTupleDPat [DPat]
    pats) DExp
    exp]

    -- Note [Annotate case return type]
    -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    --
    -- We're straining GHC's type inference here. One particular trouble area
    -- is determining the return type of a GADT pattern match. In general, GHC
    -- cannot infer return types of GADT pattern matches because the return type
    -- becomes "untouchable" in the case matches. See the OutsideIn paper. But,
    -- during singletonization, we *know* the return type. So, just add a type
    -- annotation. See #54.
    --
    -- In particular, we add a type annotation in a somewhat unorthodox fashion.
    -- Instead of the usual `(x :: t)`, we use `id @t x`. See
    -- Note [The id hack; or, how singletons learned to stop worrying and avoid
    -- kind generalization] for an explanation of why we do this.

    -- Note [Why error is so special]
    -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    -- Some of the transformations that happen before this point produce impossible
    -- case matches. We must be careful when processing these so as not to make
    -- an error GHC will complain about. When binding the case-match variables, we
    -- normally include an equality constraint saying that the scrutinee is equal
    -- to the matched pattern. But, we can't do this in inaccessible matches, because
    -- equality is bogus, and GHC (rightly) complains. However, we then have another
    -- problem, because GHC doesn't have enough information when type-checking the
    -- RHS of the inaccessible match to deem it type-safe. The solution: treat error
    -- as super-special, so that GHC doesn't look too hard at singletonized error
    -- calls. Specifically, DON'T do the applySing stuff. Just use sError, which
    -- has a custom type (Sing x -> a) anyway.

    -- Note [Singling pattern signatures]
    -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    -- We want to single a pattern signature, like so:
    --
    --   f :: Maybe a -> a
    --   f (Just x :: Maybe a) = x
    --
    -- Naïvely, one might expect this to single straightfowardly as:
    --
    --   sF :: forall (z :: Maybe a). Sing z -> Sing (F z)
    --   sF (SJust sX :: Sing (Just x :: Maybe a)) = sX
    --
    -- But the way GHC typechecks patterns prevents this from working, as GHC won't
    -- know that the type `z` is actually `Just x` until /after/ the entirety of
    -- the `SJust sX` pattern has been typechecked. (See Trac #12018 for an
    -- extended discussion on this topic.)
    --
    -- To work around this design, we resort to a somewhat unsightly trick:
    -- immediately after matching on all the patterns, we perform a case on every
    -- pattern with a pattern signature, like so:
    --
    --   sF :: forall (z :: Maybe a). Sing z -> Sing (F z)
    --   sF (SJust sX :: Sing z)
    --     = case (SJust sX :: Sing z) of
    --         (_ :: Sing (Just x :: Maybe a)) -> sX
    --
    -- Now GHC accepts the fact that `z` is `Just x`, and all is well. In order
    -- to support this construction, the type of singPat is augmented with some
    -- extra information in the form of SingDSigPaInfos:
    --
    --   type SingDSigPaInfos = [(DExp, DType)]
    --
    -- Where the DExps corresponds to the expressions we case on just after the
    -- patterns (`SJust sX :: Sing x`, in the example above), and the DTypes
    -- correspond to the singled pattern signatures to use in the case alternative
    -- (`Sing (Just x :: Maybe a)` in the example above). singPat appends to the
    -- list of SingDSigPaInfos whenever it processes a DSigPa (pattern signature),
    -- and call sites can pass these SingDSigPaInfos to mkSigPaCaseE to construct a
    -- case expression like the one featured above.
    --
    -- Some interesting consequences of this design:
    --
    -- 1. We must promote DPats to ADPats, a variation of DPat where the annotated
    --    DSigPa counterpart, ADSigPa, stores the type that the original DPat was
    --    promoted to. This is necessary since promoting the type might have
    --    generated fresh variable names, so we need to be able to use the same
    --    names when singling.
    --
    -- 2. Also when promoting a DSigPa to an ADSigPa, we remove any wildcards from
    --    the underlying pattern. To see why this is necessary, consider singling
    --    this example:
    --
    --      g (Just _ :: Maybe a) = "hi"
    --
    --    This must single to something like this:
    --
    --      sG (SJust _ :: Sing z)
    --        = case (SJust _ :: Sing z) of
    --            (_ :: Sing (Just _ :: Maybe a)) -> "hi"
    --
    --    But `SJust _` is not a valid expression, and since the minimal th-desugar
    --    AST lacks as-patterns, we can't replace it with something like
    --    `sG x@(SJust _ :: Sing z) = case x of ...`. But even if the th-desugar
    --    AST /did/ have as-patterns, we'd still be in trouble, as `Just _` isn't
    --    a valid type without the use of -XPartialTypeSignatures, which isn't a
    --    design we want to force upon others.
    --
    --    We work around both issues by simply converting all wildcard patterns
    --    from the pattern that has a signature. That means our example becomes:
    --
    --      sG (SJust sWild :: Sing z)
    --        = case (SJust sWild :: Sing z) of
    --            (_ :: Sing (Just wild :: Maybe a)) -> "hi"
    --
    --    And now everything is hunky-dory.

    singExp :: ADExp -> Maybe DKind   -- the kind of the expression, if known
            -> SgM DExp
      -- See Note [Why error is so special]
    singExp :: ADExp -> Maybe DType -> SgM DExp
    singExp (ADVarE err :: Name
    err `ADAppE` arg :: ADExp
    arg) _res_ki :: Maybe DType
    _res_ki
      | Name
    err Name -> Name -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name
    errorName = DExp -> DExp -> DExp
    DAppE (Name -> DExp
    DVarE (Name -> Name
    singValName Name
    err)) (DExp -> DExp) -> SgM DExp -> SgM DExp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
                           ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    arg (DType -> Maybe DType
    forall a. a -> Maybe a
    Just (Name -> DType
    DConT Name
    symbolName))
    singExp (ADVarE name :: Name
    name) _res_ki :: Maybe DType
    _res_ki = Name -> SgM DExp
    lookupVarE Name
    name
    singExp (ADConE name :: Name
    name) _res_ki :: Maybe DType
    _res_ki = Name -> SgM DExp
    lookupConE Name
    name
    singExp (ADLitE lit :: Lit
    lit)  _res_ki :: Maybe DType
    _res_ki = Lit -> SgM DExp
    singLit Lit
    lit
    singExp (ADAppE e1 :: ADExp
    e1 e2 :: ADExp
    e2) _res_ki :: Maybe DType
    _res_ki = do
      DExp
    e1' <- ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    e1 Maybe DType
    forall a. Maybe a
    Nothing
      DExp
    e2' <- ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    e2 Maybe DType
    forall a. Maybe a
    Nothing
      -- `applySing undefined x` kills type inference, because GHC can't figure
      -- out the type of `undefined`. So we don't emit `applySing` there.
      if DExp -> Bool
    isException DExp
    e1'
      then DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ DExp
    e1' DExp -> DExp -> DExp
    `DAppE` DExp
    e2'
      else DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ (Name -> DExp
    DVarE Name
    applySingName) DExp -> DExp -> DExp
    `DAppE` DExp
    e1' DExp -> DExp -> DExp
    `DAppE` DExp
    e2'
    singExp (ADLamE ty_names :: [Name]
    ty_names prom_lam :: DType
    prom_lam names :: [Name]
    names exp :: ADExp
    exp) _res_ki :: Maybe DType
    _res_ki = do
      let sNames :: [Name]
    sNames = (Name -> Name) -> [Name] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Name
    singValName [Name]
    names
      DExp
    exp' <- ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp Maybe DType
    forall a. Maybe a
    Nothing
      -- we need to bind the type variables... but DLamE doesn't allow SigT patterns.
      -- So: build a case
      let caseExp :: DExp
    caseExp = DExp -> [DMatch] -> DExp
    DCaseE ([DExp] -> DExp
    mkTupleDExp ((Name -> DExp) -> [Name] -> [DExp]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> DExp
    DVarE [Name]
    sNames))
                           [DPat -> DExp -> DMatch
    DMatch ([DPat] -> DPat
    mkTupleDPat
                                    ((Name -> DPat) -> [Name] -> [DPat]
    forall a b. (a -> b) -> [a] -> [b]
    map ((DPat
    DWildP DPat -> DType -> DPat
    `DSigP`) (DType -> DPat) -> (Name -> DType) -> Name -> DPat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                                          (DType
    singFamily DType -> DType -> DType
    `DAppT`) (DType -> DType) -> (Name -> DType) -> Name -> DType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
                                          Name -> DType
    DVarT) [Name]
    ty_names)) DExp
    exp']
      DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ Int -> DType -> DExp -> DExp
    wrapSingFun ([Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Name]
    names) DType
    prom_lam (DExp -> DExp) -> DExp -> DExp
    forall a b. (a -> b) -> a -> b
    $ [Name] -> DExp -> DExp
    DLamE [Name]
    sNames DExp
    caseExp
    singExp (ADCaseE exp :: ADExp
    exp matches :: [ADMatch]
    matches ret_ty :: DType
    ret_ty) res_ki :: Maybe DType
    res_ki =
        -- See Note [Annotate case return type] and
        --     Note [The id hack; or, how singletons learned to stop worrying and
        --           avoid kind generalization]
      DExp -> DExp -> DExp
    DAppE (DExp -> DType -> DExp
    DAppTypeE (Name -> DExp
    DVarE 'id)
                       (DType
    singFamily DType -> DType -> DType
    `DAppT` (DType
    ret_ty DType -> Maybe DType -> DType
    `maybeSigT` Maybe DType
    res_ki)))
        (DExp -> DExp) -> SgM DExp -> SgM DExp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (DExp -> [DMatch] -> DExp
    DCaseE (DExp -> [DMatch] -> DExp) -> SgM DExp -> SgM ([DMatch] -> DExp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp Maybe DType
    forall a. Maybe a
    Nothing SgM ([DMatch] -> DExp) -> SgM [DMatch] -> SgM DExp
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (ADMatch -> SgM DMatch) -> [ADMatch] -> SgM [DMatch]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe DType -> ADMatch -> SgM DMatch
    singMatch Maybe DType
    res_ki) [ADMatch]
    matches)
    singExp (ADLetE env :: ALetDecEnv
    env exp :: ADExp
    exp) res_ki :: Maybe DType
    res_ki = do
      -- We intentionally discard the SingI instances for exp's defunctionalization
      -- symbols, as we also do not generate the declarations for the
      -- defunctionalization symbols in the first place during promotion.
      (let_decs :: [DLetDec]
    let_decs, _, exp' :: DExp
    exp') <- ALetDecEnv -> SgM DExp -> SgM ([DLetDec], [DDec], DExp)
    forall a. ALetDecEnv -> SgM a -> SgM ([DLetDec], [DDec], a)
    singLetDecEnv ALetDecEnv
    env (SgM DExp -> SgM ([DLetDec], [DDec], DExp))
    -> SgM DExp -> SgM ([DLetDec], [DDec], DExp)
    forall a b. (a -> b) -> a -> b
    $ ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp Maybe DType
    res_ki
      DExp -> SgM DExp
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ [DLetDec] -> DExp -> DExp
    DLetE [DLetDec]
    let_decs DExp
    exp'
    singExp (ADSigE prom_exp :: DType
    prom_exp exp :: ADExp
    exp ty :: DType
    ty) _ = do
      DExp
    exp' <- ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp (DType -> Maybe DType
    forall a. a -> Maybe a
    Just DType
    ty)
      DExp -> SgM DExp
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ DExp -> DType -> DExp
    DSigE DExp
    exp' (DType -> DExp) -> DType -> DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> DType
    DConT Name
    singFamilyName DType -> DType -> DType
    `DAppT` DType -> DType -> DType
    DSigT DType
    prom_exp DType
    ty

    -- See Note [DerivedDecl] in Data.Singletons.Syntax
    singDerivedEqDecs :: DerivedEqDecl -> SgM [DDec]
    singDerivedEqDecs :: DerivedEqDecl -> SgM [DDec]
    singDerivedEqDecs (DerivedDecl { ded_mb_cxt :: forall (cls :: * -> Constraint). DerivedDecl cls -> Maybe [DType]
    ded_mb_cxt     = Maybe [DType]
    mb_ctxt
                                   , ded_type :: forall (cls :: * -> Constraint). DerivedDecl cls -> DType
    ded_type       = DType
    ty
                                   , ded_type_tycon :: forall (cls :: * -> Constraint). DerivedDecl cls -> Name
    ded_type_tycon = Name
    ty_tycon
                                   , ded_decl :: forall (cls :: * -> Constraint). DerivedDecl cls -> DataDecl
    ded_decl       = DataDecl _ _ cons :: [DCon]
    cons }) = do
      (scons :: [DCon]
    scons, _) <- [Dec] -> SgM [DCon] -> SgM ([DCon], [DDec])
    forall (q :: * -> *) a.
    DsMonad q =>
    [Dec] -> SgM a -> q (a, [DDec])
    singM [] (SgM [DCon] -> SgM ([DCon], [DDec]))
    -> SgM [DCon] -> SgM ([DCon], [DDec])
    forall a b. (a -> b) -> a -> b
    $ (DCon -> SgM DCon) -> [DCon] -> SgM [DCon]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Name -> DCon -> SgM DCon
    singCtor Name
    ty_tycon) [DCon]
    cons
      Maybe [DType]
    mb_sctxt <- ([DType] -> SgM [DType]) -> Maybe [DType] -> SgM (Maybe [DType])
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((DType -> SgM DType) -> [DType] -> SgM [DType]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM DType -> SgM DType
    singPred) Maybe [DType]
    mb_ctxt
      DType
    kind <- DType -> SgM DType
    forall (m :: * -> *). MonadFail m => DType -> m DType
    promoteType DType
    ty
      DDec
    sEqInst <- Maybe [DType]
    -> DType -> [DCon] -> [DCon] -> EqualityClassDesc SgM -> SgM DDec
    forall (q :: * -> *).
    DsMonad q =>
    Maybe [DType]
    -> DType -> [DCon] -> [DCon] -> EqualityClassDesc q -> q DDec
    mkEqualityInstance Maybe [DType]
    mb_sctxt DType
    kind [DCon]
    cons [DCon]
    scons EqualityClassDesc SgM
    forall (q :: * -> *). Quasi q => EqualityClassDesc q
    sEqClassDesc
      -- Beware! The user might have specified an instance context like this:
      --
      --   deriving instance Eq a => Eq (T a Int)
      --
      -- When we single the context, it will become (SEq a). But we do *not* want
      -- this for the SDecide instance! The simplest solution is to simply replace
      -- all occurrences of SEq with SDecide in the context.
      let mb_sctxtDecide :: Maybe [DType]
    mb_sctxtDecide = ([DType] -> [DType]) -> Maybe [DType] -> Maybe [DType]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((DType -> DType) -> [DType] -> [DType]
    forall a b. (a -> b) -> [a] -> [b]
    map DType -> DType
    sEqToSDecide) Maybe [DType]
    mb_sctxt
      DDec
    sDecideInst <- Maybe [DType]
    -> DType -> [DCon] -> [DCon] -> EqualityClassDesc SgM -> SgM DDec
    forall (q :: * -> *).
    DsMonad q =>
    Maybe [DType]
    -> DType -> [DCon] -> [DCon] -> EqualityClassDesc q -> q DDec
    mkEqualityInstance Maybe [DType]
    mb_sctxtDecide DType
    kind [DCon]
    cons [DCon]
    scons EqualityClassDesc SgM
    forall (q :: * -> *). Quasi q => EqualityClassDesc q
    sDecideClassDesc
      [DDec]
    testInsts <- (TestInstance -> SgM DDec) -> [TestInstance] -> SgM [DDec]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Maybe [DType]
    -> DType -> Name -> [DCon] -> TestInstance -> SgM DDec
    forall (q :: * -> *).
    DsMonad q =>
    Maybe [DType] -> DType -> Name -> [DCon] -> TestInstance -> q DDec
    mkTestInstance Maybe [DType]
    mb_sctxtDecide DType
    kind Name
    ty_tycon [DCon]
    cons)
                            [TestInstance
    TestEquality, TestInstance
    TestCoercion]
      [DDec] -> SgM [DDec]
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DDec
    sEqInstDDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :DDec
    sDecideInstDDec -> [DDec] -> [DDec]
    forall a. a -> [a] -> [a]
    :[DDec]
    testInsts)

    -- Walk a DPred, replacing all occurrences of SEq with SDecide.
    sEqToSDecide :: DPred -> DPred
    sEqToSDecide :: DType -> DType
    sEqToSDecide = (Name -> Name) -> DType -> DType
    modifyConNameDType ((Name -> Name) -> DType -> DType)
    -> (Name -> Name) -> DType -> DType
    forall a b. (a -> b) -> a -> b
    $ \n :: Name
    n ->
      -- Why don't we directly compare n to sEqClassName? Because n is almost certainly
      -- produced from a call to singClassName, which uses unqualified Names. Ugh.
      if Name -> String
    nameBase Name
    n String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == Name -> String
    nameBase Name
    sEqClassName
         then Name
    sDecideClassName
         else Name
    n

    -- See Note [DerivedDecl] in Data.Singletons.Syntax
    singDerivedShowDecs :: DerivedShowDecl -> SgM [DDec]
    singDerivedShowDecs :: DerivedShowDecl -> SgM [DDec]
    singDerivedShowDecs (DerivedDecl { ded_mb_cxt :: forall (cls :: * -> Constraint). DerivedDecl cls -> Maybe [DType]
    ded_mb_cxt     = Maybe [DType]
    mb_cxt
                                     , ded_type :: forall (cls :: * -> Constraint). DerivedDecl cls -> DType
    ded_type       = DType
    ty
                                     , ded_type_tycon :: forall (cls :: * -> Constraint). DerivedDecl cls -> Name
    ded_type_tycon = Name
    ty_tycon
                                     , ded_decl :: forall (cls :: * -> Constraint). DerivedDecl cls -> DataDecl
    ded_decl       = DataDecl
    data_decl }) = do
        -- Generate a Show instance for a singleton type, like this:
        --
        --   instance (ShowSing a, ShowSing b) => Show (SEither (z :: Either a b)) where
        --     showsPrec p (SLeft (sl :: Sing l)) =
        --       showParen (p > 10) $ showString "SLeft " . showsPrec 11 sl
        --         :: ShowSing' l => ShowS
        --     showsPrec p (SRight (sr :: Sing r)) =
        --       showParen (p > 10) $ showString "SRight " . showsPrec 11 sr
        --         :: ShowSing' r => ShowS
        --
        -- Be careful: we want to generate an instance context that uses ShowSing,
        -- not SShow.
        UInstDecl
    show_sing_inst <- ShowMode -> DerivDesc SgM
    forall (q :: * -> *). DsMonad q => ShowMode -> DerivDesc q
    mkShowInstance (Name -> ShowMode
    ForShowSing Name
    ty_tycon) Maybe [DType]
    mb_cxt DType
    ty DataDecl
    data_decl
        [DDec] -> SgM [DDec]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [UInstDecl -> DDec
    toInstanceD UInstDecl
    show_sing_inst]
      where
        toInstanceD :: UInstDecl -> DDec
        toInstanceD :: UInstDecl -> DDec
    toInstanceD (InstDecl { id_cxt :: forall (ann :: AnnotationFlag). InstDecl ann -> [DType]
    id_cxt = [DType]
    cxt, id_name :: forall (ann :: AnnotationFlag). InstDecl ann -> Name
    id_name = Name
    inst_name
                              , id_arg_tys :: forall (ann :: AnnotationFlag). InstDecl ann -> [DType]
    id_arg_tys = [DType]
    inst_tys, id_meths :: forall (ann :: AnnotationFlag).
    InstDecl ann -> [(Name, LetDecRHS ann)]
    id_meths = [(Name, LetDecRHS Unannotated)]
    ann_meths }) =
          Maybe Overlap
    -> Maybe [DTyVarBndr] -> [DType] -> DType -> [DDec] -> DDec
    DInstanceD Maybe Overlap
    forall a. Maybe a
    Nothing Maybe [DTyVarBndr]
    forall a. Maybe a
    Nothing [DType]
    cxt (DType -> [DType] -> DType
    foldType (Name -> DType
    DConT Name
    inst_name) [DType]
    inst_tys)
                     (((Name, LetDecRHS Unannotated) -> DDec)
    -> [(Name, LetDecRHS Unannotated)] -> [DDec]
    forall a b. (a -> b) -> [a] -> [b]
    map (DLetDec -> DDec
    DLetDec (DLetDec -> DDec)
    -> ((Name, LetDecRHS Unannotated) -> DLetDec)
    -> (Name, LetDecRHS Unannotated)
    -> DDec
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Name, LetDecRHS Unannotated) -> DLetDec
    toFunD) [(Name, LetDecRHS Unannotated)]
    ann_meths)

        toFunD :: (Name, ULetDecRHS) -> DLetDec
        toFunD :: (Name, LetDecRHS Unannotated) -> DLetDec
    toFunD (fun_name :: Name
    fun_name, UFunction clauses) = Name -> [DClause] -> DLetDec
    DFunD Name
    fun_name [DClause]
    clauses
        toFunD (val_name :: Name
    val_name, UValue rhs)        = DPat -> DExp -> DLetDec
    DValD (Name -> DPat
    DVarP Name
    val_name) DExp
    rhs

    isException :: DExp -> Bool
    isException :: DExp -> Bool
    isException (DVarE n :: Name
    n)             = Name -> String
    nameBase Name
    n String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == "sUndefined"
    isException (DConE {})            = Bool
    False
    isException (DLitE {})            = Bool
    False
    isException (DAppE (DVarE fun :: Name
    fun) _) | Name -> String
    nameBase Name
    fun String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == "sError" = Bool
    True
    isException (DAppE fun :: DExp
    fun _)         = DExp -> Bool
    isException DExp
    fun
    isException (DAppTypeE e :: DExp
    e _)       = DExp -> Bool
    isException DExp
    e
    isException (DLamE _ _)           = Bool
    False
    isException (DCaseE e :: DExp
    e _)          = DExp -> Bool
    isException DExp
    e
    isException (DLetE _ e :: DExp
    e)           = DExp -> Bool
    isException DExp
    e
    isException (DSigE e :: DExp
    e _)           = DExp -> Bool
    isException DExp
    e
    isException (DStaticE e :: DExp
    e)          = DExp -> Bool
    isException DExp
    e

    singMatch :: Maybe DKind  -- ^ the result kind, if known
              -> ADMatch -> SgM DMatch
    singMatch :: Maybe DType -> ADMatch -> SgM DMatch
    singMatch res_ki :: Maybe DType
    res_ki (ADMatch var_proms :: VarPromotions
    var_proms pat :: ADPat
    pat exp :: ADExp
    exp) = do
      (sPat :: DPat
    sPat, sigPaExpsSigs :: SingDSigPaInfos
    sigPaExpsSigs) <- QWithAux SingDSigPaInfos SgM DPat -> SgM (DPat, SingDSigPaInfos)
    forall m (q :: * -> *) a. QWithAux m q a -> q (a, m)
    evalForPair (QWithAux SingDSigPaInfos SgM DPat -> SgM (DPat, SingDSigPaInfos))
    -> QWithAux SingDSigPaInfos SgM DPat -> SgM (DPat, SingDSigPaInfos)
    forall a b. (a -> b) -> a -> b
    $ Map Name Name -> ADPat -> QWithAux SingDSigPaInfos SgM DPat
    singPat (VarPromotions -> Map Name Name
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList VarPromotions
    var_proms) ADPat
    pat
      DExp
    sExp <- ADExp -> Maybe DType -> SgM DExp
    singExp ADExp
    exp Maybe DType
    res_ki
      DMatch -> SgM DMatch
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DMatch -> SgM DMatch) -> DMatch -> SgM DMatch
    forall a b. (a -> b) -> a -> b
    $ DPat -> DExp -> DMatch
    DMatch DPat
    sPat (DExp -> DMatch) -> DExp -> DMatch
    forall a b. (a -> b) -> a -> b
    $ SingDSigPaInfos -> DExp -> DExp
    mkSigPaCaseE SingDSigPaInfos
    sigPaExpsSigs DExp
    sExp

    singLit :: Lit -> SgM DExp
    singLit :: Lit -> SgM DExp
    singLit (IntegerL n :: Integer
    n)
      | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 0    = DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $
                    Name -> DExp
    DVarE Name
    sFromIntegerName DExp -> DExp -> DExp
    `DAppE`
                    (Name -> DExp
    DVarE Name
    singMethName DExp -> DType -> DExp
    `DSigE`
                     (DType
    singFamily DType -> DType -> DType
    `DAppT` TyLit -> DType
    DLitT (Integer -> TyLit
    NumTyLit Integer
    n)))
      | Bool
    otherwise = do DExp
    sLit <- Lit -> SgM DExp
    singLit (Integer -> Lit
    IntegerL (-Integer
    n))
                       DExp -> SgM DExp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ Name -> DExp
    DVarE Name
    sNegateName DExp -> DExp -> DExp
    `DAppE` DExp
    sLit
    singLit (StringL str :: String
    str) = do
      let sing_str_lit :: DExp
    sing_str_lit = Name -> DExp
    DVarE Name
    singMethName DExp -> DType -> DExp
    `DSigE`
                         (DType
    singFamily DType -> DType -> DType
    `DAppT` TyLit -> DType
    DLitT (String -> TyLit
    StrTyLit String
    str))
      Bool
    os_enabled <- Extension -> SgM Bool
    forall (m :: * -> *). Quasi m => Extension -> m Bool
    qIsExtEnabled Extension
    LangExt.OverloadedStrings
      DExp -> SgM DExp
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (DExp -> SgM DExp) -> DExp -> SgM DExp
    forall a b. (a -> b) -> a -> b
    $ if Bool
    os_enabled
             then Name -> DExp
    DVarE Name
    sFromStringName DExp -> DExp -> DExp
    `DAppE` DExp
    sing_str_lit
             else DExp
    sing_str_lit
    singLit lit :: Lit
    lit =
      String -> SgM DExp
    forall (m :: * -> *) a. MonadFail m => String -> m a
    fail ("Only string and natural number literals can be singled: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Lit -> String
    forall a. Show a => a -> String
    show Lit
    lit)

    maybeSigT :: DType -> Maybe DKind -> DType
    maybeSigT :: DType -> Maybe DType -> DType
    maybeSigT ty :: DType
    ty Nothing   = DType
    ty
    maybeSigT ty :: DType
    ty (Just ki :: DType
    ki) = DType
    ty DType -> DType -> DType
    `DSigT` DType
    ki

    {-
    Note [The id hack; or, how singletons learned to stop worrying and avoid kind generalization]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    GHC 8.8 was a time of great change. In particular, 8.8 debuted a fix for
    Trac #15141 (decideKindGeneralisationPlan is too complicated). To fix this, a
    wily GHC developer—who shall remain unnamed, but whose username rhymes with
    schmoldfire—decided to make decideKindGeneralisationPlan less complicated by,
    well, removing the whole thing. One consequence of this is that local
    definitions are now kind-generalized (whereas they would not have been
    previously).

    While schmoldfire had the noblest of intentions when authoring his fix, he
    unintentionally made life much harder for singletons. Why? Consider the
    following program:

      class Foo a where
        bar :: a -> (a -> b) -> b
        baz :: a

      quux :: Foo a => a -> a
      quux x = x `bar` \_ -> baz

    When singled, this program will turn into something like this:

      type family Quux (x :: a) :: a where
        Quux x = Bar x (LambdaSym1 x)

      sQuux :: forall a (x :: a). SFoo a => Sing x -> Sing (Quux x :: a)
      sQuux (sX :: Sing x)
        = sBar sX
            ((singFun1 @(LambdaSym1 x))
               (\ sArg
                  -> case sArg of {
                       (_ :: Sing arg)
                         -> (case sArg of { _ -> sBaz }) ::
                              Sing (Case x arg arg) }))

      type family Case x arg t where
        Case x arg _ = Baz
      type family Lambda x t where
        Lambda x arg = Case x arg arg
      data LambdaSym1 x t
      type instance Apply (LambdaSym1 x) t = Lambda x t

    The high-level bit is the explicit `Sing (Case x arg arg)` signature. Question:
    what is the kind of `Case x arg arg`? The answer depends on whether local
    definitions are kind-generalized or not!

    1. If local definitions are *not* kind-generalized (i.e., the status quo before
       GHC 8.8), then `Case x arg arg :: a`.
    2. If local definitions *are* kind-generalized (i.e., the status quo in GHC 8.8
       and later), then `Case x arg arg :: k` for some fresh kind variable `k`.

    Unfortunately, the kind of `Case x arg arg` *must* be `a` in order for `sQuux`
    to type-check. This means that the code above suddenly stopped working in GHC
    8.8. What's more, we can't just remove these explicit signatures, as there is
    code elsewhere in `singletons` that crucially relies on them to guide type
    inference along (e.g., `sShowParen` in `Data.Singletons.Prelude.Show`).

    Luckily, there is an ingenious hack that lets us the benefits of explicit
    signatures without the pain of kind generalization: our old friend, the `id`
    function. The plan is as follows: instead of generating this code:

      (case sArg of ...) :: Sing (Case x arg arg)

    We instead generate this code:

      id @(Sing (Case x arg arg)) (case sArg of ...)

    That's it! This works because visible type arguments in terms do not get kind-
    generalized, unlike top-level or local signatures. Now `Case x arg arg`'s kind
    is not generalized, and all is well. We dub this: the `id` hack.

    One might wonder: will we need the `id` hack around forever? Perhaps not. While
    GHC 8.8 removed the decideKindGeneralisationPlan function, there have been
    rumblings that a future version of GHC may bring it back (in a limited form).
    If this happens, it is possibly that GHC's attitude towards kind-generalizing
    local definitons may change *again*, which could conceivably render the `id`
    hack unnecessary. This is all speculation, of course, so all we can do now is
    wait and revisit this design at a later date.
    -}