module Data.Singletons.Promote.Type
( promoteType, promoteType_NC
, promoteTypeArg_NC, promoteUnraveled
) where
import Language.Haskell.TH.Desugar
import Data.Singletons.Names
import Data.Singletons.Util
import Language.Haskell.TH
promoteType :: MonadFail m => DType -> m DKind
promoteType :: DType -> m DType
promoteType DType
ty = do
DType -> m ()
forall (m :: * -> *). MonadFail m => DType -> m ()
checkVanillaDType DType
ty
DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
ty
promoteType_NC :: MonadFail m => DType -> m DKind
promoteType_NC :: DType -> m DType
promoteType_NC = [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go []
where
go :: MonadFail m => [DTypeArg] -> DType -> m DKind
go :: [DTypeArg] -> DType -> m DType
go [] (DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs DType
ty) = do
DType
ty' <- [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
DType -> m DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ ForallVisFlag -> [DTyVarBndr] -> DType -> DType
DForallT ForallVisFlag
fvf [DTyVarBndr]
tvbs DType
ty'
go [] (DConstrainedT DCxt
_cxt DType
ty) = [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
go [DTypeArg]
args (DAppT DType
t1 DType
t2) = do
DType
k2 <- [DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
t2
[DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [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
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ki
[DTypeArg] -> DType -> m DType
forall (m :: * -> *). MonadFail m => [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
forall (m :: * -> *). MonadFail m => [DTypeArg] -> DType -> m DType
go [] DType
ty
DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (DType -> DType -> DType
DSigT DType
ty' DType
ki) [DTypeArg]
args
go [DTypeArg]
args (DVarT Name
name) = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DVarT Name
name) [DTypeArg]
args
go [] (DConT Name
name)
| Name
name Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
typeRepName = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
| Name -> String
nameBase Name
name String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> String
nameBase Name
repName = DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
typeKindName
go [DTypeArg]
args (DConT Name
name)
| Just Int
n <- Name -> Maybe Int
unboxedTupleNameDegree_maybe Name
name
= DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DConT (Int -> Name
tupleTypeName Int
n)) [DTypeArg]
args
| Bool
otherwise
= DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ DType -> [DTypeArg] -> DType
applyDType (Name -> DType
DConT Name
name) [DTypeArg]
args
go [DTANormal DType
k1, DTANormal DType
k2] DType
DArrowT
= DType -> m DType
forall (m :: * -> *) a. Monad m => a -> m a
return (DType -> m DType) -> DType -> m DType
forall a b. (a -> b) -> a -> b
$ Name -> DType
DConT Name
tyFunArrowName DType -> DType -> DType
`DAppT` DType
k1 DType -> DType -> DType
`DAppT` DType
k2
go [DTypeArg]
_ ty :: DType
ty@DLitT{} = DType -> m DType
forall (f :: * -> *) a. Applicative f => a -> f a
pure DType
ty
go [DTypeArg]
args DType
hd = String -> m DType
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> m DType) -> String -> m DType
forall a b. (a -> b) -> a -> b
$ String
"Illegal Haskell construct encountered:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"headed by: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DType -> String
forall a. Show a => a -> String
show DType
hd String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"applied to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [DTypeArg] -> String
forall a. Show a => a -> String
show [DTypeArg]
args
promoteTypeArg_NC :: MonadFail m => DTypeArg -> m DTypeArg
promoteTypeArg_NC :: 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 :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
t
promoteTypeArg_NC ta :: DTypeArg
ta@(DTyArg DType
_) = DTypeArg -> m DTypeArg
forall (f :: * -> *) a. Applicative f => a -> f a
pure DTypeArg
ta
promoteUnraveled :: MonadFail m
=> DType -> m ([DTyVarBndr], [DKind], DKind)
promoteUnraveled :: DType -> m ([DTyVarBndr], DCxt, DType)
promoteUnraveled DType
ty = do
([DTyVarBndr]
tvbs, DCxt
_, DCxt
arg_tys, DType
res_ty) <- DType -> m ([DTyVarBndr], DCxt, DCxt, DType)
forall (m :: * -> *).
MonadFail m =>
DType -> m ([DTyVarBndr], 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)
mapM DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DCxt
arg_tys
DType
res_ki <- DType -> m DType
forall (m :: * -> *). MonadFail m => DType -> m DType
promoteType_NC DType
res_ty
([DTyVarBndr], DCxt, DType) -> m ([DTyVarBndr], DCxt, DType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([DTyVarBndr]
tvbs, DCxt
arg_kis, DType
res_ki)