{-# LANGUAGE CPP #-}
{-# LANGUAGE MultiWayIf #-}
module GHC.Tc.Deriv.Infer
( inferConstraints
, simplifyInstanceContexts
)
where
#include "HsVersions.h"
import GHC.Prelude
import GHC.Data.Bag
import GHC.Types.Basic
import GHC.Core.Class
import GHC.Core.DataCon
import GHC.Utils.Error
import GHC.Tc.Utils.Instantiate
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.Pair
import GHC.Builtin.Names
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.Core.Predicate
import GHC.Tc.Utils.TcType
import GHC.Core.TyCon
import GHC.Core.TyCo.Ppr (pprTyVars)
import GHC.Core.Type
import GHC.Tc.Solver
import GHC.Tc.Validity (validDerivPred)
import GHC.Tc.Utils.Unify (buildImplicationFor, checkConstraints)
import GHC.Builtin.Types (typeToTypeKind)
import GHC.Core.Unify (tcUnifyTy)
import GHC.Utils.Misc
import GHC.Types.Var
import GHC.Types.Var.Set
import Control.Monad
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.Reader (ask)
import Data.List (sortBy)
import Data.Maybe
inferConstraints :: DerivSpecMechanism
-> DerivM ([ThetaOrigin], [TyVar], [TcType])
inferConstraints :: DerivSpecMechanism -> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
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 } <- ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) DerivEnv
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
; Bool
wildcard <- DerivM Bool
isStandaloneWildcardDeriv
; let infer_constraints :: DerivM ([ThetaOrigin], [TyVar], [TcType])
infer_constraints :: DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
infer_constraints =
case DerivSpecMechanism
mechanism of
DerivSpecStock{dsm_stock_dit :: DerivSpecMechanism -> DerivInstTys
dsm_stock_dit = DerivInstTys
dit}
-> DerivInstTys -> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
inferConstraintsStock DerivInstTys
dit
DerivSpecMechanism
DerivSpecAnyClass
-> DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
infer_constraints_simple DerivM [ThetaOrigin]
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 [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
infer_constraints_simple (DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType))
-> DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall a b. (a -> b) -> a -> b
$
ThetaType -> PredType -> DerivM [ThetaOrigin]
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 [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
infer_constraints_simple (DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType))
-> DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall a b. (a -> b) -> a -> b
$
ThetaType -> PredType -> DerivM [ThetaOrigin]
inferConstraintsCoerceBased ThetaType
cls_tys PredType
via_ty
infer_constraints_simple
:: DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TyVar], [TcType])
infer_constraints_simple :: DerivM [ThetaOrigin]
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
infer_constraints_simple DerivM [ThetaOrigin]
infer_thetas = do
[ThetaOrigin]
thetas <- DerivM [ThetaOrigin]
infer_thetas
([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([ThetaOrigin]
thetas, [TcTyVar]
tvs, ThetaType
inst_tys)
cls_tvs :: [TcTyVar]
cls_tvs = Class -> [TcTyVar]
classTyVars Class
main_cls
sc_constraints :: [ThetaOrigin]
sc_constraints = ASSERT2( equalLength cls_tvs inst_tys
, ppr main_cls <+> ppr inst_tys )
[ CtOrigin
-> TypeOrKind
-> [TcTyVar]
-> [TcTyVar]
-> ThetaType
-> ThetaType
-> ThetaOrigin
mkThetaOrigin (Bool -> CtOrigin
mkDerivOrigin Bool
wildcard)
TypeOrKind
TypeLevel [] [] [] (ThetaType -> ThetaOrigin) -> ThetaType -> ThetaOrigin
forall a b. (a -> b) -> a -> b
$
HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
cls_subst (Class -> ThetaType
classSCTheta Class
main_cls) ]
cls_subst :: TCvSubst
cls_subst = ASSERT( equalLength cls_tvs inst_tys )
[TcTyVar] -> ThetaType -> TCvSubst
HasDebugCallStack => [TcTyVar] -> ThetaType -> TCvSubst
zipTvSubst [TcTyVar]
cls_tvs ThetaType
inst_tys
; ([ThetaOrigin]
inferred_constraints, [TcTyVar]
tvs', ThetaType
inst_tys') <- DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
infer_constraints
; TcRn () -> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcRn () -> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) ())
-> TcRn () -> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcRn ()
traceTc String
"inferConstraints" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
main_cls SDoc -> SDoc -> SDoc
<+> ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_tys'
, [ThetaOrigin] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ThetaOrigin]
inferred_constraints
]
; ([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [ThetaOrigin]
sc_constraints [ThetaOrigin] -> [ThetaOrigin] -> [ThetaOrigin]
forall a. [a] -> [a] -> [a]
++ [ThetaOrigin]
inferred_constraints
, [TcTyVar]
tvs', ThetaType
inst_tys' ) }
inferConstraintsStock :: DerivInstTys
-> DerivM ([ThetaOrigin], [TyVar], [TcType])
inferConstraintsStock :: DerivInstTys -> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
inferConstraintsStock (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 } <- ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) DerivEnv
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 = (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
:: (CtOrigin -> TypeOrKind
-> Type
-> [([PredOrigin], Maybe TCvSubst)])
-> ([ThetaOrigin], [TyVar], [TcType])
con_arg_constraints :: (CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)])
-> ([ThetaOrigin], [TcTyVar], ThetaType)
con_arg_constraints CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)]
get_arg_constraints
= let ([[PredOrigin]]
predss, [Maybe TCvSubst]
mbSubsts) = [([PredOrigin], Maybe TCvSubst)]
-> ([[PredOrigin]], [Maybe TCvSubst])
forall a b. [(a, b)] -> ([a], [b])
unzip
[ ([PredOrigin], Maybe TCvSubst)
preds_and_mbSubst
| DataCon
data_con <- TyCon -> [DataCon]
tyConDataCons TyCon
rep_tc
, (Int
arg_n, TypeOrKind
arg_t_or_k, Scaled PredType
arg_ty)
<- [Int]
-> [TypeOrKind]
-> [Scaled PredType]
-> [(Int, TypeOrKind, Scaled PredType)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [Int
1..] [TypeOrKind]
t_or_ks ([Scaled PredType] -> [(Int, TypeOrKind, Scaled PredType)])
-> [Scaled PredType] -> [(Int, TypeOrKind, Scaled PredType)]
forall a b. (a -> b) -> a -> b
$
DataCon -> ThetaType -> [Scaled PredType]
dataConInstOrigArgTys DataCon
data_con ThetaType
all_rep_tc_args
, Bool -> Bool
not (HasDebugCallStack => PredType -> Bool
PredType -> Bool
isUnliftedType (Scaled PredType -> PredType
forall a. Scaled a -> a
irrelevantMult Scaled PredType
arg_ty))
, let orig :: CtOrigin
orig = DataCon -> Int -> Bool -> CtOrigin
DerivOriginDC DataCon
data_con Int
arg_n Bool
wildcard
, ([PredOrigin], Maybe TCvSubst)
preds_and_mbSubst
<- CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)]
get_arg_constraints CtOrigin
orig TypeOrKind
arg_t_or_k (Scaled PredType -> PredType
forall a. Scaled a -> a
irrelevantMult Scaled PredType
arg_ty)
]
preds :: [PredOrigin]
preds = [[PredOrigin]] -> [PredOrigin]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[PredOrigin]]
predss
subst :: TCvSubst
subst = (TCvSubst -> TCvSubst -> TCvSubst)
-> TCvSubst -> [TCvSubst] -> TCvSubst
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' TCvSubst -> TCvSubst -> TCvSubst
composeTCvSubst
TCvSubst
emptyTCvSubst ([Maybe TCvSubst] -> [TCvSubst]
forall a. [Maybe a] -> [a]
catMaybes [Maybe TCvSubst]
mbSubsts)
unmapped_tvs :: [TcTyVar]
unmapped_tvs = (TcTyVar -> Bool) -> [TcTyVar] -> [TcTyVar]
forall a. (a -> Bool) -> [a] -> [a]
filter (\TcTyVar
v -> TcTyVar
v TcTyVar -> TCvSubst -> Bool
`notElemTCvSubst` TCvSubst
subst
Bool -> Bool -> Bool
&& Bool -> Bool
not (TcTyVar
v TcTyVar -> TCvSubst -> Bool
`isInScope` TCvSubst
subst)) [TcTyVar]
tvs
(TCvSubst
subst', [TcTyVar]
_) = HasCallStack => TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar])
TCvSubst -> [TcTyVar] -> (TCvSubst, [TcTyVar])
substTyVarBndrs TCvSubst
subst [TcTyVar]
unmapped_tvs
preds' :: [PredOrigin]
preds' = (PredOrigin -> PredOrigin) -> [PredOrigin] -> [PredOrigin]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
TCvSubst -> PredOrigin -> PredOrigin
substPredOrigin TCvSubst
subst') [PredOrigin]
preds
inst_tys' :: ThetaType
inst_tys' = HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTys TCvSubst
subst' ThetaType
inst_tys
tvs' :: [TcTyVar]
tvs' = ThetaType -> [TcTyVar]
tyCoVarsOfTypesWellScoped ThetaType
inst_tys'
in ([[PredOrigin] -> ThetaOrigin
mkThetaOriginFromPreds [PredOrigin]
preds'], [TcTyVar]
tvs', ThetaType
inst_tys')
is_generic :: Bool
is_generic = Class
main_cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
genClassKey
is_generic1 :: Bool
is_generic1 = Class
main_cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
gen1ClassKey
is_functor_like :: Bool
is_functor_like = HasDebugCallStack => PredType -> PredType
PredType -> PredType
tcTypeKind PredType
inst_ty HasDebugCallStack => PredType -> PredType -> Bool
PredType -> PredType -> Bool
`tcEqKind` PredType
typeToTypeKind
Bool -> Bool -> Bool
|| Bool
is_generic1
get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
-> [([PredOrigin], Maybe TCvSubst)]
get_gen1_constraints :: Class
-> CtOrigin
-> TypeOrKind
-> PredType
-> [([PredOrigin], Maybe TCvSubst)]
get_gen1_constraints Class
functor_cls CtOrigin
orig TypeOrKind
t_or_k PredType
ty
= CtOrigin
-> TypeOrKind
-> Class
-> ThetaType
-> [([PredOrigin], Maybe TCvSubst)]
mk_functor_like_constraints CtOrigin
orig TypeOrKind
t_or_k Class
functor_cls (ThetaType -> [([PredOrigin], Maybe TCvSubst)])
-> ThetaType -> [([PredOrigin], Maybe TCvSubst)]
forall a b. (a -> b) -> a -> b
$
TcTyVar -> PredType -> ThetaType
get_gen1_constrained_tys TcTyVar
last_tv PredType
ty
get_std_constrained_tys :: CtOrigin -> TypeOrKind -> Type
-> [([PredOrigin], Maybe TCvSubst)]
get_std_constrained_tys :: CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)]
get_std_constrained_tys CtOrigin
orig TypeOrKind
t_or_k PredType
ty
| Bool
is_functor_like
= CtOrigin
-> TypeOrKind
-> Class
-> ThetaType
-> [([PredOrigin], Maybe TCvSubst)]
mk_functor_like_constraints CtOrigin
orig TypeOrKind
t_or_k Class
main_cls (ThetaType -> [([PredOrigin], Maybe TCvSubst)])
-> ThetaType -> [([PredOrigin], Maybe TCvSubst)]
forall a b. (a -> b) -> a -> b
$
TcTyVar -> PredType -> ThetaType
deepSubtypesContaining TcTyVar
last_tv PredType
ty
| Bool
otherwise
= [( [CtOrigin -> TypeOrKind -> Class -> PredType -> PredOrigin
mk_cls_pred CtOrigin
orig TypeOrKind
t_or_k Class
main_cls PredType
ty]
, Maybe TCvSubst
forall a. Maybe a
Nothing )]
mk_functor_like_constraints :: CtOrigin -> TypeOrKind
-> Class -> [Type]
-> [([PredOrigin], Maybe TCvSubst)]
mk_functor_like_constraints :: CtOrigin
-> TypeOrKind
-> Class
-> ThetaType
-> [([PredOrigin], Maybe TCvSubst)]
mk_functor_like_constraints CtOrigin
orig TypeOrKind
t_or_k Class
cls
= (PredType -> ([PredOrigin], Maybe TCvSubst))
-> ThetaType -> [([PredOrigin], Maybe TCvSubst)]
forall a b. (a -> b) -> [a] -> [b]
map ((PredType -> ([PredOrigin], Maybe TCvSubst))
-> ThetaType -> [([PredOrigin], Maybe TCvSubst)])
-> (PredType -> ([PredOrigin], Maybe TCvSubst))
-> ThetaType
-> [([PredOrigin], Maybe TCvSubst)]
forall a b. (a -> b) -> a -> b
$ \PredType
ty -> let ki :: PredType
ki = HasDebugCallStack => PredType -> PredType
PredType -> PredType
tcTypeKind PredType
ty in
( [ CtOrigin -> TypeOrKind -> Class -> PredType -> PredOrigin
mk_cls_pred CtOrigin
orig TypeOrKind
t_or_k Class
cls PredType
ty
, CtOrigin -> TypeOrKind -> PredType -> PredOrigin
mkPredOrigin CtOrigin
orig TypeOrKind
KindLevel
(PredType -> PredType -> PredType
mkPrimEqPred PredType
ki PredType
typeToTypeKind) ]
, PredType -> PredType -> Maybe TCvSubst
tcUnifyTy PredType
ki PredType
typeToTypeKind
)
rep_tc_tvs :: [TcTyVar]
rep_tc_tvs = TyCon -> [TcTyVar]
tyConTyVars TyCon
rep_tc
last_tv :: TcTyVar
last_tv = [TcTyVar] -> TcTyVar
forall a. [a] -> a
last [TcTyVar]
rep_tc_tvs
all_rep_tc_args :: ThetaType
all_rep_tc_args = TyCon -> ThetaType -> ThetaType
tyConInstArgTys TyCon
rep_tc ThetaType
rep_tc_args
stupid_constraints :: [ThetaOrigin]
stupid_constraints
= [ CtOrigin
-> TypeOrKind
-> [TcTyVar]
-> [TcTyVar]
-> ThetaType
-> ThetaType
-> ThetaOrigin
mkThetaOrigin CtOrigin
deriv_origin TypeOrKind
TypeLevel [] [] [] (ThetaType -> ThetaOrigin) -> ThetaType -> ThetaOrigin
forall a b. (a -> b) -> a -> b
$
HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
tc_subst (TyCon -> ThetaType
tyConStupidTheta TyCon
rep_tc) ]
tc_subst :: TCvSubst
tc_subst =
ASSERT( equalLength rep_tc_tvs all_rep_tc_args )
[TcTyVar] -> ThetaType -> TCvSubst
HasDebugCallStack => [TcTyVar] -> ThetaType -> TCvSubst
zipTvSubst [TcTyVar]
rep_tc_tvs ThetaType
all_rep_tc_args
extra_constraints :: [ThetaOrigin]
extra_constraints = [[PredOrigin] -> ThetaOrigin
mkThetaOriginFromPreds [PredOrigin]
constrs]
where
constrs :: [PredOrigin]
constrs
| Class
main_cls Class -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
dataClassKey
, (PredType -> Bool) -> ThetaType -> 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
tcTypeKind) ThetaType
rep_tc_args
= [ CtOrigin -> TypeOrKind -> Class -> PredType -> PredOrigin
mk_cls_pred CtOrigin
deriv_origin TypeOrKind
t_or_k Class
main_cls PredType
ty
| (TypeOrKind
t_or_k, PredType
ty) <- [TypeOrKind] -> ThetaType -> [(TypeOrKind, PredType)]
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 -> PredOrigin
mk_cls_pred CtOrigin
orig TypeOrKind
t_or_k Class
cls PredType
ty
= CtOrigin -> TypeOrKind -> PredType -> PredOrigin
mkPredOrigin CtOrigin
orig TypeOrKind
t_or_k (Class -> ThetaType -> PredType
mkClassPred Class
cls (ThetaType
cls_tys' ThetaType -> ThetaType -> ThetaType
forall a. [a] -> [a] -> [a]
++ [PredType
ty]))
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
-> ([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [TcTyVar]
tvs, ThetaType
inst_tys)
| Bool
is_generic1
-> ASSERT( rep_tc_tvs `lengthExceeds` 0 )
ASSERT( cls_tys `lengthIs` 1 )
do { Class
functorClass <- IOEnv (Env TcGblEnv TcLclEnv) Class
-> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) Class
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOEnv (Env TcGblEnv TcLclEnv) Class
-> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) Class)
-> IOEnv (Env TcGblEnv TcLclEnv) Class
-> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) Class
forall a b. (a -> b) -> a -> b
$ Name -> IOEnv (Env TcGblEnv TcLclEnv) Class
tcLookupClass Name
functorClassName
; ([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType))
-> ([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall a b. (a -> b) -> a -> b
$ (CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)])
-> ([ThetaOrigin], [TcTyVar], ThetaType)
con_arg_constraints
((CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)])
-> ([ThetaOrigin], [TcTyVar], ThetaType))
-> (CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)])
-> ([ThetaOrigin], [TcTyVar], ThetaType)
forall a b. (a -> b) -> a -> b
$ Class
-> CtOrigin
-> TypeOrKind
-> PredType
-> [([PredOrigin], Maybe TCvSubst)]
get_gen1_constraints Class
functorClass }
| Bool
otherwise
->
ASSERT2( equalLength rep_tc_tvs all_rep_tc_args
, ppr main_cls <+> ppr rep_tc
$$ ppr rep_tc_tvs $$ ppr all_rep_tc_args )
do { let ([ThetaOrigin]
arg_constraints, [TcTyVar]
tvs', ThetaType
inst_tys')
= (CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)])
-> ([ThetaOrigin], [TcTyVar], ThetaType)
con_arg_constraints CtOrigin
-> TypeOrKind -> PredType -> [([PredOrigin], Maybe TCvSubst)]
get_std_constrained_tys
; TcRn () -> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcRn () -> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) ())
-> TcRn () -> ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcRn ()
traceTc String
"inferConstraintsStock" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ Class -> SDoc
forall a. Outputable a => a -> SDoc
ppr Class
main_cls SDoc -> SDoc -> SDoc
<+> ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
inst_tys'
, [ThetaOrigin] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ThetaOrigin]
arg_constraints
]
; ([ThetaOrigin], [TcTyVar], ThetaType)
-> DerivM ([ThetaOrigin], [TcTyVar], ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [ThetaOrigin]
stupid_constraints [ThetaOrigin] -> [ThetaOrigin] -> [ThetaOrigin]
forall a. [a] -> [a] -> [a]
++ [ThetaOrigin]
extra_constraints
[ThetaOrigin] -> [ThetaOrigin] -> [ThetaOrigin]
forall a. [a] -> [a] -> [a]
++ [ThetaOrigin]
arg_constraints
, [TcTyVar]
tvs', ThetaType
inst_tys') }
inferConstraintsAnyclass :: DerivM [ThetaOrigin]
inferConstraintsAnyclass :: DerivM [ThetaOrigin]
inferConstraintsAnyclass
= do { DerivEnv { denv_cls :: DerivEnv -> Class
denv_cls = Class
cls
, denv_inst_tys :: DerivEnv -> ThetaType
denv_inst_tys = ThetaType
inst_tys } <- ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) DerivEnv
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask
; Bool
wildcard <- DerivM Bool
isStandaloneWildcardDeriv
; 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 ]
cls_tvs :: [TcTyVar]
cls_tvs = Class -> [TcTyVar]
classTyVars Class
cls
do_one_meth :: (Id, Type) -> TcM ThetaOrigin
do_one_meth :: (TcTyVar, PredType) -> TcM ThetaOrigin
do_one_meth (TcTyVar
sel_id, PredType
gen_dm_ty)
= do { 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' = HasCallStack => [TcTyVar] -> ThetaType -> PredType -> PredType
[TcTyVar] -> ThetaType -> PredType -> PredType
substTyWith [TcTyVar]
sel_tvs ThetaType
inst_tys PredType
meth_ty
([TcTyVar]
meth_tvs, ThetaType
meth_theta, PredType
meth_tau)
= PredType -> ([TcTyVar], ThetaType, PredType)
tcSplitNestedSigmaTys PredType
meth_ty'
gen_dm_ty' :: PredType
gen_dm_ty' = HasCallStack => [TcTyVar] -> ThetaType -> PredType -> PredType
[TcTyVar] -> ThetaType -> PredType -> PredType
substTyWith [TcTyVar]
cls_tvs ThetaType
inst_tys PredType
gen_dm_ty
([TcTyVar]
dm_tvs, ThetaType
dm_theta, PredType
dm_tau)
= PredType -> ([TcTyVar], ThetaType, PredType)
tcSplitNestedSigmaTys PredType
gen_dm_ty'
tau_eq :: PredType
tau_eq = PredType -> PredType -> PredType
mkPrimEqPred PredType
meth_tau PredType
dm_tau
; ThetaOrigin -> TcM ThetaOrigin
forall (m :: * -> *) a. Monad m => a -> m a
return (CtOrigin
-> TypeOrKind
-> [TcTyVar]
-> [TcTyVar]
-> ThetaType
-> ThetaType
-> ThetaOrigin
mkThetaOrigin (Bool -> CtOrigin
mkDerivOrigin Bool
wildcard) TypeOrKind
TypeLevel
[TcTyVar]
meth_tvs [TcTyVar]
dm_tvs ThetaType
meth_theta (PredType
tau_eqPredType -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
:ThetaType
dm_theta)) }
; TcRn [ThetaOrigin] -> DerivM [ThetaOrigin]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcRn [ThetaOrigin] -> DerivM [ThetaOrigin])
-> TcRn [ThetaOrigin] -> DerivM [ThetaOrigin]
forall a b. (a -> b) -> a -> b
$ ((TcTyVar, PredType) -> TcM ThetaOrigin)
-> [(TcTyVar, PredType)] -> TcRn [ThetaOrigin]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TcTyVar, PredType) -> TcM ThetaOrigin
do_one_meth [(TcTyVar, PredType)]
gen_dms }
inferConstraintsCoerceBased :: [Type] -> Type
-> DerivM [ThetaOrigin]
inferConstraintsCoerceBased :: ThetaType -> PredType -> DerivM [ThetaOrigin]
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 } <- ReaderT DerivEnv (IOEnv (Env TcGblEnv TcLclEnv)) DerivEnv
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 ThetaType -> ThetaType -> ThetaType
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 -> PredOrigin
rep_pred_o PredType
ty = CtOrigin -> TypeOrKind -> PredType -> PredOrigin
mkPredOrigin CtOrigin
deriv_origin TypeOrKind
TypeLevel (PredType -> PredType
rep_pred PredType
ty)
deriv_origin :: CtOrigin
deriv_origin = Bool -> CtOrigin
mkDerivOrigin Bool
sa_wildcard
meth_preds :: Type -> [PredOrigin]
meth_preds :: PredType -> [PredOrigin]
meth_preds PredType
ty
| [TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
meths = []
| Bool
otherwise = PredType -> PredOrigin
rep_pred_o PredType
ty PredOrigin -> [PredOrigin] -> [PredOrigin]
forall a. a -> [a] -> [a]
: PredType -> [PredOrigin]
coercible_constraints PredType
ty
meths :: [TcTyVar]
meths = Class -> [TcTyVar]
classMethods Class
cls
coercible_constraints :: PredType -> [PredOrigin]
coercible_constraints PredType
ty
= [ CtOrigin -> TypeOrKind -> PredType -> PredOrigin
mkPredOrigin (TcTyVar -> PredType -> PredType -> Bool -> CtOrigin
DerivOriginCoerce TcTyVar
meth PredType
t1 PredType
t2 Bool
sa_wildcard)
TypeOrKind
TypeLevel (PredType -> PredType -> PredType
mkReprPrimEqPred PredType
t1 PredType
t2)
| 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 ]
all_thetas :: Type -> [ThetaOrigin]
all_thetas :: PredType -> [ThetaOrigin]
all_thetas PredType
ty = [[PredOrigin] -> ThetaOrigin
mkThetaOriginFromPreds ([PredOrigin] -> ThetaOrigin) -> [PredOrigin] -> ThetaOrigin
forall a b. (a -> b) -> a -> b
$ PredType -> [PredOrigin]
meth_preds PredType
ty]
[ThetaOrigin] -> DerivM [ThetaOrigin]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PredType -> [ThetaOrigin]
all_thetas PredType
rep_ty)
simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]]
-> TcM [DerivSpec ThetaType]
simplifyInstanceContexts :: [DerivSpec [ThetaOrigin]] -> TcM [DerivSpec ThetaType]
simplifyInstanceContexts [] = [DerivSpec ThetaType] -> TcM [DerivSpec ThetaType]
forall (m :: * -> *) a. Monad m => a -> m a
return []
simplifyInstanceContexts [DerivSpec [ThetaOrigin]]
infer_specs
= do { String -> SDoc -> TcRn ()
traceTc String
"simplifyInstanceContexts" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat ((DerivSpec [ThetaOrigin] -> SDoc)
-> [DerivSpec [ThetaOrigin]] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map DerivSpec [ThetaOrigin] -> SDoc
forall theta. Outputable theta => DerivSpec theta -> SDoc
pprDerivSpec [DerivSpec [ThetaOrigin]]
infer_specs)
; Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
iterate_deriv Int
1 [ThetaType]
initial_solutions }
where
initial_solutions :: [ThetaType]
initial_solutions :: [ThetaType]
initial_solutions = [ [] | DerivSpec [ThetaOrigin]
_ <- [DerivSpec [ThetaOrigin]]
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
20
= String -> SDoc -> TcM [DerivSpec ThetaType]
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"solveDerivEqns: probable loop"
([SDoc] -> SDoc
vcat ((DerivSpec [ThetaOrigin] -> SDoc)
-> [DerivSpec [ThetaOrigin]] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map DerivSpec [ThetaOrigin] -> SDoc
forall theta. Outputable theta => DerivSpec theta -> SDoc
pprDerivSpec [DerivSpec [ThetaOrigin]]
infer_specs) SDoc -> SDoc -> SDoc
$$ [ThetaType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ThetaType]
current_solns)
| Bool
otherwise
= do {
[ClsInst]
inst_specs <- (ThetaType
-> DerivSpec [ThetaOrigin]
-> IOEnv (Env TcGblEnv TcLclEnv) ClsInst)
-> [ThetaType]
-> [DerivSpec [ThetaOrigin]]
-> IOEnv (Env TcGblEnv TcLclEnv) [ClsInst]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM ThetaType
-> DerivSpec [ThetaOrigin] -> IOEnv (Env TcGblEnv TcLclEnv) ClsInst
forall theta.
ThetaType
-> DerivSpec theta -> IOEnv (Env TcGblEnv TcLclEnv) ClsInst
newDerivClsInst [ThetaType]
current_solns [DerivSpec [ThetaOrigin]]
infer_specs
; [ThetaType]
new_solns <- TcM [ThetaType] -> TcM [ThetaType]
forall r. TcM r -> TcM r
checkNoErrs (TcM [ThetaType] -> TcM [ThetaType])
-> TcM [ThetaType] -> TcM [ThetaType]
forall a b. (a -> b) -> a -> b
$
[ClsInst] -> TcM [ThetaType] -> TcM [ThetaType]
forall a. [ClsInst] -> TcM a -> TcM a
extendLocalInstEnv [ClsInst]
inst_specs (TcM [ThetaType] -> TcM [ThetaType])
-> TcM [ThetaType] -> TcM [ThetaType]
forall a b. (a -> b) -> a -> b
$
(DerivSpec [ThetaOrigin]
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType)
-> [DerivSpec [ThetaOrigin]] -> TcM [ThetaType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM DerivSpec [ThetaOrigin] -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
gen_soln [DerivSpec [ThetaOrigin]]
infer_specs
; if ([ThetaType]
current_solns [ThetaType] -> [ThetaType] -> Bool
`eqSolution` [ThetaType]
new_solns) then
[DerivSpec ThetaType] -> TcM [DerivSpec ThetaType]
forall (m :: * -> *) a. Monad m => a -> m a
return [ DerivSpec [ThetaOrigin]
spec { ds_theta :: ThetaType
ds_theta = ThetaType
soln }
| (DerivSpec [ThetaOrigin]
spec, ThetaType
soln) <- [DerivSpec [ThetaOrigin]]
-> [ThetaType] -> [(DerivSpec [ThetaOrigin], ThetaType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [DerivSpec [ThetaOrigin]]
infer_specs [ThetaType]
current_solns ]
else
Int -> [ThetaType] -> TcM [DerivSpec ThetaType]
iterate_deriv (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [ThetaType]
new_solns }
eqSolution :: [ThetaType] -> [ThetaType] -> Bool
eqSolution [ThetaType]
a [ThetaType]
b = (ThetaType -> ThetaType -> Bool)
-> [ThetaType] -> [ThetaType] -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy ((PredType -> PredType -> Bool) -> ThetaType -> ThetaType -> Bool
forall a. (a -> a -> Bool) -> [a] -> [a] -> Bool
eqListBy PredType -> PredType -> Bool
eqType) ([ThetaType] -> [ThetaType]
canSolution [ThetaType]
a) ([ThetaType] -> [ThetaType]
canSolution [ThetaType]
b)
canSolution :: [ThetaType] -> [ThetaType]
canSolution = (ThetaType -> ThetaType) -> [ThetaType] -> [ThetaType]
forall a b. (a -> b) -> [a] -> [b]
map ((PredType -> PredType -> Ordering) -> ThetaType -> ThetaType
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy PredType -> PredType -> Ordering
nonDetCmpType)
gen_soln :: DerivSpec [ThetaOrigin] -> TcM ThetaType
gen_soln :: DerivSpec [ThetaOrigin] -> IOEnv (Env TcGblEnv TcLclEnv) 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 = [ThetaOrigin]
deriv_rhs })
= SrcSpan
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (IOEnv (Env TcGblEnv TcLclEnv) ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType)
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall a b. (a -> b) -> a -> b
$
SDoc
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (PredType -> SDoc
derivInstCtxt PredType
the_pred) (IOEnv (Env TcGblEnv TcLclEnv) ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType)
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall a b. (a -> b) -> a -> b
$
do { ThetaType
theta <- PredType
-> [TcTyVar]
-> [ThetaOrigin]
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
simplifyDeriv PredType
the_pred [TcTyVar]
tyvars [ThetaOrigin]
deriv_rhs
; String -> SDoc -> TcRn ()
traceTc String
"GHC.Tc.Deriv" ([ThetaOrigin] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ThetaOrigin]
deriv_rhs SDoc -> SDoc -> SDoc
$$ ThetaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
theta)
; ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
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
= String -> SDoc
text String
"When deriving the instance for" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
pred)
simplifyDeriv :: PredType
-> [TyVar]
-> [ThetaOrigin]
-> TcM ThetaType
simplifyDeriv :: PredType
-> [TcTyVar]
-> [ThetaOrigin]
-> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
simplifyDeriv PredType
pred [TcTyVar]
tvs [ThetaOrigin]
thetas
= do { (TCvSubst
skol_subst, [TcTyVar]
tvs_skols) <- [TcTyVar] -> TcM (TCvSubst, [TcTyVar])
tcInstSkolTyVars [TcTyVar]
tvs
; let skol_set :: VarSet
skol_set = [TcTyVar] -> VarSet
mkVarSet [TcTyVar]
tvs_skols
skol_info :: SkolemInfo
skol_info = PredType -> SkolemInfo
DerivSkol PredType
pred
doc :: SDoc
doc = String -> SDoc
text String
"deriving" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr PredType
pred)
mk_given_ev :: PredType -> TcM EvVar
mk_given_ev :: PredType -> TcM TcTyVar
mk_given_ev PredType
given =
let given_pred :: PredType
given_pred = HasCallStack => TCvSubst -> PredType -> PredType
TCvSubst -> PredType -> PredType
substTy TCvSubst
skol_subst PredType
given
in PredType -> TcM TcTyVar
forall gbl lcl. PredType -> TcRnIf gbl lcl TcTyVar
newEvVar PredType
given_pred
emit_wanted_constraints :: [TyVar] -> [PredOrigin] -> TcM ()
emit_wanted_constraints :: [TcTyVar] -> [PredOrigin] -> TcRn ()
emit_wanted_constraints [TcTyVar]
metas_to_be [PredOrigin]
preds
= do {
(TCvSubst
meta_subst, [TcTyVar]
_meta_tvs) <- [TcTyVar] -> TcM (TCvSubst, [TcTyVar])
newMetaTyVars [TcTyVar]
metas_to_be
; let wanted_subst :: TCvSubst
wanted_subst = TCvSubst
skol_subst TCvSubst -> TCvSubst -> TCvSubst
`unionTCvSubst` TCvSubst
meta_subst
mk_wanted_ct :: PredOrigin -> IOEnv (Env TcGblEnv TcLclEnv) Ct
mk_wanted_ct (PredOrigin PredType
wanted CtOrigin
orig TypeOrKind
t_or_k)
= do { CtEvidence
ev <- CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence
newWanted CtOrigin
orig (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
t_or_k) (PredType -> TcM CtEvidence) -> PredType -> TcM CtEvidence
forall a b. (a -> b) -> a -> b
$
TCvSubst -> PredType -> PredType
substTyUnchecked TCvSubst
wanted_subst PredType
wanted
; Ct -> IOEnv (Env TcGblEnv TcLclEnv) Ct
forall (m :: * -> *) a. Monad m => a -> m a
return (CtEvidence -> Ct
mkNonCanonical CtEvidence
ev) }
; [Ct]
cts <- (PredOrigin -> IOEnv (Env TcGblEnv TcLclEnv) Ct)
-> [PredOrigin] -> IOEnv (Env TcGblEnv TcLclEnv) [Ct]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PredOrigin -> IOEnv (Env TcGblEnv TcLclEnv) Ct
mk_wanted_ct [PredOrigin]
preds
; Cts -> TcRn ()
emitSimples ([Ct] -> Cts
listToCts [Ct]
cts) }
mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
mk_wanteds :: ThetaOrigin -> TcM WantedConstraints
mk_wanteds (ThetaOrigin { to_anyclass_skols :: ThetaOrigin -> [TcTyVar]
to_anyclass_skols = [TcTyVar]
ac_skols
, to_anyclass_metas :: ThetaOrigin -> [TcTyVar]
to_anyclass_metas = [TcTyVar]
ac_metas
, to_anyclass_givens :: ThetaOrigin -> ThetaType
to_anyclass_givens = ThetaType
ac_givens
, to_wanted_origins :: ThetaOrigin -> [PredOrigin]
to_wanted_origins = [PredOrigin]
preds })
= do { [TcTyVar]
ac_given_evs <- (PredType -> TcM TcTyVar)
-> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PredType -> TcM TcTyVar
mk_given_ev ThetaType
ac_givens
; ((TcEvBinds, ())
_, WantedConstraints
wanteds)
<- TcM (TcEvBinds, ()) -> TcM ((TcEvBinds, ()), WantedConstraints)
forall a. TcM a -> TcM (a, WantedConstraints)
captureConstraints (TcM (TcEvBinds, ()) -> TcM ((TcEvBinds, ()), WantedConstraints))
-> TcM (TcEvBinds, ()) -> TcM ((TcEvBinds, ()), WantedConstraints)
forall a b. (a -> b) -> a -> b
$
SkolemInfo
-> [TcTyVar] -> [TcTyVar] -> TcRn () -> TcM (TcEvBinds, ())
forall result.
SkolemInfo
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfo
skol_info [TcTyVar]
ac_skols [TcTyVar]
ac_given_evs (TcRn () -> TcM (TcEvBinds, ())) -> TcRn () -> TcM (TcEvBinds, ())
forall a b. (a -> b) -> a -> b
$
[TcTyVar] -> [PredOrigin] -> TcRn ()
emit_wanted_constraints [TcTyVar]
ac_metas [PredOrigin]
preds
; WantedConstraints -> TcM WantedConstraints
forall (f :: * -> *) a. Applicative f => a -> f a
pure WantedConstraints
wanteds }
; (TcLevel
tc_lvl, [WantedConstraints]
wanteds) <- TcM [WantedConstraints] -> TcM (TcLevel, [WantedConstraints])
forall a. TcM a -> TcM (TcLevel, a)
pushTcLevelM (TcM [WantedConstraints] -> TcM (TcLevel, [WantedConstraints]))
-> TcM [WantedConstraints] -> TcM (TcLevel, [WantedConstraints])
forall a b. (a -> b) -> a -> b
$
(ThetaOrigin -> TcM WantedConstraints)
-> [ThetaOrigin] -> TcM [WantedConstraints]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ThetaOrigin -> TcM WantedConstraints
mk_wanteds [ThetaOrigin]
thetas
; String -> SDoc -> TcRn ()
traceTc String
"simplifyDeriv inputs" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ [TcTyVar] -> SDoc
pprTyVars [TcTyVar]
tvs SDoc -> SDoc -> SDoc
$$ [ThetaOrigin] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [ThetaOrigin]
thetas SDoc -> SDoc -> SDoc
$$ [WantedConstraints] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [WantedConstraints]
wanteds, SDoc
doc ]
; WantedConstraints
solved_wanteds <- TcLevel -> TcM WantedConstraints -> TcM WantedConstraints
forall a. TcLevel -> TcM a -> TcM a
setTcLevel TcLevel
tc_lvl (TcM WantedConstraints -> TcM WantedConstraints)
-> TcM WantedConstraints -> TcM WantedConstraints
forall a b. (a -> b) -> a -> b
$
TcS WantedConstraints -> TcM WantedConstraints
forall a. TcS a -> TcM a
runTcSDeriveds (TcS WantedConstraints -> TcM WantedConstraints)
-> TcS WantedConstraints -> TcM WantedConstraints
forall a b. (a -> b) -> a -> b
$
WantedConstraints -> TcS WantedConstraints
solveWantedsAndDrop (WantedConstraints -> TcS WantedConstraints)
-> WantedConstraints -> TcS WantedConstraints
forall a b. (a -> b) -> a -> b
$
[WantedConstraints] -> WantedConstraints
unionsWC [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 = (Ct -> Maybe PredType) -> Cts -> Bag PredType
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
, Ct -> Bool
isWantedCt Ct
ct
= 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
; String -> SDoc -> TcRn ()
traceTc String
"simplifyDeriv outputs" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
tvs_skols, Cts -> SDoc
forall a. Outputable a => a -> SDoc
ppr Cts
residual_simple, Bag PredType -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag PredType
good ]
; let min_theta :: ThetaType
min_theta = (PredType -> PredType) -> ThetaType -> ThetaType
forall a. (a -> PredType) -> [a] -> [a]
mkMinimalBySCs PredType -> PredType
forall a. a -> a
id (Bag PredType -> ThetaType
forall a. Bag a -> [a]
bagToList Bag PredType
good)
subst_skol :: TCvSubst
subst_skol = [TcTyVar] -> ThetaType -> TCvSubst
HasDebugCallStack => [TcTyVar] -> ThetaType -> TCvSubst
zipTvSubst [TcTyVar]
tvs_skols (ThetaType -> TCvSubst) -> ThetaType -> TCvSubst
forall a b. (a -> b) -> a -> b
$ [TcTyVar] -> ThetaType
mkTyVarTys [TcTyVar]
tvs
; [TcTyVar]
min_theta_vars <- (PredType -> TcM TcTyVar)
-> ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) [TcTyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PredType -> TcM TcTyVar
forall gbl lcl. PredType -> TcRnIf gbl lcl TcTyVar
newEvVar ThetaType
min_theta
; (Bag Implication
leftover_implic, TcEvBinds
_)
<- TcLevel
-> SkolemInfo
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tc_lvl SkolemInfo
skol_info [TcTyVar]
tvs_skols
[TcTyVar]
min_theta_vars WantedConstraints
solved_wanteds
; Bag Implication -> TcRn ()
simplifyTopImplic Bag Implication
leftover_implic
; ThetaType -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => TCvSubst -> ThetaType -> ThetaType
TCvSubst -> ThetaType -> ThetaType
substTheta TCvSubst
subst_skol ThetaType
min_theta) }