{-# LANGUAGE TemplateHaskellQuotes #-}

{- Data/Singletons/TH/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-th package.
-}

module Data.Singletons.TH.Single where

import Prelude hiding ( exp )
import Language.Haskell.TH hiding ( cxt )
import Language.Haskell.TH.Syntax (NameSpace(..), Quasi(..))
import Data.Singletons.TH.Deriving.Bounded
import Data.Singletons.TH.Deriving.Enum
import Data.Singletons.TH.Deriving.Eq
import Data.Singletons.TH.Deriving.Infer
import Data.Singletons.TH.Deriving.Ord
import Data.Singletons.TH.Deriving.Show
import Data.Singletons.TH.Deriving.Util
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Partition
import Data.Singletons.TH.Promote
import Data.Singletons.TH.Promote.Defun
import Data.Singletons.TH.Promote.Monad ( promoteM )
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Single.Data
import Data.Singletons.TH.Single.Decide
import Data.Singletons.TH.Single.Defun
import Data.Singletons.TH.Single.Fixity
import Data.Singletons.TH.Single.Monad
import Data.Singletons.TH.Single.Ord
import Data.Singletons.TH.Single.Type
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
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 Data.Map.Strict as Map
import Data.Map.Strict ( Map )
import Data.Maybe
import qualified Data.Set as Set
import Control.Monad
import Control.Monad.Trans.Class
import Data.List (unzip6, zipWith4)
import qualified GHC.LanguageExtensions.Type as LangExt

{-
How singletons-th 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 singled definitions for each of the provided type-level
-- declaration 'Name's. For example, the singletons-th package itself uses
--
-- > $(genSingletons [''Bool, ''Maybe, ''Either, ''[]])
--
-- to generate singletons for Prelude types.
genSingletons :: OptionsMonad q => [Name] -> q [Dec]
genSingletons :: forall (q :: * -> *). OptionsMonad q => [Name] -> q [Dec]
genSingletons [Name]
names = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  -- See Note [Disable genQuotedDecs in genPromotions and genSingletons]
  -- in D.S.TH.Promote
  withOptions opts{genQuotedDecs = False} $ do
    checkForRep names
    ddecs <- concatMapM (singInfo <=< dsInfo <=< reifyWithLocals) names
    return $ decsToTH ddecs

-- | Make promoted and singled versions of all declarations given, retaining
-- the original declarations. See the
-- @<https://github.com/goldfirere/singletons/blob/master/README.md README>@
-- for further explanation.
singletons :: OptionsMonad q => q [Dec] -> q [Dec]
singletons :: forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
singletons q [Dec]
qdecs = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  withOptions opts{genQuotedDecs = True} $ singletons' $ lift qdecs

-- | Make promoted and singled 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 :: OptionsMonad q => q [Dec] -> q [Dec]
singletonsOnly :: forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
singletonsOnly q [Dec]
qdecs = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  withOptions opts{genQuotedDecs = False} $ singletons' $ lift qdecs

-- The workhorse for 'singletons' and 'singletonsOnly'. The difference between
-- the two functions is whether 'genQuotedDecs' is set to 'True' or 'False'.
singletons' :: OptionsMonad q => q [Dec] -> q [Dec]
singletons' :: forall (q :: * -> *). OptionsMonad q => q [Dec] -> q [Dec]
singletons' q [Dec]
qdecs = do
  opts     <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  decs     <- qdecs
  ddecs    <- withLocalDeclarations decs $ dsDecs decs
  singDecs <- singTopLevelDecs decs ddecs
  let origDecs | Options -> Bool
genQuotedDecs Options
opts = [Dec]
decs
               | Bool
otherwise          = []
  return $ origDecs ++ decsToTH singDecs

-- | Create instances of 'SEq' for the given types
singEqInstances :: OptionsMonad q => [Name] -> q [Dec]
singEqInstances :: forall (q :: * -> *). OptionsMonad q => [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 :: * -> *). OptionsMonad q => Name -> q [Dec]
singEqInstance

-- | Create instance of 'SEq' for the given type
singEqInstance :: OptionsMonad q => Name -> q [Dec]
singEqInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
singEqInstance = DerivDesc q -> String -> Name -> q [Dec]
forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
singInstance DerivDesc q
forall (q :: * -> *). DsMonad q => DerivDesc q
mkEqInstance String
"Eq"

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

-- | Create instances of 'SDecide', 'Eq', 'TestEquality', and 'TestCoercion' for
-- the given type.
singDecideInstance :: OptionsMonad q => Name -> q [Dec]
singDecideInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
singDecideInstance Name
name = do
  (_df, tvbs, cons) <- String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
getDataD (String
"I cannot make an instance of SDecide for it.") Name
name
  dtvbs <- mapM dsTvbVis tvbs
  let data_ty = DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndrVis]
dtvbs
  dcons <- concatMapM (dsCon dtvbs data_ty) cons
  (scons, _) <- singM [] $ mapM (singCtor name) dcons
  sDecideInstance <- mkDecideInstance Nothing data_ty dcons scons
  eqInstance <- mkEqInstanceForSingleton data_ty name
  testInstances <- traverse (mkTestInstance Nothing data_ty name dcons)
                            [TestEquality, TestCoercion]
  return $ decsToTH (sDecideInstance:eqInstance:testInstances)

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

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

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

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

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

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

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

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

-- | Create instance of 'Show' for the given singleton type
--
-- (Not to be confused with 'singShowInstance'.)
showSingInstance :: OptionsMonad q => Name -> q [Dec]
showSingInstance :: forall (q :: * -> *). OptionsMonad q => Name -> q [Dec]
showSingInstance Name
name = do
  (df, tvbs, cons) <- String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
getDataD (String
"I cannot make an instance of Show for it.") Name
name
  dtvbs <- mapM dsTvbVis tvbs
  let data_ty = DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndrVis]
dtvbs
  dcons <- concatMapM (dsCon dtvbs data_ty) cons
  let tyvars    = (DTyVarBndrVis -> DType) -> [DTyVarBndrVis] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name -> DType
DVarT (Name -> DType)
-> (DTyVarBndrVis -> Name) -> DTyVarBndrVis -> DType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName) [DTyVarBndrVis]
dtvbs
      kind      = DType -> DCxt -> DType
