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