{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Deriv.Infer
( inferConstraints
, simplifyInstanceContexts
)
where
import GHC.Prelude
import GHC.Tc.Deriv.Utils
import GHC.Tc.Utils.Env
import GHC.Tc.Deriv.Generate
import GHC.Tc.Deriv.Functor
import GHC.Tc.Deriv.Generics
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
import GHC.Tc.Utils.TcType
import GHC.Tc.Solver
import GHC.Tc.Solver.Monad ( runTcS )
import GHC.Tc.Validity (validDerivPred)
import GHC.Tc.Utils.Unify (buildImplicationFor)
import GHC.Core.Class
import GHC.Core.DataCon
import GHC.Core.TyCon
import GHC.Core.TyCo.Ppr (pprTyVars)
import GHC.Core.Type
import GHC.Core.Predicate
import GHC.Core.Unify (tcUnifyTy)
import GHC.Data.Pair
import GHC.Builtin.Names
import GHC.Builtin.Types (typeToTypeKind)
import GHC.Utils.Error
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Utils.Misc
import GHC.Types.Basic
import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Data.Bag
import Control.Monad
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Reader (ask)
import Data.Function (on)
import Data.Functor.Classes (liftEq)
import Data.List (sortBy)
import Data.Maybe
inferConstraints :: DerivSpecMechanism
-> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)
inferConstraints :: DerivSpecMechanism
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
inferConstraints DerivSpecMechanism
mechanism
= do { DerivEnv { denv_tvs :: DerivEnv -> [TcTyVar]
denv_tvs = [TcTyVar]
tvs
, denv_cls :: DerivEnv -> Class
denv_cls = Class
main_cls
, denv_inst_tys :: DerivEnv -> ThetaType
denv_inst_tys = ThetaType
inst_tys } <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
; Bool
wildcard <- DerivM Bool
isStandaloneWildcardDeriv
; let infer_constraints :: DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)
infer_constraints :: DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
infer_constraints =
case DerivSpecMechanism
mechanism of
DerivSpecStock{dsm_stock_dit :: DerivSpecMechanism -> DerivInstTys
dsm_stock_dit = DerivInstTys
dit}
-> do (ThetaSpec
thetas, [TcTyVar]
tvs, ThetaType
inst_tys, DerivInstTys
dit') <- DerivInstTys
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivInstTys)
inferConstraintsStock DerivInstTys
dit
forall (f :: * -> *) a. Applicative f => a -> f a
pure ( ThetaSpec
thetas, [TcTyVar]
tvs, ThetaType
inst_tys
, DerivSpecMechanism
mechanism{dsm_stock_dit :: DerivInstTys
dsm_stock_dit = DerivInstTys
dit'} )
DerivSpecMechanism
DerivSpecAnyClass
-> DerivM ThetaSpec
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
infer_constraints_simple DerivM ThetaSpec
inferConstraintsAnyclass
DerivSpecNewtype { dsm_newtype_dit :: DerivSpecMechanism -> DerivInstTys
dsm_newtype_dit =
DerivInstTys{dit_cls_tys :: DerivInstTys -> ThetaType
dit_cls_tys = ThetaType
cls_tys}
, dsm_newtype_rep_ty :: DerivSpecMechanism -> PredType
dsm_newtype_rep_ty = PredType
rep_ty }
-> DerivM ThetaSpec
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
infer_constraints_simple forall a b. (a -> b) -> a -> b
$
ThetaType -> PredType -> DerivM ThetaSpec
inferConstraintsCoerceBased ThetaType
cls_tys PredType
rep_ty
DerivSpecVia { dsm_via_cls_tys :: DerivSpecMechanism -> ThetaType
dsm_via_cls_tys = ThetaType
cls_tys
, dsm_via_ty :: DerivSpecMechanism -> PredType
dsm_via_ty = PredType
via_ty }
-> DerivM ThetaSpec
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
infer_constraints_simple forall a b. (a -> b) -> a -> b
$
ThetaType -> PredType -> DerivM ThetaSpec
inferConstraintsCoerceBased ThetaType
cls_tys PredType
via_ty
infer_constraints_simple
:: DerivM ThetaSpec
-> DerivM (ThetaSpec, [TyVar], [TcType], DerivSpecMechanism)
infer_constraints_simple :: DerivM ThetaSpec
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
infer_constraints_simple DerivM ThetaSpec
infer_thetas = do
ThetaSpec
thetas <- DerivM ThetaSpec
infer_thetas
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ThetaSpec
thetas, [TcTyVar]
tvs, ThetaType
inst_tys, DerivSpecMechanism
mechanism)
cls_tvs :: [TcTyVar]
cls_tvs = Class -> [TcTyVar]
classTyVars Class
main_cls
sc_constraints :: ThetaSpec
sc_constraints = forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (forall a b. [a] -> [b] -> Bool
equalLength [TcTyVar]
cls_tvs ThetaType
inst_tys)
(forall a. Outputable a => a -> SDoc
ppr Class
main_cls forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_tys) forall a b. (a -> b) -> a -> b
$
CtOrigin -> TypeOrKind -> ThetaType -> ThetaSpec
mkDirectThetaSpec
(Bool -> CtOrigin
mkDerivOrigin Bool
wildcard) TypeOrKind
TypeLevel
(HasDebugCallStack => Subst -> ThetaType -> ThetaType
substTheta Subst
cls_subst (Class -> ThetaType
classSCTheta Class
main_cls))
cls_subst :: Subst
cls_subst = forall a. HasCallStack => Bool -> a -> a
assert (forall a b. [a] -> [b] -> Bool
equalLength [TcTyVar]
cls_tvs ThetaType
inst_tys) forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => [TcTyVar] -> ThetaType -> Subst
zipTvSubst [TcTyVar]
cls_tvs ThetaType
inst_tys
; (ThetaSpec
inferred_constraints, [TcTyVar]
tvs', ThetaType
inst_tys', DerivSpecMechanism
mechanism')
<- DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivSpecMechanism)
infer_constraints
; forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcRn ()
traceTc String
"inferConstraints" forall a b. (a -> b) -> a -> b
$ forall doc. IsDoc doc => [doc] -> doc
vcat
[ forall a. Outputable a => a -> SDoc
ppr Class
main_cls forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_tys'
, forall a. Outputable a => a -> SDoc
ppr ThetaSpec
inferred_constraints
]
; forall (m :: * -> *) a. Monad m => a -> m a
return ( ThetaSpec
sc_constraints forall a. [a] -> [a] -> [a]
++ ThetaSpec
inferred_constraints
, [TcTyVar]
tvs', ThetaType
inst_tys', DerivSpecMechanism
mechanism' ) }
inferConstraintsStock :: DerivInstTys
-> DerivM (ThetaSpec, [TyVar], [TcType], DerivInstTys)
inferConstraintsStock :: DerivInstTys
-> DerivM (ThetaSpec, [TcTyVar], ThetaType, DerivInstTys)
inferConstraintsStock dit :: DerivInstTys
dit@(DerivInstTys { dit_cls_tys :: DerivInstTys -> ThetaType
dit_cls_tys = ThetaType
cls_tys
, dit_tc :: DerivInstTys -> TyCon
dit_tc = TyCon
tc
, dit_tc_args :: DerivInstTys -> ThetaType
dit_tc_args = ThetaType
tc_args
, dit_rep_tc :: DerivInstTys -> TyCon
dit_rep_tc = TyCon
rep_tc
, dit_rep_tc_args :: DerivInstTys -> ThetaType
dit_rep_tc_args = ThetaType
rep_tc_args })
= do DerivEnv { denv_tvs :: DerivEnv -> [TcTyVar]
denv_tvs = [TcTyVar]
tvs
, denv_cls :: DerivEnv -> Class
denv_cls = Class
main_cls
, denv_inst_tys :: DerivEnv -> ThetaType
denv_inst_tys = ThetaType
inst_tys } <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
Bool
wildcard <- DerivM Bool
isStandaloneWildcardDeriv
let inst_ty :: PredType
inst_ty = TyCon -> ThetaType -> PredType
mkTyConApp TyCon
tc ThetaType
tc_args
tc_binders :: [TyConBinder]
tc_binders = TyCon -> [TyConBinder]
tyConBinders TyCon
rep_tc
choose_level :: TyConBinder -> TypeOrKind
choose_level TyConBinder
bndr
| TyConBinder -> Bool
isNamedTyConBinder TyConBinder
bndr = TypeOrKind
KindLevel
| Bool
otherwise = TypeOrKind
TypeLevel
t_or_ks :: [TypeOrKind]
t_or_ks = forall a b. (a -> b) -> [a] -> [b]
map TyConBinder -> TypeOrKind
choose_level [TyConBinder]
tc_binders forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat TypeOrKind
TypeLevel
con_arg_constraints
:: ([TyVar] -> CtOrigin
-> TypeOrKind
-> Type
-> [(ThetaSpec, Maybe Subst)])
-> (ThetaSpec, [TyVar], [TcType], DerivInstTys)
con_arg_constraints :: ([TcTyVar]
-> CtOrigin
-> TypeOrKind
-> PredType
-> [(ThetaSpec, Maybe Subst)])
-> (ThetaSpec, [TcTyVar], ThetaType, DerivInstTys)
con_arg_constraints [TcTyVar]
-> CtOrigin -> TypeOrKind -> PredType -> [(ThetaSpec, Maybe Subst)]
get_arg_constraints
= let
([ThetaSpec]
predss, [Maybe Subst]
mbSubsts) = forall a b. [(a, b)] -> ([a], [b])
unzip
[ (ThetaSpec, Maybe Subst)
preds_and_mbSubst
| DataCon
data_con <- TyCon -> [DataCon]
tyConDataCons TyCon
rep_tc
, (Int
arg_n, TypeOrKind
arg_t_or_k, PredType
arg_ty)
<- forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
1..] [TypeOrKind]
t_or_ks forall a b. (a -> b) -> a -> b
$
DataCon -> DerivInstTys -> ThetaType
derivDataConInstArgTys DataCon
data_con DerivInstTys
dit
, Bool -> Bool
not (HasDebugCallStack => PredType -> Bool
isUnliftedType PredType
arg_ty)
, let orig :: CtOrigin
orig = DataCon -> Int -> Bool -> CtOrigin
DerivOriginDC DataCon
data_con Int
arg_n Bool
wildcard
, (ThetaSpec, Maybe Subst)
preds_and_mbSubst
<- [TcTyVar]
-> CtOrigin -> TypeOrKind -> PredType -> [(ThetaSpec, Maybe Subst)]
get_arg_constraints (DataCon -> [TcTyVar]
dataConUnivTyVars DataCon
data_con)
CtOrigin
orig TypeOrKind
arg_t_or_k PredType
arg_ty
]
stupid_theta :: ThetaType
stupid_theta =
[ HasDebugCallStack => [TcTyVar] -> ThetaType -> PredType -> PredType
substTyWith (DataCon -> [TcTyVar]
dataConUnivTyVars DataCon
data_con)
(DataCon -> ThetaType -> ThetaType
dataConInstUnivs DataCon
data_con ThetaType
rep_tc_args)
PredType
stupid_pred
| DataCon
data_con <- TyCon -> [DataCon]
tyConDataCons TyCon
rep_tc
, PredType
stupid_pred <- DataCon -> ThetaType
dataConStupidTheta DataCon
data_con
]
preds :: ThetaSpec
preds = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ThetaSpec]
predss
subst :: Subst
subst = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Subst -> Subst -> Subst
composeTCvSubst
Subst
emptySubst (forall a. [Maybe a] -> [a]
catMaybes [Maybe Subst]
mbSubsts)
unmapped_tvs :: [TcTyVar]
unmapped_tvs = forall a. (a -> Bool) -> [a] -> [a]
filter (\TcTyVar
v -> TcTyVar
v TcTyVar -> Subst -> Bool
`notElemSubst` Subst
subst
Bool -> Bool -> Bool
&& Bool -> Bool
not (TcTyVar
v TcTyVar -> Subst -> Bool
`isInScope` Subst
subst)) [TcTyVar]
tvs
(Subst
subst', [TcTyVar]
_) = HasDebugCallStack => Subst -> [TcTyVar] -> (Subst, [TcTyVar])
substTyVarBndrs Subst
subst [TcTyVar]
unmapped_tvs
stupid_theta_origin :: ThetaSpec
stupid_theta_origin = CtOrigin -> TypeOrKind -> ThetaType -> ThetaSpec
mkDirectThetaSpec
CtOrigin
deriv_origin TypeOrKind
TypeLevel
(HasDebugCallStack => Subst -> ThetaType -> ThetaType
substTheta Subst
subst' ThetaType
stupid_theta)
preds' :: ThetaSpec
preds' = forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => Subst -> PredSpec -> PredSpec
substPredSpec Subst
subst') ThetaSpec
preds
inst_tys' :: ThetaType
inst_tys' = HasDebugCallStack => Subst -> ThetaType -> ThetaType
substTys Subst
subst' ThetaType
inst_tys
dit' :: DerivInstTys
dit' = Subst -> DerivInstTys -> DerivInstTys
substDerivInstTys Subst
subst' DerivInstTys
dit
tvs' :: [TcTyVar]
tvs' = ThetaType -> [TcTyVar]
tyCoVarsOfTypesWellScoped ThetaType
inst_tys'
in ( ThetaSpec
stupid_theta_origin forall a. [a] -> [a] -> [a]
++ ThetaSpec
preds'
, [TcTyVar]
tvs', ThetaType
inst_tys', DerivInstTys
dit' )
is_generic :: Bool
is_generic = Class
main_cls forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
genClassKey
is_generic1 :: Bool
is_generic1 = Class
main_cls forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
gen1ClassKey
is_functor_like :: Bool
is_functor_like = HasDebugCallStack => PredType -> PredType
typeKind PredType
inst_ty HasDebugCallStack => PredType -> PredType -> Bool
`tcEqKind` PredType
typeToTypeKind
Bool -> Bool -> Bool
|| Bool
is_generic1
get_gen1_constraints ::
Class
-> [TyVar]
-> CtOrigin -> TypeOrKind -> Type
-> [(ThetaSpec, Maybe Subst)]
get_gen1_constraints :: Class
-> [TcTyVar]
-> CtOrigin
-> TypeOrKind
-> PredType
-> [(ThetaSpec, Maybe Subst)]
get_gen1_constraints Class
functor_cls [TcTyVar]
dc_univs CtOrigin
orig TypeOrKind
t_or_k PredType
ty
= CtOrigin
-> TypeOrKind -> Class -> ThetaType -> [(ThetaSpec, Maybe Subst)]
mk_functor_like_constraints CtOrigin
orig TypeOrKind
t_or_k Class
functor_cls forall a b. (a -> b) -> a -> b
$
TcTyVar -> PredType -> ThetaType
get_gen1_constrained_tys TcTyVar
last_dc_univ PredType
ty
where
last_dc_univ :: TcTyVar
last_dc_univ = forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
dc_univs)) forall a b. (a -> b) -> a -> b
$
forall a. [a] -> a
last [TcTyVar]
dc_univs
get_std_constrained_tys ::
[TyVar]
-> CtOrigin -> TypeOrKind -> Type
-> [(ThetaSpec, Maybe Subst)]
get_std_constrained_tys :: [TcTyVar]
-> CtOrigin -> TypeOrKind -> PredType -> [(ThetaSpec, Maybe Subst)]
get_std_constrained_tys [TcTyVar]
dc_univs CtOrigin
orig TypeOrKind
t_or_k PredType
ty
| Bool
is_functor_like
= CtOrigin
-> TypeOrKind -> Class -> ThetaType -> [(ThetaSpec, Maybe Subst)]
mk_functor_like_constraints CtOrigin
orig TypeOrKind
t_or_k Class
main_cls forall a b. (a -> b) -> a -> b
$
TcTyVar -> PredType -> ThetaType
deepSubtypesContaining TcTyVar
last_dc_univ PredType
ty
| Bool
otherwise
= [( [CtOrigin -> TypeOrKind -> Class -> PredType -> PredSpec
mk_cls_pred CtOrigin
orig TypeOrKind
t_or_k Class
main_cls PredType
ty]
, forall a. Maybe a
Nothing )]
where
last_dc_univ :: TcTyVar
last_dc_univ = forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
dc_univs)) forall a b. (a -> b) -> a -> b
$
forall a. [a] -> a
last [TcTyVar]
dc_univs
mk_functor_like_constraints :: CtOrigin -> TypeOrKind
-> Class -> [Type]
-> [(ThetaSpec, Maybe Subst)]
mk_functor_like_constraints :: CtOrigin
-> TypeOrKind -> Class -> ThetaType -> [(ThetaSpec, Maybe Subst)]
mk_functor_like_constraints CtOrigin
orig TypeOrKind
t_or_k Class
cls
= forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a -> b) -> a -> b
$ \PredType
ty -> let ki :: PredType
ki = HasDebugCallStack => PredType -> PredType
typeKind PredType
ty in
( [ CtOrigin -> TypeOrKind -> Class -> PredType -> PredSpec
mk_cls_pred CtOrigin
orig TypeOrKind
t_or_k Class
cls PredType
ty
, SimplePredSpec
{ sps_pred :: PredType
sps_pred = PredType -> PredType -> PredType
mkPrimEqPred PredType
ki PredType
typeToTypeKind
, sps_origin :: CtOrigin
sps_origin = CtOrigin
orig
, sps_type_or_kind :: TypeOrKind
sps_type_or_kind = TypeOrKind
KindLevel
}
]
, PredType -> PredType -> Maybe Subst
tcUnifyTy PredType
ki PredType
typeToTypeKind
)
extra_constraints :: ThetaSpec
extra_constraints
| Class
main_cls forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
dataClassKey
, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PredType -> Bool
isLiftedTypeKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasDebugCallStack => PredType -> PredType
typeKind) ThetaType
rep_tc_args
= [ CtOrigin -> TypeOrKind -> Class -> PredType -> PredSpec
mk_cls_pred CtOrigin
deriv_origin TypeOrKind
t_or_k Class
main_cls PredType
ty
| (TypeOrKind
t_or_k, PredType
ty) <- forall a b. [a] -> [b] -> [(a, b)]
zip [TypeOrKind]
t_or_ks ThetaType
rep_tc_args]
| Bool
otherwise
= []
mk_cls_pred :: CtOrigin -> TypeOrKind -> Class -> PredType -> PredSpec
mk_cls_pred CtOrigin
orig TypeOrKind
t_or_k Class
cls PredType
ty
= SimplePredSpec
{ sps_pred :: PredType
sps_pred = Class -> ThetaType -> PredType
mkClassPred Class
cls (ThetaType
cls_tys' forall a. [a] -> [a] -> [a]
++ [PredType
ty])
, sps_origin :: CtOrigin
sps_origin = CtOrigin
orig
, sps_type_or_kind :: TypeOrKind
sps_type_or_kind = TypeOrKind
t_or_k
}
cls_tys' :: ThetaType
cls_tys' | Bool
is_generic1 = []
| Bool
otherwise = ThetaType
cls_tys
deriv_origin :: CtOrigin
deriv_origin = Bool -> CtOrigin
mkDerivOrigin Bool
wildcard
if
| Bool
is_generic
-> forall (m :: * -> *) a. Monad m => a -> m a
return ([], [TcTyVar]
tvs, ThetaType
inst_tys, DerivInstTys
dit)
| Bool
is_generic1
-> forall a. HasCallStack => Bool -> a -> a
assert (TyCon -> [TcTyVar]
tyConTyVars TyCon
rep_tc forall a. [a] -> Int -> Bool
`lengthExceeds` Int
0) forall a b. (a -> b) -> a -> b
$
forall a. HasCallStack => Bool -> a -> a
assert (ThetaType
cls_tys forall a. [a] -> Int -> Bool
`lengthIs` Int
1) forall a b. (a -> b) -> a -> b
$
do { Class
functorClass <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Name -> TcM Class
tcLookupClass Name
functorClassName
; forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ ([TcTyVar]
-> CtOrigin
-> TypeOrKind
-> PredType
-> [(ThetaSpec, Maybe Subst)])
-> (ThetaSpec, [TcTyVar], ThetaType, DerivInstTys)
con_arg_constraints
forall a b. (a -> b) -> a -> b
$ Class
-> [TcTyVar]
-> CtOrigin
-> TypeOrKind
-> PredType
-> [(ThetaSpec, Maybe Subst)]
get_gen1_constraints Class
functorClass }
| Bool
otherwise
-> do { let (ThetaSpec
arg_constraints, [TcTyVar]
tvs', ThetaType
inst_tys', DerivInstTys
dit')
= ([TcTyVar]
-> CtOrigin
-> TypeOrKind
-> PredType
-> [(ThetaSpec, Maybe Subst)])
-> (ThetaSpec, [TcTyVar], ThetaType, DerivInstTys)
con_arg_constraints [TcTyVar]
-> CtOrigin -> TypeOrKind -> PredType -> [(ThetaSpec, Maybe Subst)]
get_std_constrained_tys
; forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcRn ()
traceTc String
"inferConstraintsStock" forall a b. (a -> b) -> a -> b
$ forall doc. IsDoc doc => [doc] -> doc
vcat
[ forall a. Outputable a => a -> SDoc
ppr Class
main_cls forall doc. IsLine doc => doc -> doc -> doc
<+> forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_tys'
, forall a. Outputable a => a -> SDoc
ppr ThetaSpec
arg_constraints
]
; forall (m :: * -> *) a. Monad m => a -> m a
return ( ThetaSpec
extra_constraints forall a. [a] -> [a] -> [a]
++ ThetaSpec
arg_constraints
, [TcTyVar]
tvs', ThetaType
inst_tys', DerivInstTys
dit' ) }
inferConstraintsAnyclass :: DerivM ThetaSpec
inferConstraintsAnyclass :: DerivM ThetaSpec
inferConstraintsAnyclass
= do { DerivEnv { denv_cls :: DerivEnv -> Class
denv_cls = Class
cls
, denv_inst_tys :: DerivEnv -> ThetaType
denv_inst_tys = ThetaType
inst_tys } <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
; let gen_dms :: [(TcTyVar, PredType)]
gen_dms = [ (TcTyVar
sel_id, PredType
dm_ty)
| (TcTyVar
sel_id, Just (Name
_, GenericDM PredType
dm_ty)) <- Class -> [(TcTyVar, DefMethInfo)]
classOpItems Class
cls ]
; Bool
wildcard <- DerivM Bool
isStandaloneWildcardDeriv
; let meth_pred :: (Id, Type) -> PredSpec
meth_pred :: (TcTyVar, PredType) -> PredSpec
meth_pred (TcTyVar
sel_id, PredType
gen_dm_ty)
= let ([TcTyVar]
sel_tvs, PredType
_cls_pred, PredType
meth_ty) = PredType -> ([TcTyVar], PredType, PredType)
tcSplitMethodTy (TcTyVar -> PredType
varType TcTyVar
sel_id)
meth_ty' :: PredType
meth_ty' = HasDebugCallStack => [TcTyVar] -> ThetaType -> PredType -> PredType
substTyWith [TcTyVar]
sel_tvs ThetaType
inst_tys PredType
meth_ty
gen_dm_ty' :: PredType
gen_dm_ty' = HasDebugCallStack => [TcTyVar] -> ThetaType -> PredType -> PredType
substTyWith [TcTyVar]
sel_tvs ThetaType
inst_tys PredType
gen_dm_ty in
SubTypePredSpec { stps_ty_actual :: PredType
stps_ty_actual = PredType
gen_dm_ty'
, stps_ty_expected :: PredType
stps_ty_expected = PredType
meth_ty'
, stps_origin :: CtOrigin
stps_origin = Bool -> CtOrigin
mkDerivOrigin Bool
wildcard
}
; forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (TcTyVar, PredType) -> PredSpec
meth_pred [(TcTyVar, PredType)]
gen_dms }
inferConstraintsCoerceBased :: [Type] -> Type
-> DerivM ThetaSpec
inferConstraintsCoerceBased :: ThetaType -> PredType -> DerivM ThetaSpec
inferConstraintsCoerceBased ThetaType
cls_tys PredType
rep_ty = do
DerivEnv { denv_tvs :: DerivEnv -> [TcTyVar]
denv_tvs = [TcTyVar]
tvs
, denv_cls :: DerivEnv -> Class
denv_cls = Class
cls
, denv_inst_tys :: DerivEnv -> ThetaType
denv_inst_tys = ThetaType
inst_tys } <- forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
Bool
sa_wildcard <- DerivM Bool
isStandaloneWildcardDeriv
let
rep_tys :: PredType -> ThetaType
rep_tys PredType
ty = ThetaType
cls_tys forall a. [a] -> [a] -> [a]
++ [PredType
ty]
rep_pred :: PredType -> PredType
rep_pred PredType
ty = Class -> ThetaType -> PredType
mkClassPred Class
cls (PredType -> ThetaType
rep_tys PredType
ty)
rep_pred_o :: PredType -> PredSpec
rep_pred_o PredType
ty = SimplePredSpec { sps_pred :: PredType
sps_pred = PredType -> PredType
rep_pred PredType
ty
, sps_origin :: CtOrigin
sps_origin = CtOrigin
deriv_origin
, sps_type_or_kind :: TypeOrKind
sps_type_or_kind = TypeOrKind
TypeLevel
}
deriv_origin :: CtOrigin
deriv_origin = Bool -> CtOrigin
mkDerivOrigin Bool
sa_wildcard
meth_preds :: Type -> ThetaSpec
meth_preds :: PredType -> ThetaSpec
meth_preds PredType
ty
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
meths = []
| Bool
otherwise = PredType -> PredSpec
rep_pred_o PredType
ty forall a. a -> [a] -> [a]
: PredType -> ThetaSpec
coercible_constraints PredType
ty
meths :: [TcTyVar]
meths = Class -> [TcTyVar]
classMethods Class
cls
coercible_constraints :: PredType -> ThetaSpec
coercible_constraints PredType
ty
= [ SimplePredSpec
{ sps_pred :: PredType
sps_pred = PredType -> PredType -> PredType
mkReprPrimEqPred PredType
t1 PredType
t2
, sps_origin :: CtOrigin
sps_origin = TcTyVar -> PredType -> PredType -> Bool -> CtOrigin
DerivOriginCoerce TcTyVar
meth PredType
t1 PredType
t2 Bool
sa_wildcard
, sps_type_or_kind :: TypeOrKind
sps_type_or_kind = TypeOrKind
TypeLevel
}
| TcTyVar
meth <- [TcTyVar]
meths
, let (Pair PredType
t1 PredType
t2) = Class
-> [TcTyVar] -> ThetaType -> PredType -> TcTyVar -> Pair PredType
mkCoerceClassMethEqn Class
cls [TcTyVar]
tvs
ThetaType
inst_tys PredType
ty TcTyVar
meth ]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PredType -> ThetaSpec
meth_preds PredType
rep_ty)
simplifyInstanceContexts :: [DerivSpec ThetaSpec]
-> TcM [DerivSpec ThetaType]
simplifyInstanceContexts :: [DerivSpec ThetaSpec] -> TcM [DerivSpec ThetaType]
simplifyInstanceContexts [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
simplifyInstanceContexts [DerivSpec ThetaSpec]
infer_specs
= do { String -> SDoc -> TcRn ()
traceTc String
"simplifyInstanceContexts" forall a b. (a -> b) -> a -> b
$ forall doc. IsDoc doc => [doc] -> doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall theta. Outputable theta => DerivSpec theta -> SDoc
pprDerivSpec [DerivSpec ThetaSpec]
infer_specs)
; [DerivSpec ThetaType]
final_specs <- Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
iterate_deriv Int
1 [ThetaType]
initial_solutions
; forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DerivSpec ThetaType -> TcM (DerivSpec ThetaType)
zonkDerivSpec [DerivSpec ThetaType]
final_specs }
where
initial_solutions :: [ThetaType]
initial_solutions :: [ThetaType]
initial_solutions = [ [] | DerivSpec ThetaSpec
_ <- [DerivSpec ThetaSpec]
infer_specs ]
iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
iterate_deriv :: Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
iterate_deriv Int
n [ThetaType]
current_solns
| Int
n forall a. Ord a => a -> a -> Bool
> Int
20
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveDerivEqns: probable loop"
(forall doc. IsDoc doc => [doc] -> doc
vcat (forall a b. (a -> b) -> [a] -> [b]
map forall theta. Outputable theta => DerivSpec theta -> SDoc
pprDerivSpec [DerivSpec ThetaSpec]
infer_specs) forall doc. IsDoc doc => doc -> doc -> doc
$$ forall a. Outputable a => a -> SDoc
ppr [ThetaType]
current_solns)
| Bool
otherwise
= do {
[ClsInst]
inst_specs <- forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (\ThetaType
soln -> DerivSpec ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) ClsInst
newDerivClsInst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall theta' theta. theta' -> DerivSpec theta -> DerivSpec theta'
setDerivSpecTheta ThetaType
soln)
[ThetaType]
current_solns [DerivSpec ThetaSpec]
infer_specs
; [ThetaType]
new_solns <- forall r. TcM r -> TcM r
checkNoErrs forall a b. (a -> b) -> a -> b
$
forall a. [ClsInst] -> TcM a -> TcM a
extendLocalInstEnv [ClsInst]
inst_specs forall a b. (a -> b) -> a -> b
$
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DerivSpec ThetaSpec -> TcM ThetaType
gen_soln [DerivSpec ThetaSpec]
infer_specs
; if ([ThetaType]
current_solns [ThetaType] -> [ThetaType] -> Bool
`eqSolution` [ThetaType]
new_solns) then
forall (m :: * -> *) a. Monad m => a -> m a
return [ forall theta' theta. theta' -> DerivSpec theta -> DerivSpec theta'
setDerivSpecTheta ThetaType
soln DerivSpec ThetaSpec
spec
| (DerivSpec ThetaSpec
spec, ThetaType
soln) <- forall a b. [a] -> [b] -> [(a, b)]
zip [DerivSpec ThetaSpec]
infer_specs [ThetaType]
current_solns ]
else
Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
iterate_deriv (Int
nforall a. Num a => a -> a -> a
+Int
1) [ThetaType]
new_solns }
eqSolution :: [ThetaType] -> [ThetaType] -> Bool
eqSolution = (forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b.
Eq1 f =>
(a -> b -> Bool) -> f a -> f b -> Bool
liftEq) PredType -> PredType -> Bool
eqType forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` [ThetaType] -> [ThetaType]
canSolution
canSolution :: [ThetaType] -> [ThetaType]
canSolution = forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy PredType -> PredType -> Ordering
nonDetCmpType)
gen_soln :: DerivSpec ThetaSpec -> TcM ThetaType
gen_soln :: DerivSpec ThetaSpec -> TcM ThetaType
gen_soln (DS { ds_loc :: forall theta. DerivSpec theta -> SrcSpan
ds_loc = SrcSpan
loc, ds_tvs :: forall theta. DerivSpec theta -> [TcTyVar]
ds_tvs = [TcTyVar]
tyvars
, ds_cls :: forall theta. DerivSpec theta -> Class
ds_cls = Class
clas, ds_tys :: forall theta. DerivSpec theta -> ThetaType
ds_tys = ThetaType
inst_tys, ds_theta :: forall theta. DerivSpec theta -> theta
ds_theta = ThetaSpec
deriv_rhs
, ds_skol_info :: forall theta. DerivSpec theta -> SkolemInfo
ds_skol_info = SkolemInfo
skol_info, ds_user_ctxt :: forall theta. DerivSpec theta -> UserTypeCtxt
ds_user_ctxt = UserTypeCtxt
user_ctxt })
= forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc forall a b. (a -> b) -> a -> b
$
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (PredType -> SDoc
derivInstCtxt PredType
the_pred) forall a b. (a -> b) -> a -> b
$
do { ThetaType
theta <- SkolemInfo
-> UserTypeCtxt -> [TcTyVar] -> ThetaSpec -> TcM ThetaType
simplifyDeriv SkolemInfo
skol_info UserTypeCtxt
user_ctxt [TcTyVar]
tyvars ThetaSpec
deriv_rhs
; String -> SDoc -> TcRn ()
traceTc String
"GHC.Tc.Deriv" (forall a. Outputable a => a -> SDoc
ppr ThetaSpec
deriv_rhs forall doc. IsDoc doc => doc -> doc -> doc
$$ forall a. Outputable a => a -> SDoc
ppr ThetaType
theta)
; forall (m :: * -> *) a. Monad m => a -> m a
return ThetaType
theta }
where
the_pred :: PredType
the_pred = Class -> ThetaType -> PredType
mkClassPred Class
clas ThetaType
inst_tys
derivInstCtxt :: PredType -> SDoc
derivInstCtxt :: PredType -> SDoc
derivInstCtxt PredType
pred
= forall doc. IsLine doc => String -> doc
text String
"When deriving the instance for" forall doc. IsLine doc => doc -> doc -> doc
<+> forall doc. IsLine doc => doc -> doc
parens (forall a. Outputable a => a -> SDoc
ppr PredType
pred)
simplifyDeriv :: SkolemInfo
-> UserTypeCtxt
-> [TcTyVar]
-> ThetaSpec
-> TcM ThetaType
simplifyDeriv :: SkolemInfo
-> UserTypeCtxt -> [TcTyVar] -> ThetaSpec -> TcM ThetaType
simplifyDeriv SkolemInfo
skol_info UserTypeCtxt
user_ctxt [TcTyVar]
tvs ThetaSpec
theta
= do { let skol_set :: VarSet
skol_set = [TcTyVar] -> VarSet
mkVarSet [TcTyVar]
tvs
; (TcLevel
tc_lvl, WantedConstraints
wanteds) <- UserTypeCtxt -> ThetaSpec -> TcM (TcLevel, WantedConstraints)
captureThetaSpecConstraints UserTypeCtxt
user_ctxt ThetaSpec
theta
; String -> SDoc -> TcRn ()
traceTc String
"simplifyDeriv inputs" forall a b. (a -> b) -> a -> b
$
forall doc. IsDoc doc => [doc] -> doc
vcat [ [TcTyVar] -> SDoc
pprTyVars [TcTyVar]
tvs forall doc. IsDoc doc => doc -> doc -> doc
$$ forall a. Outputable a => a -> SDoc
ppr ThetaSpec
theta forall doc. IsDoc doc => doc -> doc -> doc
$$ forall a. Outputable a => a -> SDoc
ppr WantedConstraints
wanteds, forall a. Outputable a => a -> SDoc
ppr SkolemInfo
skol_info ]
; (WantedConstraints
solved_wanteds, EvBindMap
_) <- forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
tc_lvl forall a b. (a -> b) -> a -> b
$
forall a. TcS a -> TcM (a, EvBindMap)
runTcS forall a b. (a -> b) -> a -> b
$
WantedConstraints -> TcS WantedConstraints
solveWanteds WantedConstraints
wanteds
; WantedConstraints
solved_wanteds <- WantedConstraints -> TcM WantedConstraints
zonkWC WantedConstraints
solved_wanteds
; let residual_simple :: Cts
residual_simple = Bool -> WantedConstraints -> Cts
approximateWC Bool
True WantedConstraints
solved_wanteds
good :: Bag PredType
good = forall a b. (a -> Maybe b) -> Bag a -> Bag b
mapMaybeBag Ct -> Maybe PredType
get_good Cts
residual_simple
get_good :: Ct -> Maybe PredType
get_good :: Ct -> Maybe PredType
get_good Ct
ct | VarSet -> PredType -> Bool
validDerivPred VarSet
skol_set PredType
p
= forall a. a -> Maybe a
Just PredType
p
| Bool
otherwise
= forall a. Maybe a
Nothing
where p :: PredType
p = Ct -> PredType
ctPred Ct
ct
; String -> SDoc -> TcRn ()
traceTc String
"simplifyDeriv outputs" forall a b. (a -> b) -> a -> b
$
forall doc. IsDoc doc => [doc] -> doc
vcat [ forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs, forall a. Outputable a => a -> SDoc
ppr Cts
residual_simple, forall a. Outputable a => a -> SDoc
ppr Bag PredType
good ]
; let min_theta :: ThetaType
min_theta = forall a. (a -> PredType) -> [a] -> [a]
mkMinimalBySCs forall a. a -> a
id (forall a. Bag a -> [a]
bagToList Bag PredType
good)
; [TcTyVar]
min_theta_vars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall gbl lcl. PredType -> TcRnIf gbl lcl TcTyVar
newEvVar ThetaType
min_theta
; (Bag Implication
leftover_implic, TcEvBinds
_)
<- TcLevel
-> SkolemInfoAnon
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
tvs
[TcTyVar]
min_theta_vars WantedConstraints
solved_wanteds
; Bag Implication -> TcRn ()
simplifyTopImplic Bag Implication
leftover_implic
; forall (m :: * -> *) a. Monad m => a -> m a
return ThetaType
min_theta }