foldType (Name -> DType
DConT Name
name) DCxt
tyvars
      data_decl = DataFlavor -> Name -> [DTyVarBndrVis] -> [DCon] -> DataDecl
DataDecl DataFlavor
df Name
name [DTyVarBndrVis]
dtvbs [DCon]
dcons
      deriv_show_decl = DerivedDecl { ded_mb_cxt :: Maybe DCxt
ded_mb_cxt     = Maybe DCxt
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, _) <- singM [] $ singDerivedShowDecs deriv_show_decl
  pure $ decsToTH show_insts

-- | Create instances of 'Show' for the given singleton types
--
-- (Not to be confused with 'singShowInstances'.)
showSingInstances :: OptionsMonad q => [Name] -> q [Dec]
showSingInstances :: forall (q :: * -> *). OptionsMonad q => [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 :: * -> *). OptionsMonad 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 :: forall (q :: * -> *). DsMonad q => [Int] -> q [Dec]
singITyConInstances = (Int -> q Dec) -> [Int] -> q [Dec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM 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 :: forall (q :: * -> *). DsMonad q => Int -> q Dec
singITyConInstance Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
  = String -> q Dec
forall a. String -> q a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q Dec) -> String -> q Dec
forall a b. (a -> b) -> a -> b
$ String
"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]
++ String
")"
  | Bool
otherwise
  = do 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 String
"a")
       ks <- replicateM n (qNewName "k")
       k_last <- qNewName "k_last"
       f      <- qNewName "f"
       x      <- qNewName "x"
       let k_penult = [Name] -> Name
forall a. HasCallStack => [a] -> a
last [Name]
ks
           k_fun = [DTyVarBndrSpec] -> DCxt -> DCxt -> DType -> DType
ravelVanillaDType [] [] ((Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
ks) (Name -> DType
DVarT Name
k_last)
           f_ty  = Name -> DType
DVarT Name
f
           a_tys = (Name -> DType) -> [Name] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map Name -> DType
DVarT [Name]
as
           mk_fun DType
arrow DType
t1 DType
t2 = DType
arrow DType -> DType -> DType
`DAppT` DType
t1 DType -> DType -> DType
`DAppT` DType
t2
           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 -> DType -> DType -> DType
mk_fun (Name -> DType
DConT Name
tyFunArrowName) (Name -> DType
DVarT Name
k_penult) (Name -> DType
DVarT Name
k_last)
           ctxt = [ DForallTelescope -> DType -> DType
DForallT ([DTyVarBndrSpec] -> DForallTelescope
DForallInvis ((Name -> DTyVarBndrSpec) -> [Name] -> [DTyVarBndrSpec]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Specificity -> DTyVarBndrSpec
forall flag. Name -> flag -> DTyVarBndr flag
`DPlainTV` Specificity
SpecifiedSpec) [Name]
as)) (DType -> DType) -> DType -> DType
forall a b. (a -> b) -> a -> b
$
                    DCxt -> DType -> DType
DConstrainedT ((DType -> DType) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DType -> DType -> DType
DAppT (Name -> DType
DConT Name
singIName)) DCxt
a_tys)
                                  (Name -> DType
DConT Name
singIName DType -> DType -> DType
`DAppT` DType -> DCxt -> DType
foldType DType
f_ty DCxt
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
                  ]
       pure $ decToTH
            $ DInstanceD
                Nothing Nothing ctxt
                (DConT singIName `DAppT` (DConT (mkTyConName n) `DAppT` (f_ty `DSigT` k_fun)))
                [DLetDec $ DFunD singMethName
                           [DClause [] $
                            wrapSingFun 1 DWildCardT $
                            DLamE [x] $
                            DVarE withSingIName `DAppE` DVarE x
                                                `DAppE` DVarE singMethName]]

singInstance :: OptionsMonad q => DerivDesc q -> String -> Name -> q [Dec]
singInstance :: forall (q :: * -> *).
OptionsMonad q =>
DerivDesc q -> String -> Name -> q [Dec]
singInstance DerivDesc q
mk_inst String
inst_name Name
name = do
  (df, tvbs, cons) <- String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
forall (q :: * -> *).
DsMonad q =>
String -> Name -> q (DataFlavor, [TyVarBndrVis], [Con])
getDataD (String
"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]
++ String
" for it.") Name
name
  dtvbs <- mapM dsTvbVis tvbs
  let data_ty = DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs (Name -> DType
DConT Name
name) [DTyVarBndrVis]
dtvbs
  dcons <- concatMapM (dsCon dtvbs data_ty) cons
  let data_decl = DataFlavor -> Name -> [DTyVarBndrVis] -> [DCon] -> DataDecl
