{-# LANGUAGE ScopedTypeVariables #-}
module Data.Singletons.Deriving.Infer ( inferConstraints, inferConstraintsDef ) where
import Language.Haskell.TH.Desugar
import Language.Haskell.TH.Syntax
import Data.Singletons.Deriving.Util
import Data.Singletons.Util
import Data.List (nub)
import Data.Maybe (fromJust)
inferConstraints :: forall q. DsMonad q => DPred -> DType -> [DCon] -> q DCxt
inferConstraints :: DPred -> DPred -> [DCon] -> q DCxt
inferConstraints DPred
pr DPred
inst_ty = (DCxt -> DCxt) -> q DCxt -> q DCxt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DCxt -> DCxt
forall a. Eq a => [a] -> [a]
nub (q DCxt -> q DCxt) -> ([DCon] -> q DCxt) -> [DCon] -> q DCxt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DCon -> q DCxt) -> [DCon] -> q DCxt
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM DCon -> q DCxt
infer_ct
where
infer_ct :: DCon -> q DCxt
infer_ct :: DCon -> q DCxt
infer_ct (DCon [DTyVarBndr]
_ DCxt
_ Name
_ DConFields
fields DPred
res_ty) = do
let field_tys :: DCxt
field_tys = DConFields -> DCxt
tysOfConFields DConFields
fields
eta_expanded_inst_ty :: DPred
eta_expanded_inst_ty
| Bool
is_functor_like = DPred
inst_ty DPred -> DPred -> DPred
`DAppT` Name -> DPred
DVarT (String -> Name
mkName String
"dummy")
| Bool
otherwise = DPred
inst_ty
DPred
res_ty' <- DPred -> q DPred
forall (q :: * -> *). DsMonad q => DPred -> q DPred
expandType DPred
res_ty
DPred
inst_ty' <- DPred -> q DPred
forall (q :: * -> *). DsMonad q => DPred -> q DPred
expandType DPred
eta_expanded_inst_ty
DCxt
field_tys' <- case IgnoreKinds -> DPred -> DPred -> Maybe DSubst
matchTy IgnoreKinds
YesIgnore DPred
res_ty' DPred
inst_ty' of
Maybe DSubst
Nothing -> String -> q DCxt
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> q DCxt) -> String -> q DCxt
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Unable to match type "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DPred -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 DPred
res_ty'
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" with "
ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> DPred -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 DPred
inst_ty'
ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
""
Just DSubst
subst -> (DPred -> q DPred) -> DCxt -> q DCxt
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (DSubst -> DPred -> q DPred
forall (q :: * -> *). Quasi q => DSubst -> DPred -> q DPred
substTy DSubst
subst) DCxt
field_tys
if Bool
is_functor_like
then DCxt -> DPred -> q DCxt
mk_functor_like_constraints DCxt
field_tys' DPred
res_ty'
else DCxt -> q DCxt
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DCxt -> q DCxt) -> DCxt -> q DCxt
forall a b. (a -> b) -> a -> b
$ (DPred -> DPred) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DPred
pr DPred -> DPred -> DPred
`DAppT`) DCxt
field_tys'
mk_functor_like_constraints :: [DType] -> DType -> q DCxt
mk_functor_like_constraints :: DCxt -> DPred -> q DCxt
mk_functor_like_constraints DCxt
fields DPred
res_ty = do
let (DPred
_, [DTypeArg]
res_ty_args) = DPred -> (DPred, [DTypeArg])
unfoldDType DPred
res_ty
(DCxt
_, DPred
last_res_ty_arg) = DCxt -> (DCxt, DPred)
forall a. [a] -> ([a], a)
snocView (DCxt -> (DCxt, DPred)) -> DCxt -> (DCxt, DPred)
forall a b. (a -> b) -> a -> b
$ [DTypeArg] -> DCxt
filterDTANormals [DTypeArg]
res_ty_args
last_tv :: Name
last_tv = Maybe Name -> Name
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Name -> Name) -> Maybe Name -> Name
forall a b. (a -> b) -> a -> b
$ DPred -> Maybe Name
getDVarTName_maybe DPred
last_res_ty_arg
DCxt
deep_subtypes <- (DPred -> q DCxt) -> DCxt -> q DCxt
forall (monad :: * -> *) monoid (t :: * -> *) a.
(Monad monad, Monoid monoid, Traversable t) =>
(a -> monad monoid) -> t a -> monad monoid
concatMapM (Name -> DPred -> q DCxt
forall (q :: * -> *). DsMonad q => Name -> DPred -> q DCxt
deepSubtypesContaining Name
last_tv) DCxt
fields
DCxt -> q DCxt
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DCxt -> q DCxt) -> DCxt -> q DCxt
forall a b. (a -> b) -> a -> b
$ (DPred -> DPred) -> DCxt -> DCxt
forall a b. (a -> b) -> [a] -> [b]
map (DPred
pr DPred -> DPred -> DPred
`DAppT`) DCxt
deep_subtypes
is_functor_like :: Bool
is_functor_like :: Bool
is_functor_like
| (DConT Name
pr_class_name, [DTypeArg]
_) <- DPred -> (DPred, [DTypeArg])
unfoldDType DPred
pr
= Name -> Bool
isFunctorLikeClassName Name
pr_class_name
| Bool
otherwise
= Bool
False
inferConstraintsDef :: DsMonad q => Maybe DCxt -> DPred -> DType -> [DCon] -> q DCxt
inferConstraintsDef :: Maybe DCxt -> DPred -> DPred -> [DCon] -> q DCxt
inferConstraintsDef Maybe DCxt
mb_ctxt DPred
pr DPred
inst_ty [DCon]
cons =
q DCxt -> (DCxt -> q DCxt) -> Maybe DCxt -> q DCxt
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (DPred -> DPred -> [DCon] -> q DCxt
forall (q :: * -> *).
DsMonad q =>
DPred -> DPred -> [DCon] -> q DCxt
inferConstraints DPred
pr DPred
inst_ty [DCon]
cons) DCxt -> q DCxt
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe DCxt
mb_ctxt