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