DataDecl DataFlavor
df Name
name [DTyVarBndrVis]
dtvbs [DCon]
dcons
  raw_inst <- mk_inst Nothing data_ty data_decl
  (a_inst, decs) <- promoteM [] $
                    promoteInstanceDec OMap.empty Map.empty raw_inst
  decs' <- singDecsM [] $ (:[]) <$> singInstD a_inst
  return $ decsToTH (decs ++ decs')

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

singTopLevelDecs :: OptionsMonad q => [Dec] -> [DDec] -> q [DDec]
singTopLevelDecs :: forall (q :: * -> *). OptionsMonad q => [Dec] -> [DDec] -> q [DDec]
singTopLevelDecs [Dec]
locals [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
  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                = letDecls
        , pd_class_decs              = classes
        , pd_instance_decs           = insts
        , pd_data_decs               = datas
        , pd_ty_syn_decs             = ty_syns
        , pd_open_type_family_decs   = o_tyfams
        , pd_closed_type_family_decs = c_tyfams
        , pd_derived_eq_decs         = derivedEqDecs
        , pd_derived_ord_decs        = derivedOrdDecs
        , pd_derived_show_decs       = derivedShowDecs } <- partitionDecs decls

  ((letDecEnv, classes', insts'), promDecls) <- promoteM locals $ do
    defunTopLevelTypeDecls ty_syns c_tyfams o_tyfams
    recSelLetDecls <- promoteDataDecs datas
    (_, letDecEnv) <- promoteLetDecs Nothing $ recSelLetDecls ++ letDecls
    classes' <- mapM promoteClassDec classes
    let meth_sigs    = (UClassDecl -> OMap Name DType) -> [UClassDecl] -> OMap Name DType
forall m a. Monoid m => (a -> m) -> [a] -> m
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
        cls_tvbs_map = [(Name, [DTyVarBndrVis])] -> Map Name [DTyVarBndrVis]
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Name, [DTyVarBndrVis])] -> Map Name [DTyVarBndrVis])
-> [(Name, [DTyVarBndrVis])] -> Map Name [DTyVarBndrVis]
forall a b. (a -> b) -> a -> b
$ (UClassDecl -> (Name, [DTyVarBndrVis]))
-> [UClassDecl] -> [(Name, [DTyVarBndrVis])]
forall a b. (a -> b) -> [a] -> [b]
map (\UClassDecl
cd -> (UClassDecl -> Name
forall (ann :: AnnotationFlag). ClassDecl ann -> Name
cd_name UClassDecl
cd, UClassDecl -> [DTyVarBndrVis]
forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndrVis]
cd_tvbs UClassDecl
cd)) [UClassDecl]
classes
    insts' <- mapM (promoteInstanceDec meth_sigs cls_tvbs_map) insts
    return (letDecEnv, classes', insts')

  singDecsM locals $ do
    dataLetBinds <- concatMapM buildDataLets datas
    methLetBinds <- concatMapM buildMethLets classes
    let letBinds = [(Name, DExp)]
dataLetBinds [(Name, DExp)] -> [(Name, DExp)] -> [(Name, DExp)]
forall a. [a] -> [a] -> [a]
++ [(Name, DExp)]
methLetBinds
    (newLetDecls, singIDefunDecls, newDecls)
                            <- bindLets letBinds $
                               singLetDecEnv letDecEnv $ do
                                 newDataDecls <- concatMapM singDataD datas
                                 newClassDecls <- mapM singClassD classes'
                                 newInstDecls <- mapM singInstD insts'
                                 newDerivedEqDecs <- concatMapM singDerivedEqDecs derivedEqDecs
                                 newDerivedOrdDecs <- concatMapM singDerivedOrdDecs derivedOrdDecs
                                 newDerivedShowDecs <- concatMapM singDerivedShowDecs derivedShowDecs
                                 return $ newDataDecls ++ newClassDecls
                                                       ++ newInstDecls
                                                       ++ newDerivedEqDecs
                                                       ++ newDerivedOrdDecs
                                                       ++ newDerivedShowDecs
    return $ promDecls ++ (map DLetDec newLetDecls) ++ singIDefunDecls ++ newDecls

-- see comment at top of file
buildDataLets :: OptionsMonad q => DataDecl -> q [(Name, DExp)]
buildDataLets :: forall (q :: * -> *).
OptionsMonad q =>
DataDecl -> q [(Name, DExp)]
buildDataLets (DataDecl DataFlavor
_df Name
_name [DTyVarBndrVis]
_tvbs [DCon]
cons) = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  fld_sels <- qIsExtEnabled LangExt.FieldSelectors
  pure $ concatMap (con_num_args opts fld_sels) cons
  where
    con_num_args :: Options -> Bool -> DCon -> [(Name, DExp)]
    con_num_args :: Options -> Bool -> DCon -> [(Name, DExp)]
con_num_args Options
opts Bool
fld_sels (DCon [DTyVarBndrSpec]
_tvbs DCxt
_cxt Name
name DConFields
fields DType
_rty) =
      (Name
name, Int -> DType -> DExp -> DExp
wrapSingFun (DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (DConFields -> DCxt
tysOfConFields DConFields
fields))
                         (Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
name)
                         (Name -> DExp
DConE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledDataConName Options
opts Name
name))
      (Name, DExp) -> [(Name, DExp)] -> [(Name, DExp)]
forall a. a -> [a] -> [a]
: Options -> Bool -> DConFields -> [(Name, DExp)]
rec_selectors Options
opts Bool
fld_sels DConFields
fields

    rec_selectors :: Options -> Bool -> DConFields -> [(Name, DExp)]
    rec_selectors :: Options -> Bool -> DConFields -> [(Name, DExp)]
rec_selectors Options
opts Bool
fld_sels DConFields
con
      | Bool
fld_sels
      = case DConFields
con of
          DNormalC {} -> []
          DRecC [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 Int
1 (Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
name)
                                   (Name -> DExp
DVarE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledValueName Options
opts Name
name))
            | Name
name <- [Name]
names ]

      | Bool
otherwise
      = []

-- see comment at top of file
buildMethLets :: OptionsMonad q => UClassDecl -> q [(Name, DExp)]
buildMethLets :: forall (q :: * -> *).
OptionsMonad q =>
UClassDecl -> q [(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 } }) = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  pure $ map (mk_bind opts) (OMap.assocs meth_sigs)
  where
    mk_bind :: Options -> LetBind -> (Name, DExp)
mk_bind Options
opts (Name
meth_name, DType
meth_ty) =
      ( Name
meth_name
      , Int -> DType -> DExp -> DExp
wrapSingFun (DType -> Int
countArgs DType
meth_ty) (Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
meth_name)
                                        (Name -> DExp
DVarE (Name -> DExp) -> Name -> DExp
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
singledValueName Options
opts Name
meth_name) )

singClassD :: AClassDecl -> SgM DDec
singClassD :: AClassDecl -> SgM DDec
singClassD (ClassDecl { cd_cxt :: forall (ann :: AnnotationFlag). ClassDecl ann -> DCxt
cd_cxt  = DCxt
cls_cxt
                      , cd_name :: forall (ann :: AnnotationFlag). ClassDecl ann -> Name
cd_name = Name
cls_name
                      , cd_tvbs :: forall (ann :: AnnotationFlag). ClassDecl ann -> [DTyVarBndrVis]
cd_tvbs = [DTyVarBndrVis]
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 } }) =
  DCxt -> SgM DDec -> SgM DDec
