module Data.Singletons.TH.Promote.Type
( promoteType, promoteType_NC, promoteType_options
, PromoteTypeOptions(..), defaultPromoteTypeOptions
, promoteTypeArg_NC, promoteUnraveled
) where
import Control.Monad (when)
import Language.Haskell.TH (pprint)
import Language.Haskell.TH.Desugar
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Util
promoteType :: OptionsMonad m => DType -> m DKind
promoteType :: forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType = PromoteTypeOptions -> DType -> m DType
forall (m :: * -> *).
OptionsMonad m =>
PromoteTypeOptions -> DType -> m DType
promoteType_options PromoteTypeOptions
defaultPromoteTypeOptions{ptoCheckVanilla = True}
promoteType_NC :: forall m. OptionsMonad m => DType -> m DKind
promoteType_NC :: forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC = PromoteTypeOptions -> DType -> m DType
forall (m :: * -> *).
OptionsMonad m =>
PromoteTypeOptions -> DType -> m DType
promoteType_options PromoteTypeOptions
defaultPromoteTypeOptions
data PromoteTypeOptions = PromoteTypeOptions
{ PromoteTypeOptions -> Bool
ptoCheckVanilla :: Bool
, PromoteTypeOptions -> Bool
ptoAllowWildcards :: Bool
} deriving Int -> PromoteTypeOptions -> ShowS
[PromoteTypeOptions] -> ShowS
PromoteTypeOptions -> String
(Int -> PromoteTypeOptions -> ShowS)
-> (PromoteTypeOptions -> String)
-> ([PromoteTypeOptions] -> ShowS)
-> Show PromoteTypeOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PromoteTypeOptions -> ShowS
showsPrec :: Int -> PromoteTypeOptions -> ShowS
$cshow :: PromoteTypeOptions -> String
show :: PromoteTypeOptions -> String
$cshowList :: [PromoteTypeOptions] -> ShowS
showList :: [PromoteTypeOptions] -> ShowS
Show
defaultPromoteTypeOptions :: PromoteTypeOptions
defaultPromoteTypeOptions :: PromoteTypeOptions
defaultPromoteTypeOptions = PromoteTypeOptions
{ ptoCheckVanilla :: Bool
ptoCheckVanilla = Bool
False
, ptoAllowWildcards :: Bool
ptoAllowWildcards = Bool
False
}
promoteType_options :: forall m. OptionsMonad m => PromoteTypeOptions -> DType -> m DKind
promoteType_options :: forall (m :: * -> *).
OptionsMonad m =>
PromoteTypeOptions -> DType -> m DType
promoteType_options PromoteTypeOptions
pto DType
typ = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (PromoteTypeOptions -> Bool
ptoCheckVanilla PromoteTypeOptions
pto) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
DType -> m ()
forall (m :: * -> *). MonadFail m => DType -> m ()
checkVanillaDType DType
typ
[DTypeArg] -> DType -> m DType
go [] DType
typ
where
go :: [DTypeArg] -> DType -> m DKind
go :: [DTypeArg] -> DType -> m DType
go [] (DForallT DForallTelescope
tele DType
ty) = do
DType
ty' <- [DTypeArg] -> DType -> m DType
go [] DType
ty
DType -> m DType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DForallTelescope -> DType -> DType
DForallT DForallTelescope
tele DType
ty'
go [DTypeArg]
args ty :: DType
ty@DForallT{} = [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
go [] (DConstrainedT DCxt
_cxt DType
ty) = [DTypeArg] -> DType -> m DType
go [] DType
ty
go [DTypeArg]
args ty :: DType
ty@DConstrainedT{} = [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
go [DTypeArg]
args (DAppT DType
t1 DType
t2) = do
DType
k2 <- [DTypeArg] -> DType -> m DType
go [] DType
t2
[DTypeArg] -> DType -> m DType
go (DType -> DTypeArg
DTANormal DType
k2 DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
args) DType
t1
go [DTypeArg]
args (DAppKindT DType
ty DType
ki) = do
DType
ki' <- [DTypeArg] -> DType -> m DType
go [] DType
ki
[DTypeArg] -> DType -> m DType
go (DType -> DTypeArg
DTyArg DType
ki' DTypeArg -> [DTypeArg] -> [DTypeArg]
forall a. a -> [a] -> [a]
: [DTypeArg]
args) DType
ty
go [DTypeArg]
args (DSigT DType
ty DType
ki) = do
DType
ty' <- [DTypeArg] -> DType -> m DType
go [] DType
ty
DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (DType -> DType -> DType
DSigT DType
ty' DType
ki) [DTypeArg]
args
go [DTypeArg]
args (DVarT Name
name) = DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DVarT Name
name) [DTypeArg]
args
go [DTypeArg]
args (DConT Name
name) = do
Options
opts <- m Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DConT (Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name)) [DTypeArg]
args
go [DTypeArg]
args ty :: DType
ty@DType
DArrowT =
case [DTypeArg] -> DCxt
filterDTANormals [DTypeArg]
args of
[] -> m DType
forall a. m a
noPartialArrows
[DType
_] -> m DType
forall a. m a
noPartialArrows
[DType
k1, DType
k2] -> DType -> m DType
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
tyFunArrowName DType -> DType -> DType
`DAppT` DType
k1 DType -> DType -> DType
`DAppT` DType
k2
(DType
_:DType
_:DType
_:DCxt
_) -> [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
go [] ty :: DType
ty@DLitT{} = DType -> m DType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
ty
go [DTypeArg]
args ty :: DType
ty@DLitT{} = [DTypeArg] -> DType -> m DType
forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
ty
go [DTypeArg]
args ty :: DType
ty@DWildCardT{}
| PromoteTypeOptions -> Bool
ptoAllowWildcards PromoteTypeOptions
pto
= DType -> m DType
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType DType
ty [DTypeArg]
args
| Bool
otherwise
= String -> m DType
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m DType) -> String -> m DType
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"`singletons-th` does not support wildcard types"
, String
"\tunless they appear in visible type patterns of data constructors"
, String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
herald
]
noPartialArrows :: m a
noPartialArrows :: forall a. m a
noPartialArrows = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"`singletons-th` does not support partial applications of (->)"
, String
"\t" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
herald
]
herald :: String
herald :: String
herald = String
"In the type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Type -> String
forall a. Ppr a => a -> String
pprint (DType -> Type
forall th ds. Desugar th ds => ds -> th
sweeten DType
typ)
illegal :: [DTypeArg] -> DType -> m a
illegal :: forall a. [DTypeArg] -> DType -> m a
illegal [DTypeArg]
args DType
hd = String -> m a
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m a) -> String -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
"Illegal Haskell construct encountered:"
, String
"\theaded by: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ DType -> String
forall a. Show a => a -> String
show DType
hd
, String
"\tapplied to: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [DTypeArg] -> String
forall a. Show a => a -> String
show [DTypeArg]
args
]
promoteTypeArg_NC :: OptionsMonad m => DTypeArg -> m DTypeArg
promoteTypeArg_NC :: forall (m :: * -> *). OptionsMonad m => DTypeArg -> m DTypeArg
promoteTypeArg_NC (DTANormal DType
t) = DType -> DTypeArg
DTANormal (DType -> DTypeArg) -> m DType -> m DTypeArg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DType -> m DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC DType
t
promoteTypeArg_NC ta :: DTypeArg
ta@(DTyArg DType
_) = DTypeArg -> m DTypeArg
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTypeArg
ta
promoteUnraveled :: OptionsMonad m
=> DType -> m ([DTyVarBndrSpec], [DKind], DKind)
promoteUnraveled :: forall (m :: * -> *).
OptionsMonad m =>
DType -> m ([DTyVarBndrSpec], DCxt, DType)
promoteUnraveled DType
ty = do
([DTyVarBndrSpec]
tvbs, DCxt
_, DCxt
arg_tys, DType
res_ty) <- DType -> m ([DTyVarBndrSpec], DCxt, DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndrSpec], DCxt, DCxt, DType)
unravelVanillaDType DType
ty
DCxt
arg_kis <- (DType -> m DType) -> DCxt -> m DCxt
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 DType -> m DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC DCxt
arg_tys
DType
res_ki <- DType -> m DType
forall (m :: * -> *). OptionsMonad m => DType -> m DType
promoteType_NC DType
res_ty
([DTyVarBndrSpec], DCxt, DType)
-> m ([DTyVarBndrSpec], DCxt, DType)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([DTyVarBndrSpec]
tvbs, DCxt
arg_kis, DType
res_ki)