{-# LANGUAGE TemplateHaskellQuotes #-}
module Data.Singletons.TH.Promote.Defun where
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.TH.Names
import Data.Singletons.TH.Options
import Data.Singletons.TH.Promote.Monad
import Data.Singletons.TH.Promote.Type
import Data.Singletons.TH.Syntax
import Data.Singletons.TH.Util
import Control.Monad
import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import Data.Maybe
defunInfo :: DInfo -> PrM [DDec]
defunInfo :: DInfo -> PrM [DDec]
defunInfo (DTyConI DDec
dec Maybe [DDec]
_instances) = DDec -> PrM [DDec]
buildDefunSyms DDec
dec
defunInfo (DPrimTyConI Name
_name Int
_numArgs Bool
_unlifted) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DDec]) -> String -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ String
"Building defunctionalization symbols of primitive " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"type constructors not supported"
defunInfo (DVarI Name
_name DKind
_ty Maybe Name
_mdec) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of values not supported"
defunInfo (DTyVarI Name
_name DKind
_ty) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of type variables not supported"
defunInfo (DPatSynI {}) =
String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Building defunctionalization symbols of pattern synonyms not supported"
defunTopLevelTypeDecls ::
[TySynDecl]
-> [ClosedTypeFamilyDecl]
-> [OpenTypeFamilyDecl]
-> PrM ()
defunTopLevelTypeDecls :: [TySynDecl]
-> [ClosedTypeFamilyDecl] -> [OpenTypeFamilyDecl] -> PrM ()
defunTopLevelTypeDecls [TySynDecl]
ty_syns [ClosedTypeFamilyDecl]
c_tyfams [OpenTypeFamilyDecl]
o_tyfams = do
defun_ty_syns <-
(TySynDecl -> PrM [DDec]) -> [TySynDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (\(TySynDecl Name
name [DTyVarBndrVis]
tvbs DKind
rhs) -> Name -> [DTyVarBndrVis] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrVis]
tvbs DKind
rhs) [TySynDecl]
ty_syns
defun_c_tyfams <-
concatMapM (buildDefunSymsClosedTypeFamilyD . getTypeFamilyDecl) c_tyfams
defun_o_tyfams <-
concatMapM (buildDefunSymsOpenTypeFamilyD . getTypeFamilyDecl) o_tyfams
emitDecs $ defun_ty_syns ++ defun_c_tyfams ++ defun_o_tyfams
defunAssociatedTypeFamilies ::
[DTyVarBndrVis]
-> [OpenTypeFamilyDecl]
-> PrM ()
defunAssociatedTypeFamilies :: [DTyVarBndrVis] -> [OpenTypeFamilyDecl] -> PrM ()
defunAssociatedTypeFamilies [DTyVarBndrVis]
cls_tvbs [OpenTypeFamilyDecl]
atfs = do
defun_atfs <- (OpenTypeFamilyDecl -> PrM [DDec])
-> [OpenTypeFamilyDecl] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM OpenTypeFamilyDecl -> PrM [DDec]
defun [OpenTypeFamilyDecl]
atfs
emitDecs defun_atfs
where
defun :: OpenTypeFamilyDecl -> PrM [DDec]
defun :: OpenTypeFamilyDecl -> PrM [DDec]
defun (TypeFamilyDecl DTypeFamilyHead
tf_head) =
(DTyVarBndrVis -> DTyVarBndrVis)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrVis -> DTyVarBndrVis
ascribe_tf_tvb_kind Maybe DKind -> Maybe DKind
forall a. a -> a
id DTypeFamilyHead
tf_head
cls_tvb_kind_map :: Map Name DKind
cls_tvb_kind_map :: Map Name DKind
cls_tvb_kind_map = [(Name, DKind)] -> Map Name DKind
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrVis
tvb, DKind
tvb_kind)
| DTyVarBndrVis
tvb <- [DTyVarBndrVis]
cls_tvbs
, Just DKind
tvb_kind <- [DTyVarBndrVis -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrVis
tvb]
]
ascribe_tf_tvb_kind :: DTyVarBndrVis -> DTyVarBndrVis
ascribe_tf_tvb_kind :: DTyVarBndrVis -> DTyVarBndrVis
ascribe_tf_tvb_kind DTyVarBndrVis
tvb =
case DTyVarBndrVis
tvb of
DKindedTV{} -> DTyVarBndrVis
tvb
DPlainTV Name
n BndrVis
_ -> DTyVarBndrVis
-> (DKind -> DTyVarBndrVis) -> Maybe DKind -> DTyVarBndrVis
forall b a. b -> (a -> b) -> Maybe a -> b
maybe DTyVarBndrVis
tvb (Name -> BndrVis -> DKind -> DTyVarBndrVis
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
n BndrVis
BndrReq) (Maybe DKind -> DTyVarBndrVis) -> Maybe DKind -> DTyVarBndrVis
forall a b. (a -> b) -> a -> b
$ Name -> Map Name DKind -> Maybe DKind
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Name
n Map Name DKind
cls_tvb_kind_map
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms :: DDec -> PrM [DDec]
buildDefunSyms DDec
dec =
case DDec
dec of
DDataD DataFlavor
_new_or_data DCxt
_cxt Name
_tyName [DTyVarBndrVis]
_tvbs Maybe DKind
_k [DCon]
ctors [DDerivClause]
_derivings ->
[DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors
DClosedTypeFamilyD DTypeFamilyHead
tf_head [DTySynEqn]
_ ->
DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD DTypeFamilyHead
tf_head
DOpenTypeFamilyD DTypeFamilyHead
tf_head ->
DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD DTypeFamilyHead
tf_head
DTySynD Name
name [DTyVarBndrVis]
tvbs DKind
rhs ->
Name -> [DTyVarBndrVis] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrVis]
tvbs DKind
rhs
DClassD DCxt
_cxt Name
name [DTyVarBndrVis]
tvbs [FunDep]
_fundeps [DDec]
_members ->
Name -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrVis]
tvbs (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (Name -> DKind
DConT Name
constraintName))
DDec
_ -> String -> PrM [DDec]
forall a. String -> PrM a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> PrM [DDec]) -> String -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ String
"Defunctionalization symbols can only be built for " String -> String -> String
forall a. [a] -> [a] -> [a]
++
String
"type families and data declarations"
buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsClosedTypeFamilyD = (DTyVarBndrVis -> DTyVarBndrVis)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrVis -> DTyVarBndrVis
forall a. a -> a
id Maybe DKind -> Maybe DKind
forall a. a -> a
id
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD :: DTypeFamilyHead -> PrM [DDec]
buildDefunSymsOpenTypeFamilyD =
(DTyVarBndrVis -> DTyVarBndrVis)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrVis -> DTyVarBndrVis
forall flag. DTyVarBndr flag -> DTyVarBndr flag
defaultTvbToTypeKind (DKind -> Maybe DKind
forall a. a -> Maybe a
Just (DKind -> Maybe DKind)
-> (Maybe DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe DKind -> DKind
defaultMaybeToTypeKind)
buildDefunSymsTypeFamilyHead
:: (DTyVarBndrVis -> DTyVarBndrVis)
-> (Maybe DKind -> Maybe DKind)
-> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead :: (DTyVarBndrVis -> DTyVarBndrVis)
-> (Maybe DKind -> Maybe DKind) -> DTypeFamilyHead -> PrM [DDec]
buildDefunSymsTypeFamilyHead DTyVarBndrVis -> DTyVarBndrVis
default_tvb Maybe DKind -> Maybe DKind
default_kind
(DTypeFamilyHead Name
name [DTyVarBndrVis]
tvbs DFamilyResultSig
result_sig Maybe InjectivityAnn
_) = do
let arg_tvbs :: [DTyVarBndrVis]
arg_tvbs = (DTyVarBndrVis -> DTyVarBndrVis)
-> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a b. (a -> b) -> [a] -> [b]
map DTyVarBndrVis -> DTyVarBndrVis
default_tvb [DTyVarBndrVis]
tvbs
res_kind :: Maybe DKind
res_kind = Maybe DKind -> Maybe DKind
default_kind (DFamilyResultSig -> Maybe DKind
resultSigToMaybeKind DFamilyResultSig
result_sig)
Name -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrVis]
arg_tvbs Maybe DKind
res_kind
buildDefunSymsTySynD :: Name -> [DTyVarBndrVis] -> DType -> PrM [DDec]
buildDefunSymsTySynD :: Name -> [DTyVarBndrVis] -> DKind -> PrM [DDec]
buildDefunSymsTySynD Name
name [DTyVarBndrVis]
tvbs DKind
rhs = Name -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrVis]
tvbs Maybe DKind
mb_res_kind
where
mb_res_kind :: Maybe DKind
mb_res_kind :: Maybe DKind
mb_res_kind = case DKind
rhs of
DSigT DKind
_ DKind
k -> DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
k
DKind
_ -> Maybe DKind
forall a. Maybe a
Nothing
buildDefunSymsDataD :: [DCon] -> PrM [DDec]
buildDefunSymsDataD :: [DCon] -> PrM [DDec]
buildDefunSymsDataD [DCon]
ctors =
(DCon -> PrM [DDec]) -> [DCon] -> PrM [DDec]
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM DCon -> PrM [DDec]
promoteCtor [DCon]
ctors
where
promoteCtor :: DCon -> PrM [DDec]
promoteCtor :: DCon -> PrM [DDec]
promoteCtor (DCon [DTyVarBndrSpec]
tvbs DCxt
_ Name
name DConFields
fields DKind
res_ty) = do
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
let name' = Options -> Name -> Name
promotedDataTypeOrConName Options
opts Name
name
arg_tys = DConFields -> DCxt
tysOfConFields DConFields
fields
arg_kis <- traverse promoteType_NC arg_tys
res_ki <- promoteType_NC res_ty
let con_ki = [DTyVarBndrSpec] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndrSpec]
tvbs [] DCxt
arg_kis DKind
res_ki
m_fixity <- reifyFixityWithLocals name'
defunctionalize name' m_fixity $ DefunSAK con_ki
defunReify :: Name
-> [DTyVarBndrVis]
-> Maybe DKind
-> PrM [DDec]
defunReify :: Name -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defunReify Name
name [DTyVarBndrVis]
tvbs Maybe DKind
m_res_kind = do
m_fixity <- Name -> PrM (Maybe Fixity)
forall (q :: * -> *). DsMonad q => Name -> q (Maybe Fixity)
reifyFixityWithLocals Name
name
m_sak <- dsReifyType name
let defun = Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity
case m_sak of
Just DKind
sak -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ DKind -> DefunKindInfo
DefunSAK DKind
sak
Maybe DKind
Nothing -> DefunKindInfo -> PrM [DDec]
defun (DefunKindInfo -> PrM [DDec]) -> DefunKindInfo -> PrM [DDec]
forall a b. (a -> b) -> a -> b
$ [DTyVarBndrVis] -> Maybe DKind -> DefunKindInfo
DefunNoSAK [DTyVarBndrVis]
tvbs Maybe DKind
m_res_kind
defunctionalize :: Name
-> Maybe Fixity
-> DefunKindInfo
-> PrM [DDec]
defunctionalize :: Name -> Maybe Fixity -> DefunKindInfo -> PrM [DDec]
defunctionalize Name
name Maybe Fixity
m_fixity DefunKindInfo
defun_ki = do
case DefunKindInfo
defun_ki of
DefunSAK DKind
sak ->
case DKind -> Either String ([DTyVarBndrSpec], DCxt, DCxt, DKind)
unravelVanillaDType_either DKind
sak of
Left String
_ -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defun_fallback [] (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sak)
Right ([DTyVarBndrSpec]
sak_tvbs, DCxt
_sak_cxt, DCxt
sak_arg_kis, DKind
sak_res_ki)
-> [DTyVarBndrSpec] -> DCxt -> DKind -> PrM [DDec]
defun_vanilla_sak [DTyVarBndrSpec]
sak_tvbs DCxt
sak_arg_kis DKind
sak_res_ki
DefunNoSAK [DTyVarBndrVis]
tvbs Maybe DKind
m_res -> [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defun_fallback [DTyVarBndrVis]
tvbs Maybe DKind
m_res
where
defun_vanilla_sak :: [DTyVarBndrSpec] -> [DKind] -> DKind -> PrM [DDec]
defun_vanilla_sak :: [DTyVarBndrSpec] -> DCxt -> DKind -> PrM [DDec]
defun_vanilla_sak [DTyVarBndrSpec]
sak_tvbs DCxt
sak_arg_kis DKind
sak_res_ki = do
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
extra_name <- qNewName "arg"
let sak_arg_n = DCxt -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length DCxt
sak_arg_kis
arg_names <- replicateM sak_arg_n (noExactName <$> qNewName "a")
let
go :: Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go Int
n [(Name, DKind)]
arg_nks [(Name, DKind)]
res_nkss =
let arg_tvbs :: [DTyVarBndrVis]
arg_tvbs :: [DTyVarBndrVis]
arg_tvbs = ((Name, DKind) -> DTyVarBndrVis)
-> [(Name, DKind)] -> [DTyVarBndrVis]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
na, DKind
ki) -> Name -> BndrVis -> DKind -> DTyVarBndrVis
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
na BndrVis
BndrReq DKind
ki) [(Name, DKind)]
arg_nks
mk_sak_dec :: DKind -> DDec
mk_sak_dec :: DKind -> DDec
mk_sak_dec DKind
res_ki =
Name -> DKind -> DDec
DKiSigD (Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n) (DKind -> DDec) -> DKind -> DDec
forall a b. (a -> b) -> a -> b
$
[DTyVarBndrSpec] -> DCxt -> DCxt -> DKind -> DKind
ravelVanillaDType [DTyVarBndrSpec]
sak_tvbs [] (((Name, DKind) -> DKind) -> [(Name, DKind)] -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (Name, DKind) -> DKind
forall a b. (a, b) -> b
snd [(Name, DKind)]
arg_nks) DKind
res_ki in
case [(Name, DKind)]
res_nkss of
[] ->
let sat_sak_dec :: DDec
sat_sak_dec = DKind -> DDec
mk_sak_dec DKind
sak_res_ki
sak_tvbs' :: [DTyVarBndrSpec]
sak_tvbs' | [DTyVarBndrSpec] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [DTyVarBndrSpec]
sak_tvbs
= Specificity -> [DTyVarBndr ()] -> [DTyVarBndrSpec]
forall newFlag oldFlag.
newFlag -> [DTyVarBndr oldFlag] -> [DTyVarBndr newFlag]
changeDTVFlags Specificity
SpecifiedSpec ([DTyVarBndr ()] -> [DTyVarBndrSpec])
-> [DTyVarBndr ()] -> [DTyVarBndrSpec]
forall a b. (a -> b) -> a -> b
$
DCxt -> [DTyVarBndr ()]
toposortTyVarsOf (DCxt
sak_arg_kis DCxt -> DCxt -> DCxt
forall a. [a] -> [a] -> [a]
++ [DKind
sak_res_ki])
| Bool
otherwise
= [DTyVarBndrSpec]
sak_tvbs
sat_decs :: [DDec]
sat_decs = Options
-> Int
-> [DTyVarBndrSpec]
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrSpec]
sak_tvbs' [DTyVarBndrVis]
arg_tvbs (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
sak_res_ki)
in (DKind
sak_res_ki, DDec
sat_sak_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
sat_decs)
(Name, DKind)
res_nk:[(Name, DKind)]
res_nks ->
let (DKind
res_ki, [DDec]
decs) = Int -> [(Name, DKind)] -> [(Name, DKind)] -> (DKind, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([(Name, DKind)]
arg_nks [(Name, DKind)] -> [(Name, DKind)] -> [(Name, DKind)]
forall a. [a] -> [a] -> [a]
++ [(Name, DKind)
res_nk]) [(Name, DKind)]
res_nks
tyfun :: DKind
tyfun = DKind -> DKind -> DKind
buildTyFunArrow ((Name, DKind) -> DKind
forall a b. (a, b) -> b
snd (Name, DKind)
res_nk) DKind
res_ki
defun_sak_dec :: DDec
defun_sak_dec = DKind -> DDec
mk_sak_dec DKind
tyfun
defun_other_decs :: [DDec]
defun_other_decs = Options
-> Int
-> Int
-> [DTyVarBndrVis]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
sak_arg_n
[DTyVarBndrVis]
arg_tvbs ((Name, DKind) -> Name
forall a b. (a, b) -> a
fst (Name, DKind)
res_nk)
Name
extra_name (DKind -> Maybe DKind
forall a. a -> Maybe a
Just DKind
tyfun)
in (DKind
tyfun, DDec
defun_sak_decDDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
:[DDec]
defun_other_decs [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)
pure $ snd $ go 0 [] $ zip arg_names sak_arg_kis
defun_fallback :: [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defun_fallback :: [DTyVarBndrVis] -> Maybe DKind -> PrM [DDec]
defun_fallback [DTyVarBndrVis]
tvbs' Maybe DKind
m_res' = do
opts <- PrM Options
forall (m :: * -> *). OptionsMonad m => m Options
getOptions
extra_name <- qNewName "arg"
(tvbs, m_res) <- eta_expand (noExactTyVars tvbs') (noExactTyVars m_res')
let tvbs_n = [DTyVarBndrVis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [DTyVarBndrVis]
tvbs
go :: Int -> [DTyVarBndrVis] -> [DTyVarBndrVis] -> (Maybe DKind, [DDec])
go Int
n [DTyVarBndrVis]
arg_tvbs [DTyVarBndrVis]
res_tvbss =
case [DTyVarBndrVis]
res_tvbss of
[] ->
let sat_decs :: [DDec]
sat_decs = Options
-> Int
-> [DTyVarBndrSpec]
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DDec]
mk_sat_decs Options
opts Int
n [] [DTyVarBndrVis]
arg_tvbs Maybe DKind
m_res
in (Maybe DKind
m_res, [DDec]
sat_decs)
DTyVarBndrVis
res_tvb:[DTyVarBndrVis]
res_tvbs ->
let (Maybe DKind
m_res_ki, [DDec]
decs) = Int -> [DTyVarBndrVis] -> [DTyVarBndrVis] -> (Maybe DKind, [DDec])
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) ([DTyVarBndrVis]
arg_tvbs [DTyVarBndrVis] -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrVis
res_tvb]) [DTyVarBndrVis]
res_tvbs
m_tyfun :: Maybe DKind
m_tyfun = Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe (DTyVarBndrVis -> Maybe DKind
forall flag. DTyVarBndr flag -> Maybe DKind
extractTvbKind DTyVarBndrVis
res_tvb)
Maybe DKind
m_res_ki
defun_decs' :: [DDec]
defun_decs' = Options
-> Int
-> Int
-> [DTyVarBndrVis]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
tvbs_n [DTyVarBndrVis]
arg_tvbs
(DTyVarBndrVis -> Name
forall flag. DTyVarBndr flag -> Name
extractTvbName DTyVarBndrVis
res_tvb)
Name
extra_name Maybe DKind
m_tyfun
in (Maybe DKind
m_tyfun, [DDec]
defun_decs' [DDec] -> [DDec] -> [DDec]
forall a. [a] -> [a] -> [a]
++ [DDec]
decs)
pure $ snd $ go 0 [] tvbs
mk_defun_decs :: Options
-> Int
-> Int
-> [DTyVarBndrVis]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs :: Options
-> Int
-> Int
-> [DTyVarBndrVis]
-> Name
-> Name
-> Maybe DKind
-> [DDec]
mk_defun_decs Options
opts Int
n Int
fully_sat_n [DTyVarBndrVis]
arg_tvbs Name
tyfun_name Name
extra_name Maybe DKind
m_tyfun =
let data_name :: Name
data_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n
next_name :: Name
next_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
con_name :: Name
con_name = String -> String -> Name -> Name
prefixName String
"" String
":" (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ String -> String -> Name -> Name
suffixName String
"KindInference" String
"###" Name
data_name
params :: [DTyVarBndrVis]
params = [DTyVarBndrVis]
arg_tvbs [DTyVarBndrVis] -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. [a] -> [a] -> [a]
++ [Name -> BndrVis -> DTyVarBndrVis
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
tyfun_name BndrVis
BndrReq]
con_eq_ct :: DKind
con_eq_ct = Name -> DKind
DConT Name
sameKindName DKind -> DKind -> DKind
`DAppT` DKind
lhs DKind -> DKind -> DKind
`DAppT` DKind
rhs
where
lhs :: DKind
lhs = DKind
app_data_ty DKind -> DKind -> DKind
`apply` Name -> DKind
DVarT Name
extra_name
rhs :: DKind
rhs = DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
next_name)
([DTyVarBndrVis]
arg_tvbs [DTyVarBndrVis] -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. [a] -> [a] -> [a]
++ [Name -> BndrVis -> DTyVarBndrVis
forall flag. Name -> flag -> DTyVarBndr flag
DPlainTV Name
extra_name BndrVis
BndrReq])
con_decl :: DCon
con_decl = [DTyVarBndrSpec] -> DCxt -> Name -> DConFields -> DKind -> DCon
DCon [] [DKind
con_eq_ct] Name
con_name (Bool -> [DBangType] -> DConFields
DNormalC Bool
False [])
(DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
data_name) [DTyVarBndrVis]
params)
data_decl :: DDec
data_decl = DataFlavor
-> DCxt
-> Name
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DCon]
-> [DDerivClause]
-> DDec
DDataD DataFlavor
Data [] Name
data_name [DTyVarBndrVis]
args Maybe DKind
m_tyfun [DCon
con_decl] []
where
args :: [DTyVarBndrVis]
args | Maybe DKind -> Bool
forall a. Maybe a -> Bool
isJust Maybe DKind
m_tyfun = [DTyVarBndrVis]
arg_tvbs
| Bool
otherwise = [DTyVarBndrVis]
params
app_data_ty :: DKind
app_data_ty = DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
data_name) [DTyVarBndrVis]
arg_tvbs
app_eqn :: DTySynEqn
app_eqn = Maybe [DTyVarBndr ()] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr ()]
forall a. Maybe a
Nothing
(Name -> DKind
DConT Name
applyName DKind -> DKind -> DKind
`DAppT` DKind
app_data_ty
DKind -> DKind -> DKind
`DAppT` Name -> DKind
DVarT Name
tyfun_name)
(DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
app_eqn_rhs_name) [DTyVarBndrVis]
params)
app_eqn_rhs_name :: Name
app_eqn_rhs_name | Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
fully_sat_n = Name
name
| Bool
otherwise = Name
next_name
app_decl :: DDec
app_decl = DTySynEqn -> DDec
DTySynInstD DTySynEqn
app_eqn
suppress :: DDec
suppress = Maybe Overlap
-> Maybe [DTyVarBndr ()] -> DCxt -> DKind -> [DDec] -> DDec
DInstanceD Maybe Overlap
forall a. Maybe a
Nothing Maybe [DTyVarBndr ()]
forall a. Maybe a
Nothing []
(Name -> DKind
DConT Name
suppressClassName DKind -> DKind -> DKind
`DAppT` DKind
app_data_ty)
[DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Name -> [DClause] -> DLetDec
DFunD Name
suppressMethodName
[[DPat] -> DExp -> DClause
DClause []
((Name -> DExp
DVarE 'snd) DExp -> DExp -> DExp
`DAppE`
[DExp] -> DExp
mkTupleDExp [Name -> DExp
DConE Name
con_name,
[DExp] -> DExp
mkTupleDExp []])]]
fixity_decl :: [DDec]
fixity_decl = Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec]
forall a b. (a -> b) -> a -> b
$ (Fixity -> DDec) -> Maybe Fixity -> 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 -> Fixity -> DDec
mk_fix_decl Name
data_name) Maybe Fixity
m_fixity
in DDec
data_decl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: DDec
app_decl DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: DDec
suppress DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: [DDec]
fixity_decl
mk_sat_decs ::
Options
-> Int
-> [DTyVarBndrSpec]
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DDec]
mk_sat_decs :: Options
-> Int
-> [DTyVarBndrSpec]
-> [DTyVarBndrVis]
-> Maybe DKind
-> [DDec]
mk_sat_decs Options
opts Int
n [DTyVarBndrSpec]
sat_tvbs [DTyVarBndrVis]
sat_args Maybe DKind
m_sat_res =
let sat_name :: Name
sat_name = Options -> Name -> Int -> Name
defunctionalizedName Options
opts Name
name Int
n
sat_dec :: DDec
sat_dec = DTypeFamilyHead -> [DTySynEqn] -> DDec
DClosedTypeFamilyD
(Name
-> [DTyVarBndrVis]
-> DFamilyResultSig
-> Maybe InjectivityAnn
-> DTypeFamilyHead
DTypeFamilyHead Name
sat_name
([DTyVarBndrSpec] -> [DTyVarBndrVis]
tvbSpecsToBndrVis [DTyVarBndrSpec]
sat_tvbs [DTyVarBndrVis] -> [DTyVarBndrVis] -> [DTyVarBndrVis]
forall a. [a] -> [a] -> [a]
++ [DTyVarBndrVis]
sat_args)
(Maybe DKind -> DFamilyResultSig
maybeKindToResultSig Maybe DKind
m_sat_res) Maybe InjectivityAnn
forall a. Maybe a
Nothing)
[Maybe [DTyVarBndr ()] -> DKind -> DKind -> DTySynEqn
DTySynEqn Maybe [DTyVarBndr ()]
forall a. Maybe a
Nothing
(DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
sat_name) [DTyVarBndrVis]
sat_args)
(DKind -> [DTyVarBndrVis] -> DKind
foldTypeTvbs (Name -> DKind
DConT Name
name) [DTyVarBndrVis]
sat_args)]
sat_fixity_dec :: [DDec]
sat_fixity_dec = Maybe DDec -> [DDec]
forall a. Maybe a -> [a]
maybeToList (Maybe DDec -> [DDec]) -> Maybe DDec -> [DDec]
forall a b. (a -> b) -> a -> b
$ (Fixity -> DDec) -> Maybe Fixity -> 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 -> Fixity -> DDec
mk_fix_decl Name
sat_name) Maybe Fixity
m_fixity
in DDec
sat_dec DDec -> [DDec] -> [DDec]
forall a. a -> [a] -> [a]
: [DDec]
sat_fixity_dec
eta_expand :: [DTyVarBndrVis] -> Maybe DKind -> PrM ([DTyVarBndrVis], Maybe DKind)
eta_expand :: [DTyVarBndrVis]
-> Maybe DKind -> PrM ([DTyVarBndrVis], Maybe DKind)
eta_expand [DTyVarBndrVis]
m_arg_tvbs Maybe DKind
Nothing = ([DTyVarBndrVis], Maybe DKind)
-> PrM ([DTyVarBndrVis], Maybe DKind)
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([DTyVarBndrVis]
m_arg_tvbs, Maybe DKind
forall a. Maybe a
Nothing)
eta_expand [DTyVarBndrVis]
m_arg_tvbs (Just DKind
res_kind) = do
let (DFunArgs
arg_ks, DKind
result_k) = DKind -> (DFunArgs, DKind)
unravelDType DKind
res_kind
vis_arg_ks :: [DVisFunArg]
vis_arg_ks = DFunArgs -> [DVisFunArg]
filterDVisFunArgs DFunArgs
arg_ks
extra_arg_tvbs <- (DVisFunArg -> PrM DTyVarBndrVis)
-> [DVisFunArg] -> PrM [DTyVarBndrVis]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DVisFunArg -> PrM DTyVarBndrVis
mk_extra_tvb [DVisFunArg]
vis_arg_ks
pure (m_arg_tvbs ++ extra_arg_tvbs, Just result_k)
mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrVis
mk_extra_tvb :: DVisFunArg -> PrM DTyVarBndrVis
mk_extra_tvb DVisFunArg
vfa =
case DVisFunArg
vfa of
DVisFADep DTyVarBndr ()
tvb -> DTyVarBndrVis -> PrM DTyVarBndrVis
forall a. a -> PrM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BndrVis
BndrReq BndrVis -> DTyVarBndr () -> DTyVarBndrVis
forall a b. a -> DTyVarBndr b -> DTyVarBndr a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ DTyVarBndr ()
tvb)
DVisFAAnon DKind
k -> (\Name
n -> Name -> BndrVis -> DKind -> DTyVarBndrVis
forall flag. Name -> flag -> DKind -> DTyVarBndr flag
DKindedTV Name
n BndrVis
BndrReq DKind
k) (Name -> DTyVarBndrVis) -> PrM Name -> PrM DTyVarBndrVis
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(Name -> Name
noExactName (Name -> Name) -> PrM Name -> PrM Name
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> PrM Name
forall (m :: * -> *). Quasi m => String -> m Name
qNewName String
"e")
mk_fix_decl :: Name -> Fixity -> DDec
mk_fix_decl :: Name -> Fixity -> DDec
mk_fix_decl Name
n Fixity
f = DLetDec -> DDec
DLetDec (DLetDec -> DDec) -> DLetDec -> DDec
forall a b. (a -> b) -> a -> b
$ Fixity -> NamespaceSpecifier -> Name -> DLetDec
DInfixD Fixity
f NamespaceSpecifier
NoNamespaceSpecifier Name
n
data DefunKindInfo
= DefunSAK DKind
| DefunNoSAK [DTyVarBndrVis] (Maybe DKind)
buildTyFunArrow :: DKind -> DKind -> DKind
buildTyFunArrow :: DKind -> DKind -> DKind
buildTyFunArrow DKind
k1 DKind
k2 = Name -> DKind
DConT Name
tyFunArrowName DKind -> DKind -> DKind
`DAppT` DKind
k1 DKind -> DKind -> DKind
`DAppT` DKind
k2
buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe :: Maybe DKind -> Maybe DKind -> Maybe DKind
buildTyFunArrow_maybe Maybe DKind
m_k1 Maybe DKind
m_k2 = DKind -> DKind -> DKind
buildTyFunArrow (DKind -> DKind -> DKind) -> Maybe DKind -> Maybe (DKind -> DKind)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe DKind
m_k1 Maybe (DKind -> DKind) -> Maybe DKind -> Maybe DKind
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe DKind
m_k2