forall a. DCxt -> SgM a -> SgM a
bindContext [DType -> [DTyVarBndrVis] -> DType
foldTypeTvbs (Name -> DType
DConT Name
cls_name) [DTyVarBndrVis]
cls_tvbs] (SgM DDec -> SgM DDec) -> SgM DDec -> SgM DDec
forall a b. (a -> b) -> a -> b
$ do
    opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
    mb_cls_sak <- dsReifyType cls_name
    let sing_cls_name   = Options -> Name -> Name
singledClassName Options
opts Name
cls_name
        mb_sing_cls_sak = (DType -> DDec) -> Maybe DType -> Maybe DDec
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Name -> DType -> DDec
DKiSigD Name
sing_cls_name) Maybe DType
mb_cls_sak
    cls_infix_decls <- singReifiedInfixDecls $ cls_name:meth_names
    (sing_sigs, _, tyvar_names, cxts, res_kis, singIDefunss)
      <- unzip6 <$> zipWithM (singTySig no_meth_defns meth_sigs)
                             meth_names
                             (map (DConT . defunctionalizedName0 opts) meth_names)
    emitDecs $ maybeToList mb_sing_cls_sak ++ cls_infix_decls ++ concat singIDefunss
    let 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] -> Maybe DType -> Maybe DDec)
-> [Name] -> [DLetDec] -> [[Name]] -> [Maybe DType] -> [Maybe DDec]
forall a b c d e.
(a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]
zipWith4 (Options -> Name -> DLetDec -> [Name] -> Maybe DType -> Maybe DDec
mk_default_sig Options
opts) [Name]
meth_names [DLetDec]
sing_sigs
                                                      [[Name]]
tyvar_names [Maybe DType]
res_kis
    sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList cxts)))
                       (OMap.assocs default_defns)
    fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs fixities
    cls_cxt' <- mapM singPred cls_cxt
    return $ DClassD cls_cxt'
                     sing_cls_name
                     cls_tvbs
                     cls_fundeps   -- they are fine without modification
                     (map DLetDec (sing_sigs ++ sing_meths ++ fixities') ++ default_sigs)
  where
    no_meth_defns :: a
no_meth_defns = String -> a
forall a. HasCallStack => String -> a
error String
"Internal error: can't find declared method type"
    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 :: Options -> Name -> DLetDec -> [Name] -> Maybe DType -> Maybe DDec
    mk_default_sig :: Options -> Name -> DLetDec -> [Name] -> Maybe DType -> Maybe DDec
mk_default_sig Options
opts Name
meth_name (DSigD Name
s_name DType
sty) [Name]
bound_kvs (Just 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
<$> Options -> Name -> DType -> [Name] -> DType -> Maybe DType
add_constraints Options
opts Name
meth_name DType
sty [Name]
bound_kvs DType
res_ki
    mk_default_sig Options
_ Name
_ DLetDec
_ [Name]
_ Maybe DType
_ = String -> Maybe DDec
forall a. HasCallStack => String -> a
error String
"Internal error: a singled signature isn't a signature."

    add_constraints :: Options -> Name -> DType -> [Name] -> DType -> Maybe DType
    -- We must look through `... :: Type` kind annotations, which can be added
    -- when singling type signatures lacking explicit `forall`s.
    -- See Note [Preserve the order of type variables during singling]
    -- (wrinkle 1) in D.S.TH.Single.Type.
    add_constraints :: Options -> Name -> DType -> [Name] -> DType -> Maybe DType
add_constraints Options
opts Name
meth_name (DSigT DType
sty DType
ski) [Name]
bound_kvs DType
res_ki = do
      sty' <- Options -> Name -> DType -> [Name] -> DType -> Maybe DType
add_constraints Options
opts Name
meth_name DType
sty [Name]
bound_kvs DType
res_ki
      pure $ DSigT sty' ski
    add_constraints Options
opts Name
meth_name DType
sty [Name]
bound_kvs DType
res_ki = do
      (tvbs, cxt, args, res) <- DType -> Maybe ([DTyVarBndrSpec], DCxt, DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndrSpec], DCxt, DCxt, DType)
unravelVanillaDType DType
sty
      prom_dflt <- OMap.lookup meth_name promoted_defaults

      -- 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.
      let tvs = (DTyVarBndrSpec -> DType) -> [DTyVarBndrSpec] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrSpec -> DType
forall flag. DTyVarBndr flag -> DType
tvbToType ([DTyVarBndrSpec] -> DCxt) -> [DTyVarBndrSpec] -> DCxt
forall a b. (a -> b) -> a -> b
$
                (DTyVarBndrSpec -> Bool) -> [DTyVarBndrSpec] -> [DTyVarBndrSpec]
forall a. (a -> Bool) -> [a] -> [a]
filter (\DTyVarBndrSpec
tvb -> DTyVarBndrSpec -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrSpec
tvb Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Name
bound_kv_set) [DTyVarBndrSpec]
tvbs
          prom_meth =  Name -> DType
DConT (Name -> DType) -> Name -> DType
forall a b. (a -> b) -> a -> b
$ Options -> Name -> Name
defunctionalizedName0 Options
opts Name
meth_name
          default_pred = DType -> DCxt -> 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 -> DCxt -> DType
foldApply DType
prom_meth DCxt
tvs DType -> DType -> DType
`DSigT` DType
res_ki
                               , DType -> DCxt -> DType
foldApply DType
prom_dflt DCxt
tvs ]
      return $ ravelVanillaDType tvbs (default_pred : cxt) args res
      where
        bound_kv_set :: Set Name
bound_kv_set = [Name] -> Set Name
forall a. Ord a => [a] -> Set a
Set.fromList [Name]
bound_kvs

singInstD :: AInstDecl -> SgM DDec
singInstD :: AInstDecl -> SgM DDec
singInstD (InstDecl { id_cxt :: forall (ann :: AnnotationFlag). InstDecl ann -> DCxt
id_cxt = DCxt
cxt, id_name :: forall (ann :: AnnotationFlag). InstDecl ann -> Name
id_name = Name
inst_name, id_arg_tys :: forall (ann :: AnnotationFlag). InstDecl ann -> DCxt
id_arg_tys = DCxt
inst_tys
                    , id_sigs :: forall (ann :: AnnotationFlag). InstDecl ann -> OMap Name DType
id_sigs = OMap Name DType
inst_sigs, id_meths :: forall (ann :: AnnotationFlag).
InstDecl ann -> [(Name, LetDecRHS ann)]
id_meths = [(Name, LetDecRHS Annotated)]
ann_meths }) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let s_inst_name = Options -> Name -> Name
singledClassName Options
opts Name
inst_name
  bindContext cxt $ do
    cxt' <- mapM singPred cxt
    inst_kis <- mapM promoteType inst_tys
    meths <- concatMapM (uncurry sing_meth) ann_meths
    return (DInstanceD Nothing
                       Nothing
                       cxt'
                       (foldl DAppT (DConT s_inst_name) inst_kis)
                       meths)

  where
    sing_meth :: Name -> ALetDecRHS -> SgM [DDec]
    sing_meth :: Name -> LetDecRHS Annotated -> SgM [DDec]
sing_meth Name
name LetDecRHS Annotated
rhs = do
      opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      mb_s_info <- dsReify (singledValueName opts name)
      inst_kis <- mapM promoteType inst_tys
      let mk_subst [DTyVarBndr flag]
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] -> DCxt -> [LetBind]
forall a b. [a] -> [b] -> [(a, b)]
zip ((DTyVarBndr flag -> Name) -> [DTyVarBndr flag] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndr flag -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName [DTyVarBndr flag]
vis_cls_tvbs) DCxt
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 flag]
vis_cls_tvbs = Int -> [DTyVarBndr flag] -> [DTyVarBndr flag]
forall a. Int -> [a] -> [a]
drop ([DTyVarBndr flag] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndr flag]
cls_tvbs Int -> Int -> Int
forall a. Num a => a -> a -> a
- DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
inst_kis) [DTyVarBndr flag]
cls_tvbs

          sing_meth_ty :: DType -> SgM DType
          sing_meth_ty DType
inner_ty = do
            -- Make sure to expand through type synonyms here! Not doing so
            -- resulted in #167.
            raw_ty <- DType -> SgM DType
forall (q :: * -> *) a. (DsMonad q, Data a) => a -> q a
expand DType
inner_ty
            (s_ty, _num_args, _tyvar_names, _ctxt, _arg_kis, _res_ki)
              <- singType (DConT $ defunctionalizedName0 opts name) raw_ty
            pure s_ty

      s_ty <- case OMap.lookup name inst_sigs of
        Just DType
inst_sig ->
          -- We have an InstanceSig, so just single that type.
          DType -> SgM DType
sing_meth_ty DType
inst_sig
        Maybe DType
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 Name
_ (DForallT (DForallInvis [DTyVarBndrSpec]
cls_tvbs) (DConstrainedT DCxt
_cls_pred DType
s_ty)) Maybe Name
_) ->
            DType -> SgM DType
forall a. a -> SgM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> SgM DType) -> DType -> SgM DType
forall a b. (a -> b) -> a -> b
$ Map Name DType -> DType -> DType
substType ([DTyVarBndrSpec] -> Map Name DType
forall {flag}. [DTyVarBndr flag] -> Map Name DType
mk_subst [DTyVarBndrSpec]
cls_tvbs) DType
s_ty
          Maybe DInfo
_ -> do
            mb_info <- Name -> SgM (Maybe DInfo)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe DInfo)
dsReify Name
name
            case mb_info of
              Just (DVarI Name
_ (DForallT (DForallInvis [DTyVarBndrSpec]
cls_tvbs)
                                      (DConstrainedT DCxt
_cls_pred DType
inner_ty)) Maybe Name
_) -> do
                s_ty <- DType -> SgM DType
sing_meth_ty DType
inner_ty
                pure $ substType (mk_subst cls_tvbs) s_ty
              Maybe DInfo
_ -> String -> SgM DType
forall a. String -> SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> SgM DType) -> String -> SgM DType
forall a b. (a -> b) -> a -> b
$ String
"Cannot find type of method " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
name

      meth' <- singLetDecRHS
                 Map.empty -- Because we are singling an instance declaration,
                           -- we aren't generating defunctionalization symbols
                           -- for the class methods, and hence we aren't
                           -- generating any SingI instances. Therefore, we
                           -- don't need to include anything in this Map.
                 name rhs
      return $ map DLetDec [DSigD (singledValueName opts name) s_ty, 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.TH.Single.Defun)
                 -- 3. The result of running the `SgM a` action
singLetDecEnv :: forall a. 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 })
              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, letBinds, _tyvarNames, cxts, _res_kis, singIDefunss)
    <- [(DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType,
  [DDec])]
-> ([DLetDec], [(Name, DExp)], [[Name]], [(Name, DCxt)],
    [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, DCxt), Maybe DType,
   [DDec])]
 -> ([DLetDec], [(Name, DExp)], [[Name]], [(Name, DCxt)],
     [Maybe DType], [[DDec]]))
-> SgM
     [(DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType,
       [DDec])]
-> SgM
     ([DLetDec], [(Name, DExp)], [[Name]], [(Name, DCxt)],
      [Maybe DType], [[DDec]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (LetBind
 -> SgM
      (DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType, [DDec]))
-> [LetBind]
-> SgM
     [(DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType,
       [DDec])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Name
 -> DType
 -> SgM
      (DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType, [DDec]))
-> LetBind
-> SgM
     (DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType, [DDec])
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (OMap Name (LetDecRHS Annotated)
-> OMap Name DType
-> Name
-> DType
-> SgM
     (DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType, [DDec])
singTySig OMap Name (LetDecRHS Annotated)
defns OMap Name DType
types)) [LetBind]
prom_list
  infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs infix_decls
  bindLets letBinds $ do
    let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList cxts)))
                     (OMap.assocs defns)
    thing <- thing_inside
    return (infix_decls' ++ typeSigs ++ let_decs, concat singIDefunss, thing)

singTySig :: OMap Name ALetDecRHS  -- definitions
          -> OMap Name DType       -- type signatures
          -> 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]          -- 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
-> Name
-> DType
-> SgM
     (DLetDec, (Name, DExp), [Name], (Name, DCxt), Maybe DType, [DDec])
singTySig OMap Name (LetDecRHS Annotated)
defns OMap Name DType
types Name
name DType
prom_ty = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let sName = Options -> Name -> Name
singledValueName Options
opts Name
name
  case OMap.lookup name types of
    Maybe DType
Nothing -> do
      num_args <- SgM Int
guess_num_args
      (sty, tyvar_names) <- mk_sing_ty num_args
      singIDefuns <- singDefuns name VarName []
                                (map (const Nothing) tyvar_names) Nothing
      return ( DSigD sName sty
             , (name, wrapSingFun num_args prom_ty (DVarE sName))
             , tyvar_names
             , (name, [])
             , Nothing
             , singIDefuns )
    Just DType
ty -> do
      (sty, num_args, tyvar_names, ctxt, arg_kis, res_ki)
        <- DType -> DType -> SgM (DType, Int, [Name], DCxt, DCxt, DType)
singType DType
prom_ty DType
ty
      bound_cxt <- askContext
      singIDefuns <- singDefuns name VarName (bound_cxt ++ ctxt)
                                (map Just arg_kis) (Just res_ki)
      return ( DSigD sName sty
             , (name, wrapSingFun num_args prom_ty (DVarE sName))
             , tyvar_names
             , (name, ctxt)
             , Just res_ki
             , 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
        Maybe (LetDecRHS Annotated)
Nothing -> String -> SgM Int
forall a. String -> SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Internal error: promotion known for something not let-bound."
        Just (AValue ADExp
_) -> Int -> SgM Int
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
0
        Just (AFunction Int
n [ADClause]
_) -> Int -> SgM Int
forall a. a -> SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n

      -- 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 Int
n = do
      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 String
"arg")
      -- If there are no arguments, use `Sing @_` instead of `Sing`.
      -- See Note [Disable kind generalization for local functions if possible]
      let sing_w_wildcard | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = DType
singFamily DType -> DType -> DType
`DAppKindT` DType
DWildCardT
                          | Bool
otherwise = DType
singFamily
      return ( ravelVanillaDType
                 (map (`DPlainTV` SpecifiedSpec) arg_names)
                 []
                 (map (\Name
nm -> DType
singFamily DType -> DType -> DType
`DAppT` Name -> DType
DVarT Name
nm) arg_names)
                 (sing_w_wildcard `DAppT`
                      (foldApply prom_ty (map DVarT arg_names)))
             , arg_names )

{-
Note [Disable kind generalization for local functions if possible]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this example (from #296):

  f :: forall a. MyProxy a -> MyProxy a
  f MyProxy =
    let x = let z :: MyProxy a
                z = MyProxy in z
    in x

A naïve attempt at singling `f` is as follows:

  type LetZ :: MyProxy a
  type family LetZ where
    LetZ = 'MyProxy

  type family LetX where
    LetX = LetZ

  type F :: forall a. MyProxy a -> MyProxy a
  type family F x where
    F 'MyProxy = LetX

  sF :: forall a (t :: MyProxy a). Sing t -> Sing (F t :: MyProxy a)
  sF SMyProxy =
    let sX :: Sing LetX
        sX = let sZ :: Sing (LetZ :: MyProxy a)
                 sZ = SMyProxy in sZ
    in sX

This will not typecheck, however. The is because the return kind of
`LetX` (in `let sX :: Sing LetX`) will get generalized by virtue of `sX`
having a type signature. It's as if one had written this:

  sF :: forall a (t :: MyProxy a). Sing t -> Sing (F t :: MyProxy a)
  sF SMyProxy =
    let sX :: forall a1. Sing (LetX :: MyProxy a1)
        sX = ...

This is too general, since `sX` will only typecheck if the return kind of
`LetX` is `MyProxy a`, not `MyProxy a1`. In order to avoid this problem,
we need to avoid kind generalization when kind-checking the type of `sX`.
To accomplish this, we borrow a trick from
Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization]
and use TypeApplications plus a wildcard type. That is, we generate this code
for `sF`:

  sF :: forall a (t :: MyProxy a). Sing t -> Sing (F t :: MyProxy a)
  sF SMyProxy =
    let sX :: Sing @_ LetX
        sX = ...

The presence of the wildcard type disables kind generalization, which allows
GHC's kind inference to deduce that the return kind of `LetX` should be `a`.
Now `sF` typechecks, and since we only use wildcards within visible kind
applications, we don't even have to force users to enable
PartialTypeSignatures. Hooray!

Question: where should we put wildcard types when singling? One possible answer
is: put a wildcard in any type signature that gets generated when singling a
function that lacks a type signature. Unfortunately, this is a step too far.
This will break singling the `foldr` function:

    foldr                   :: (a -> b -> b) -> b -> [a] -> b
    foldr k z = go
              where
                go []     = z
                go (y:ys) = y `k` go ys

If the type of `sGo` is given a wildcard, then it will fail to typecheck. This
is because `sGo` is polymorphically recursive, so disabling kind generalization
forces GHC to infer `sGo`'s type. Attempting to infer a polymorphically
recursive type, unsurprisingly, leads to failure.

To avoid this sort of situation, where adopt a simple metric: if a function
lacks a type signature, only put @_ in its singled type signature if it has
zero arguments. This allows `sX` to typecheck without breaking things like
`sGo`. This metric is a bit conservative, however, since it means that this
small tweak to `x` still would not typecheck:

  f :: forall a. MyProxy a -> MyProxy a
  f MyProxy =
    let x () = let z :: MyProxy a
                   z = MyProxy in z
    in x ()

We need not let perfect be the enemy of good, however. It is extremely
common for local definitions to have zero arguments, so it makes good sense
to optimize for that special case. In fact, this special treatment is the only
reason that `foo8` from the `T183` test case singles successfully, since
the as-patterns in `foo8` desugar to code very similar to the `f` example
above.
-}

singLetDecRHS :: Map Name DCxt    -- the context of the type signature
                                  -- (might not be known)
              -> Name -> ALetDecRHS -> SgM DLetDec
singLetDecRHS :: Map Name DCxt -> Name -> LetDecRHS Annotated -> SgM DLetDec
singLetDecRHS Map Name DCxt
cxts Name
name LetDecRHS Annotated
ld_rhs = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  bindContext (Map.findWithDefault [] name cxts) $
    case ld_rhs of
      AValue ADExp
exp ->
        DPat -> DExp -> DLetDec
DValD (Name -> DPat
DVarP (Options -> Name -> Name
singledValueName Options
opts Name
name)) (DExp -> DLetDec) -> SgM DExp -> SgM DLetDec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        ADExp -> SgM DExp
singExp ADExp
exp
      AFunction Int
_num_arrows [ADClause]
clauses ->
        Name -> [DClause] -> DLetDec
DFunD (Options -> Name -> Name
singledValueName Options
opts 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ADClause -> SgM DClause
singClause [ADClause]
clauses

singClause :: ADClause -> SgM DClause
singClause :: ADClause -> SgM DClause
singClause (ADClause VarPromotions
var_proms [ADPat]
pats ADExp
exp) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  (sPats, sigPaExpsSigs) <- evalForPair $ mapM (singPat (Map.fromList var_proms)) pats
  let lambda_binds = ((Name, Name) -> (Name, Name)) -> VarPromotions -> VarPromotions
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,Name
_) -> (Name
n, Options -> Name -> Name
singledValueName Options
opts Name
n)) VarPromotions
var_proms
  sBody <- bindLambdas lambda_binds $ singExp exp
  return $ DClause sPats $ mkSigPaCaseE sigPaExpsSigs 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 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) =
      String -> QWithAux SingDSigPaInfos SgM DPat
forall a. String -> QWithAux SingDSigPaInfos SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Singling of literal patterns not yet supported"
    go (ADVarP Name
name) = do
      opts <- QWithAux SingDSigPaInfos SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      tyname <- case Map.lookup name var_proms of
                  Maybe Name
Nothing     ->
                    String -> QWithAux SingDSigPaInfos SgM Name
forall a. String -> QWithAux SingDSigPaInfos SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Internal error: unknown variable when singling pattern"
                  Just Name
tyname -> Name -> QWithAux SingDSigPaInfos SgM Name
forall a. a -> QWithAux SingDSigPaInfos SgM a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
tyname
      pure $ DVarP (singledValueName opts name)
               `DSigP` (singFamily `DAppT` DVarT tyname)
    go (ADConP Name
name DCxt
tys [ADPat]
pats) = do
      opts <- QWithAux SingDSigPaInfos SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
      DConP (singledDataConName opts name) tys <$> mapM go pats
    go (ADTildeP ADPat
pat) = do
      String -> QWithAux SingDSigPaInfos SgM ()
forall (q :: * -> *). Quasi q => String -> q ()
qReportWarning
        String
"Lazy pattern converted into regular pattern during singleton generation."
      ADPat -> QWithAux SingDSigPaInfos SgM DPat
go ADPat
pat
    go (ADBangP 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 DType
prom_pat ADPat
pat DType
ty) = do
      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].
      addElement (dPatToDExp pat', DSigT prom_pat ty)
      pure pat'
    go ADPat
ADWildP = DPat -> QWithAux SingDSigPaInfos SgM DPat
forall a. a -> QWithAux SingDSigPaInfos SgM a
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 SingDSigPaInfos
exps_with_sigs DExp
exp
  | SingDSigPaInfos -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null SingDSigPaInfos
exps_with_sigs = DExp
exp
  | Bool
otherwise =
      let ([DExp]
exps, DCxt
sigs) = SingDSigPaInfos -> ([DExp], DCxt)
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) -> DCxt -> [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)) DCxt
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-th 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 -> SgM DExp
  -- See Note [Why error is so special]
singExp :: ADExp -> SgM DExp
singExp (ADVarE Name
err `ADAppE` ADExp
arg)
  | Name
err Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
errorName = do opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
                          DAppE (DVarE (singledValueName opts err)) <$>
                            singExp arg
singExp (ADVarE Name
name) = Name -> SgM DExp
lookupVarE Name
name
singExp (ADConE Name
name) = Name -> SgM DExp
lookupConE Name
name
singExp (ADLitE Lit
lit)  = Lit -> SgM DExp
singLit Lit
lit
singExp (ADAppE ADExp
e1 ADExp
e2) = do
  e1' <- ADExp -> SgM DExp
singExp ADExp
e1
  e2' <- singExp e2
  -- `applySing undefined x` kills type inference, because GHC can't figure
  -- out the type of `undefined`. So we don't emit `applySing` there.
  if isException e1'
  then return $ e1' `DAppE` e2'
  else return $ (DVarE applySingName) `DAppE` e1' `DAppE` e2'
singExp (ADLamE [Name]
ty_names DType
prom_lam [Name]
names ADExp
exp) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let sNames = (Name -> Name) -> [Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Options -> Name -> Name
singledValueName Options
opts) [Name]
names
  exp' <- bindLambdas (zip names sNames) $ singExp exp
  -- we need to bind the type variables... but DLamE doesn't allow SigT patterns.
  -- So: build a case
  let 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']
  return $ wrapSingFun (length names) prom_lam $ DLamE sNames caseExp
singExp (ADCaseE ADExp
exp [ADMatch]
matches DType
ret_ty) =
    -- See Note [Annotate case return type] and
    --     Note [The id hack; or, how singletons-th 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))
    (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 -> SgM DExp
singExp ADExp
exp SgM ([DMatch] -> DExp) -> SgM [DMatch] -> SgM DExp
forall a b. SgM (a -> b) -> SgM a -> SgM b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ADMatch -> SgM DMatch
singMatch [ADMatch]
matches)
singExp (ADLetE ALetDecEnv
env ADExp
exp) = 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, _, 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 -> SgM DExp
singExp ADExp
exp
  pure $ DLetE let_decs exp'
singExp (ADSigE DType
prom_exp ADExp
exp DType
ty) = do
  exp' <- ADExp -> SgM DExp
singExp ADExp
exp
  pure $ DSigE exp' $ DConT singFamilyName `DAppT` DSigT prom_exp ty

-- See Note [DerivedDecl] in Data.Singletons.TH.Syntax
singDerivedEqDecs :: DerivedEqDecl -> SgM [DDec]
singDerivedEqDecs :: DerivedEqDecl -> SgM [DDec]
singDerivedEqDecs (DerivedDecl { ded_mb_cxt :: forall (cls :: * -> Constraint). DerivedDecl cls -> Maybe DCxt
ded_mb_cxt     = Maybe DCxt
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 DataFlavor
_ Name
_ [DTyVarBndrVis]
_ [DCon]
cons }) = do
  (scons, _) <- [Dec] -> SgM [DCon] -> SgM ([DCon], [DDec])
forall (q :: * -> *) a.
OptionsMonad 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name -> DCon -> SgM DCon
singCtor Name
ty_tycon) [DCon]
cons
  mb_sctxt <- mapM (mapM singPred) mb_ctxt
  -- 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.
  mb_sctxtDecide <- traverse (traverse sEqToSDecide) mb_sctxt
  sDecideInst <- mkDecideInstance mb_sctxtDecide ty cons scons
  eqInst <- mkEqInstanceForSingleton ty ty_tycon
  testInsts <- traverse (mkTestInstance mb_sctxtDecide ty ty_tycon cons)
                        [TestEquality, TestCoercion]
  return (sDecideInst:eqInst:testInsts)

-- Walk a DPred, replacing all occurrences of SEq with SDecide.
sEqToSDecide :: OptionsMonad q => DPred -> q DPred
sEqToSDecide :: forall (m :: * -> *). OptionsMonad m => DType -> m DType
sEqToSDecide DType
p = do
  opts <- q Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  pure $ modifyConNameDType (\Name
n ->
         if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Options -> Name -> Name
singledClassName Options
opts Name
eqName
            then Name
sDecideClassName
            else Name
n) p

-- See Note [DerivedDecl] in Data.Singletons.TH.Syntax
singDerivedOrdDecs :: DerivedOrdDecl -> SgM [DDec]
singDerivedOrdDecs :: DerivedOrdDecl -> SgM [DDec]
singDerivedOrdDecs (DerivedDecl { 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 }) = do
    ord_inst <- DType -> Name -> SgM DDec
forall (q :: * -> *). OptionsMonad q => DType -> Name -> q DDec
mkOrdInstanceForSingleton DType
ty Name
ty_tycon
    pure [ord_inst]

-- See Note [DerivedDecl] in Data.Singletons.TH.Syntax
singDerivedShowDecs :: DerivedShowDecl -> SgM [DDec]
singDerivedShowDecs :: DerivedShowDecl -> SgM [DDec]
singDerivedShowDecs (DerivedDecl { ded_mb_cxt :: forall (cls :: * -> Constraint). DerivedDecl cls -> Maybe DCxt
ded_mb_cxt     = Maybe DCxt
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 DataFlavor
_ Name
_ [DTyVarBndrVis]
_ [DCon]
cons }) = do
    opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
    z <- qNewName "z"
    -- Generate a Show instance for a singleton type, like this:
    --
    --   deriving instance (ShowSing a, ShowSing b) => Sing (SEither (z :: Either a b))
    --
    -- Be careful: we want to generate an instance context that uses ShowSing,
    -- not SShow.
    show_cxt <- inferConstraintsDef (fmap mkShowSingContext mb_cxt)
                                    (DConT showSingName)
                                    ty cons
    ki <- promoteType ty
    let sty_tycon = Options -> Name -> Name
singledDataTypeName Options
opts Name
ty_tycon
        show_inst = Maybe DDerivStrategy
-> Maybe [DTyVarBndrUnit] -> DCxt -> DType -> DDec
DStandaloneDerivD Maybe DDerivStrategy
forall a. Maybe a
Nothing Maybe [DTyVarBndrUnit]
forall a. Maybe a
Nothing DCxt
show_cxt
                      (Name -> DType
DConT Name
showName DType -> DType -> DType
`DAppT` (Name -> DType
DConT Name
sty_tycon DType -> DType -> DType
`DAppT` DType -> DType -> DType
DSigT (Name -> DType
DVarT Name
z) DType
ki))
    pure [show_inst]

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

singMatch :: ADMatch -> SgM DMatch
singMatch :: ADMatch -> SgM DMatch
singMatch (ADMatch VarPromotions
var_proms ADPat
pat ADExp
exp) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  (sPat, sigPaExpsSigs) <- evalForPair $ singPat (Map.fromList var_proms) pat
  let lambda_binds = ((Name, Name) -> (Name, Name)) -> VarPromotions -> VarPromotions
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
n,Name
_) -> (Name
n, Options -> Name -> Name
singledValueName Options
opts Name
n)) VarPromotions
var_proms
  sExp <- bindLambdas lambda_binds $ singExp exp
  return $ DMatch sPat $ mkSigPaCaseE sigPaExpsSigs sExp

singLit :: Lit -> SgM DExp
singLit :: Lit -> SgM DExp
singLit (IntegerL Integer
n) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  if n >= 0
     then return $
          DVarE (singledValueName opts fromIntegerName) `DAppE`
          (DVarE singMethName `DSigE`
           (singFamily `DAppT` DLitT (NumTyLit n)))
     else do sLit <- singLit (IntegerL (-n))
             return $ DVarE (singledValueName opts negateName) `DAppE` sLit
singLit (StringL String
str) = do
  opts <- SgM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
  let 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))
  os_enabled <- qIsExtEnabled LangExt.OverloadedStrings
  pure $ if os_enabled
         then DVarE (singledValueName opts fromStringName) `DAppE` sing_str_lit
         else sing_str_lit
singLit (CharL Char
c) =
  DExp -> SgM DExp
forall a. a -> SgM a
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
singMethName DExp -> DType -> DExp
`DSigE` (DType
singFamily DType -> DType -> DType
`DAppT` TyLit -> DType
DLitT (Char -> TyLit
CharTyLit Char
c))
singLit Lit
lit =
  String -> SgM DExp
forall a. String -> SgM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Only string, natural number, and character literals can be singled: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Lit -> String
forall a. Show a => a -> String
show Lit
lit)

{-
Note [The id hack; or, how singletons-th 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-th. 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-th` that crucially relies on them to guide type
inference along (e.g., `sShowParen` in `Text.Show.Singletons`).

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