{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RecordWildCards #-}
module GHC.Tc.Utils.Unify (
tcWrapResult, tcWrapResultO, tcWrapResultMono,
tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS,
tcSubTypeAmbiguity, tcSubMult,
checkConstraints, checkTvConstraints,
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
DeepSubsumptionFlag(..), getDeepSubsumptionFlag, isRhoTyDS,
tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
unifyExprType, unifyTypeAndEmit, promoteTcType,
swapOverTyVars, touchabilityAndShapeTest, checkTopShape, lhsPriority,
UnifyEnv(..), updUEnvLoc, setUEnvRole,
uType,
tcInfer,
matchExpectedListTy,
matchExpectedTyConApp,
matchExpectedAppTy,
matchExpectedFunTys,
matchExpectedFunKind,
matchActualFunTy, matchActualFunTys,
checkTyEqRhs, recurseIntoTyConApp,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
famAppArgFlags, checkPromoteFreeVars,
simpleUnifyCheck, UnifyCheckCaller(..),
fillInferResult,
) where
import GHC.Prelude
import GHC.Hs
import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, hasFixedRuntimeRep_syntactic )
import GHC.Tc.Utils.Env
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.TcType
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.CtLoc( CtLoc, mkKindEqLoc, adjustCtLoc )
import GHC.Tc.Types.Origin
import GHC.Tc.Zonk.TcType
import GHC.Core.Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs( isInjectiveInType )
import GHC.Core.TyCo.Ppr( debugPprType )
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Predicate( mkEqPredRole )
import GHC.Core.Multiplicity
import GHC.Core.Reduction
import qualified GHC.LanguageExtensions as LangExt
import GHC.Builtin.Types
import GHC.Types.Name
import GHC.Types.Id( idType )
import GHC.Types.Var as Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Basic
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
import GHC.Utils.Error
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import GHC.Driver.DynFlags
import GHC.Data.Bag
import GHC.Data.FastString( fsLit )
import Control.Monad
import Data.Monoid as DM ( Any(..) )
import qualified Data.Semigroup as S ( (<>) )
matchActualFunTy
:: ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Arity, TcType)
-> TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
matchActualFunTy :: ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Int, TcType)
-> TcType
-> TcM (HsWrapper, Scaled TcType, TcType)
matchActualFunTy ExpectedFunTyOrigin
herald Maybe TypedThing
mb_thing (Int, TcType)
err_info TcType
fun_ty
= Bool
-> SDoc
-> TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcType -> Bool
isRhoTy TcType
fun_ty) (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
fun_ty) (TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType))
-> TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType)
forall a b. (a -> b) -> a -> b
$
TcType -> TcM (HsWrapper, Scaled TcType, TcType)
go TcType
fun_ty
where
go :: TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
go :: TcType -> TcM (HsWrapper, Scaled TcType, TcType)
go TcType
ty | Just TcType
ty' <- TcType -> Maybe TcType
coreView TcType
ty = TcType -> TcM (HsWrapper, Scaled TcType, TcType)
go TcType
ty'
go (FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: TcType -> TcType
ft_mult = TcType
w, ft_arg :: TcType -> TcType
ft_arg = TcType
arg_ty, ft_res :: TcType -> TcType
ft_res = TcType
res_ty })
= Bool
-> TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType)
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af) (TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType))
-> TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType)
forall a b. (a -> b) -> a -> b
$
do { HasDebugCallStack => FixedRuntimeRepContext -> TcType -> TcM ()
FixedRuntimeRepContext -> TcType -> TcM ()
hasFixedRuntimeRep_syntactic (ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Int
1) TcType
arg_ty
; (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, TcType -> TcType -> Scaled TcType
forall a. TcType -> a -> Scaled a
Scaled TcType
w TcType
arg_ty, TcType
res_ty) }
go ty :: TcType
ty@(TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { cts <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
tv
; case cts of
Indirect TcType
ty' -> TcType -> TcM (HsWrapper, Scaled TcType, TcType)
go TcType
ty'
MetaDetails
Flexi -> TcType -> TcM (HsWrapper, Scaled TcType, TcType)
defer TcType
ty }
go TcType
ty = (TidyEnv -> ZonkM (TidyEnv, SDoc))
-> TcM (HsWrapper, Scaled TcType, TcType)
-> TcM (HsWrapper, Scaled TcType, TcType)
forall a. (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_ctxt TcType
ty) (TcType -> TcM (HsWrapper, Scaled TcType, TcType)
defer TcType
ty)
defer :: TcType -> TcM (HsWrapper, Scaled TcType, TcType)
defer TcType
fun_ty
= do { arg_ty <- ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
new_check_arg_ty ExpectedFunTyOrigin
herald Int
1
; res_ty <- newOpenFlexiTyVarTy
; let unif_fun_ty = [Scaled TcType] -> TcType -> TcType
HasDebugCallStack => [Scaled TcType] -> TcType -> TcType
mkScaledFunTys [Scaled TcType
arg_ty] TcType
res_ty
; co <- unifyType mb_thing fun_ty unif_fun_ty
; return (mkWpCastN co, arg_ty, res_ty) }
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_ctxt TcType
_res_ty = ExpectedFunTyOrigin
-> (Int, TcType) -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mkFunTysMsg ExpectedFunTyOrigin
herald (Int, TcType)
err_info
matchActualFunTys :: ExpectedFunTyOrigin
-> CtOrigin
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
matchActualFunTys :: ExpectedFunTyOrigin
-> CtOrigin
-> Int
-> TcType
-> TcM (HsWrapper, [Scaled TcType], TcType)
matchActualFunTys ExpectedFunTyOrigin
herald CtOrigin
ct_orig Int
n_val_args_wanted TcType
top_ty
= Int
-> [Scaled TcType]
-> TcType
-> TcM (HsWrapper, [Scaled TcType], TcType)
go Int
n_val_args_wanted [] TcType
top_ty
where
go :: Int
-> [Scaled TcType]
-> TcType
-> TcM (HsWrapper, [Scaled TcType], TcType)
go Int
n [Scaled TcType]
so_far TcType
fun_ty
| Bool -> Bool
not (TcType -> Bool
isRhoTy TcType
fun_ty)
= do { (wrap1, rho) <- CtOrigin -> TcType -> TcM (HsWrapper, TcType)
topInstantiate CtOrigin
ct_orig TcType
fun_ty
; (wrap2, arg_tys, res_ty) <- go n so_far rho
; return (wrap2 <.> wrap1, arg_tys, res_ty) }
go Int
0 [Scaled TcType]
_ TcType
fun_ty = (HsWrapper, [Scaled TcType], TcType)
-> TcM (HsWrapper, [Scaled TcType], TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, [], TcType
fun_ty)
go Int
n [Scaled TcType]
so_far TcType
fun_ty
= do { (wrap_fun1, arg_ty1, res_ty1) <- ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Int, TcType)
-> TcType
-> TcM (HsWrapper, Scaled TcType, TcType)
matchActualFunTy
ExpectedFunTyOrigin
herald Maybe TypedThing
forall a. Maybe a
Nothing
(Int
n_val_args_wanted, TcType
top_ty)
TcType
fun_ty
; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
; let wrap_fun2 = HsWrapper -> HsWrapper -> Scaled TcType -> TcType -> HsWrapper
mkWpFun HsWrapper
idHsWrapper HsWrapper
wrap_res Scaled TcType
arg_ty1 TcType
res_ty
; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
tcSkolemiseGeneral
:: DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType -> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral :: forall result.
DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral DeepSubsumptionFlag
ds_flag UserTypeCtxt
ctxt TcType
top_ty TcType
expected_ty [(Name, TcInvisTVBinder)] -> TcType -> TcM result
thing_inside
| DeepSubsumptionFlag -> TcType -> Bool
isRhoTyDS DeepSubsumptionFlag
ds_flag TcType
expected_ty
= do { let sig_skol :: SkolemInfoAnon
sig_skol = UserTypeCtxt -> TcType -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt TcType
top_ty []
; (ev_binds, result) <- SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfoAnon
sig_skol [] [] (TcM result -> TcM (TcEvBinds, result))
-> TcM result -> TcM (TcEvBinds, result)
forall a b. (a -> b) -> a -> b
$
[(Name, TcInvisTVBinder)] -> TcType -> TcM result
thing_inside [] TcType
expected_ty
; return (mkWpLet ev_binds, result) }
| Bool
otherwise
= do {
; rec { (wrap, tv_prs, given, rho_ty) <- case ds_flag of
DeepSubsumptionFlag
Deep -> SkolemInfo
-> TcType
-> IOEnv
(Env TcGblEnv TcLclEnv)
(HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
deeplySkolemise SkolemInfo
skol_info TcType
expected_ty
DeepSubsumptionFlag
Shallow -> SkolemInfo
-> TcType
-> IOEnv
(Env TcGblEnv TcLclEnv)
(HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
topSkolemise SkolemInfo
skol_info TcType
expected_ty
; let sig_skol = UserTypeCtxt -> TcType -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt TcType
top_ty (((Name, TcInvisTVBinder) -> (Name, TcTyVar))
-> [(Name, TcInvisTVBinder)] -> [(Name, TcTyVar)]
forall a b. (a -> b) -> [a] -> [b]
map ((TcInvisTVBinder -> TcTyVar)
-> (Name, TcInvisTVBinder) -> (Name, TcTyVar)
forall a b. (a -> b) -> (Name, a) -> (Name, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcInvisTVBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar) [(Name, TcInvisTVBinder)]
tv_prs)
; skol_info <- mkSkolemInfo sig_skol }
; let skol_tvs = ((Name, TcInvisTVBinder) -> TcTyVar)
-> [(Name, TcInvisTVBinder)] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (TcInvisTVBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar (TcInvisTVBinder -> TcTyVar)
-> ((Name, TcInvisTVBinder) -> TcInvisTVBinder)
-> (Name, TcInvisTVBinder)
-> TcTyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, TcInvisTVBinder) -> TcInvisTVBinder
forall a b. (a, b) -> b
snd) [(Name, TcInvisTVBinder)]
tv_prs
; traceTc "tcSkolemiseGeneral" (pprUserTypeCtxt ctxt <+> ppr skol_tvs <+> ppr given)
; (ev_binds, result) <- checkConstraints sig_skol skol_tvs given $
thing_inside tv_prs rho_ty
; return (wrap <.> mkWpLet ev_binds, result) }
tcSkolemiseCompleteSig :: TcCompleteSig
-> ([ExpPatType] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseCompleteSig :: forall result.
TcCompleteSig
-> ([ExpPatType] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseCompleteSig (CSig { sig_bndr :: TcCompleteSig -> TcTyVar
sig_bndr = TcTyVar
poly_id, sig_ctxt :: TcCompleteSig -> UserTypeCtxt
sig_ctxt = UserTypeCtxt
ctxt, sig_loc :: TcCompleteSig -> SrcSpan
sig_loc = SrcSpan
loc })
[ExpPatType] -> TcType -> TcM result
thing_inside
= do { cur_loc <- TcRn SrcSpan
getSrcSpanM
; let poly_ty = TcTyVar -> TcType
idType TcTyVar
poly_id
; setSrcSpan loc $
tcSkolemiseGeneral Shallow ctxt poly_ty poly_ty $ \[(Name, TcInvisTVBinder)]
tv_prs TcType
rho_ty ->
SrcSpan -> TcM result -> TcM result
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
cur_loc (TcM result -> TcM result) -> TcM result -> TcM result
forall a b. (a -> b) -> a -> b
$
[(Name, TcTyVar)] -> TcM result -> TcM result
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv (((Name, TcInvisTVBinder) -> (Name, TcTyVar))
-> [(Name, TcInvisTVBinder)] -> [(Name, TcTyVar)]
forall a b. (a -> b) -> [a] -> [b]
map ((TcInvisTVBinder -> TcTyVar)
-> (Name, TcInvisTVBinder) -> (Name, TcTyVar)
forall a b. (a -> b) -> (Name, a) -> (Name, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TcInvisTVBinder -> TcTyVar
forall tv argf. VarBndr tv argf -> tv
binderVar) [(Name, TcInvisTVBinder)]
tv_prs) (TcM result -> TcM result) -> TcM result -> TcM result
forall a b. (a -> b) -> a -> b
$
[ExpPatType] -> TcType -> TcM result
thing_inside (((Name, TcInvisTVBinder) -> ExpPatType)
-> [(Name, TcInvisTVBinder)] -> [ExpPatType]
forall a b. (a -> b) -> [a] -> [b]
map (TcInvisTVBinder -> ExpPatType
mkInvisExpPatType (TcInvisTVBinder -> ExpPatType)
-> ((Name, TcInvisTVBinder) -> TcInvisTVBinder)
-> (Name, TcInvisTVBinder)
-> ExpPatType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, TcInvisTVBinder) -> TcInvisTVBinder
forall a b. (a, b) -> b
snd) [(Name, TcInvisTVBinder)]
tv_prs) TcType
rho_ty }
tcSkolemiseExpectedType :: TcSigmaType
-> ([ExpPatType] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseExpectedType :: forall result.
TcType
-> ([ExpPatType] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseExpectedType TcType
exp_ty [ExpPatType] -> TcType -> TcM result
thing_inside
= DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
forall result.
DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral DeepSubsumptionFlag
Shallow UserTypeCtxt
GenSigCtxt TcType
exp_ty TcType
exp_ty (([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result))
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
forall a b. (a -> b) -> a -> b
$ \[(Name, TcInvisTVBinder)]
tv_prs TcType
rho_ty ->
[ExpPatType] -> TcType -> TcM result
thing_inside (((Name, TcInvisTVBinder) -> ExpPatType)
-> [(Name, TcInvisTVBinder)] -> [ExpPatType]
forall a b. (a -> b) -> [a] -> [b]
map (TcInvisTVBinder -> ExpPatType
mkInvisExpPatType (TcInvisTVBinder -> ExpPatType)
-> ((Name, TcInvisTVBinder) -> TcInvisTVBinder)
-> (Name, TcInvisTVBinder)
-> ExpPatType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, TcInvisTVBinder) -> TcInvisTVBinder
forall a b. (a, b) -> b
snd) [(Name, TcInvisTVBinder)]
tv_prs) TcType
rho_ty
tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType
-> (TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise :: forall result.
DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> (TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise DeepSubsumptionFlag
ds_flag UserTypeCtxt
ctxt TcType
expected_ty TcType -> TcM result
thing_inside
= DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
forall result.
DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral DeepSubsumptionFlag
ds_flag UserTypeCtxt
ctxt TcType
expected_ty TcType
expected_ty (([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result))
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
forall a b. (a -> b) -> a -> b
$ \[(Name, TcInvisTVBinder)]
_ TcType
rho_ty ->
TcType -> TcM result
thing_inside TcType
rho_ty
checkConstraints :: SkolemInfoAnon
-> [TcTyVar]
-> [EvVar]
-> TcM result
-> TcM (TcEvBinds, result)
checkConstraints :: forall result.
SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given TcM result
thing_inside
= do { implication_needed <- SkolemInfoAnon -> [TcTyVar] -> [TcTyVar] -> TcM Bool
implicationNeeded SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given
; if implication_needed
then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
; emitImplications implics
; return (ev_binds, result) }
else
do { res <- thing_inside
; return (emptyTcEvBinds, res) } }
checkTvConstraints :: SkolemInfo
-> [TcTyVar]
-> TcM result
-> TcM result
checkTvConstraints :: forall result. SkolemInfo -> [TcTyVar] -> TcM result -> TcM result
checkTvConstraints SkolemInfo
skol_info [TcTyVar]
skol_tvs TcM result
thing_inside
= do { (tclvl, wanted, result) <- TcM result -> TcM (TcLevel, WantedConstraints, result)
forall a. TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndCaptureConstraints TcM result
thing_inside
; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
; return result }
emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
| Bool -> Bool
not (WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted) Bool -> Bool -> Bool
||
SkolemInfoAnon -> Bool
checkTelescopeSkol SkolemInfoAnon
skol_info_anon
=
do { implic <- SkolemInfoAnon
-> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfoAnon
skol_info_anon [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; emitImplication implic }
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
skol_info_anon :: SkolemInfoAnon
skol_info_anon = SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info
buildTvImplication :: SkolemInfoAnon -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication :: SkolemInfoAnon
-> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
= Bool -> SDoc -> TcM Implication -> TcM Implication
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((TcTyVar -> Bool) -> [TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Bool
isSkolemTyVar (TcTyVar -> Bool) -> (TcTyVar -> Bool) -> TcTyVar -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> TcTyVar -> Bool
isTyVarTyVar) [TcTyVar]
skol_tvs) ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs) (TcM Implication -> TcM Implication)
-> TcM Implication -> TcM Implication
forall a b. (a -> b) -> a -> b
$
do { ev_binds <- TcM EvBindsVar
newNoTcEvBinds
; implic <- newImplication
; let implic' = Implication
implic { ic_tclvl = tclvl
, ic_skols = skol_tvs
, ic_given_eqs = NoGivenEqs
, ic_wanted = wanted
, ic_binds = ev_binds
, ic_info = skol_info }
; checkImplicationInvariants implic'
; return implic' }
implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [TcTyVar] -> TcM Bool
implicationNeeded SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given
| [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
skol_tvs
, [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
given
, Bool -> Bool
not (SkolemInfoAnon -> Bool
alwaysBuildImplication SkolemInfoAnon
skol_info)
=
do { tc_lvl <- TcM TcLevel
getTcLevel
; if not (isTopTcLevel tc_lvl)
then return False
else
do { dflags <- getDynFlags
; return (gopt Opt_DeferTypeErrors dflags ||
gopt Opt_DeferTypedHoles dflags ||
gopt Opt_DeferOutOfScopeVariables dflags) } }
| Bool
otherwise
= Bool -> TcM Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
alwaysBuildImplication :: SkolemInfoAnon -> Bool
alwaysBuildImplication :: SkolemInfoAnon -> Bool
alwaysBuildImplication SkolemInfoAnon
_ = Bool
False
buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar]
-> [EvVar] -> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor :: TcLevel
-> SkolemInfoAnon
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given WantedConstraints
wanted
| WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted Bool -> Bool -> Bool
&& [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
given
= (Bag Implication, TcEvBinds) -> TcM (Bag Implication, TcEvBinds)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag Implication
forall a. Bag a
emptyBag, TcEvBinds
emptyTcEvBinds)
| Bool
otherwise
= Bool
-> SDoc
-> TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((TcTyVar -> Bool) -> [TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Bool
isSkolemTyVar (TcTyVar -> Bool) -> (TcTyVar -> Bool) -> TcTyVar -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> TcTyVar -> Bool
isTyVarTyVar) [TcTyVar]
skol_tvs) ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs) (TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds))
-> TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds)
forall a b. (a -> b) -> a -> b
$
do { ev_binds_var <- TcM EvBindsVar
newTcEvBinds
; implic <- newImplication
; let implic' = Implication
implic { ic_tclvl = tclvl
, ic_skols = skol_tvs
, ic_given = given
, ic_wanted = wanted
, ic_binds = ev_binds_var
, ic_info = skol_info }
; checkImplicationInvariants implic'
; return (unitBag implic', TcEvBinds ev_binds_var) }
matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin
-> UserTypeCtxt
-> VisArity
-> ExpSigmaType
-> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin
-> UserTypeCtxt
-> Int
-> ExpRhoType
-> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys ExpectedFunTyOrigin
herald UserTypeCtxt
_ Int
arity (Infer InferResult
inf_res) [ExpPatType] -> ExpRhoType -> TcM a
thing_inside
= do { arg_tys <- (Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType))
-> [Int] -> IOEnv (Env TcGblEnv TcLclEnv) [Scaled ExpRhoType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ExpectedFunTyOrigin
-> Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
new_infer_arg_ty ExpectedFunTyOrigin
herald) [Int
1 .. Int
arity]
; res_ty <- newInferExpType
; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty
; arg_tys <- mapM (\(Scaled TcType
m ExpRhoType
t) -> TcType -> TcType -> Scaled TcType
forall a. TcType -> a -> Scaled a
Scaled TcType
m (TcType -> Scaled TcType) -> TcM TcType -> TcM (Scaled TcType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpRhoType -> TcM TcType
forall (m :: * -> *). MonadIO m => ExpRhoType -> m TcType
readExpType ExpRhoType
t) arg_tys
; res_ty <- readExpType res_ty
; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res
; return (mkWpCastN co, result) }
matchExpectedFunTys ExpectedFunTyOrigin
herald UserTypeCtxt
ctx Int
arity (Check TcType
top_ty) [ExpPatType] -> ExpRhoType -> TcM a
thing_inside
= Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
check Int
arity [] TcType
top_ty
where
check :: VisArity -> [ExpPatType] -> TcSigmaType -> TcM (HsWrapper, a)
check :: Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
check Int
n_req [ExpPatType]
rev_pat_tys TcType
ty
| TcType -> Bool
isSigmaTy TcType
ty
Bool -> Bool -> Bool
|| (Int
n_req Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& TcType -> Bool
isForAllTy TcType
ty)
= do { rec { (n_req', wrap_gen, tv_nms, bndrs, given, inner_ty) <- skolemiseRequired skol_info n_req ty
; let sig_skol = UserTypeCtxt -> TcType -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctx TcType
top_ty ([Name]
tv_nms [Name] -> [TcTyVar] -> [(Name, TcTyVar)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcTyVar]
skol_tvs)
skol_tvs = [ForAllTyBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [ForAllTyBinder]
bndrs
; skol_info <- mkSkolemInfo sig_skol }
; (ev_binds, (wrap_res, result))
<- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
check n_req'
(reverse (map ExpForAllPatTy bndrs) ++ rev_pat_tys)
inner_ty
; assertPpr (not (null bndrs && null given)) (ppr ty) $
return (wrap_gen <.> mkWpLet ev_binds <.> wrap_res, result) }
check Int
n_req [ExpPatType]
rev_pat_tys TcType
rho_ty
| Int
n_req Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
= do { let pat_tys :: [ExpPatType]
pat_tys = [ExpPatType] -> [ExpPatType]
forall a. [a] -> [a]
reverse [ExpPatType]
rev_pat_tys
; ds_flag <- TcM DeepSubsumptionFlag
getDeepSubsumptionFlag
; case ds_flag of
DeepSubsumptionFlag
Shallow -> do { res <- [ExpPatType] -> ExpRhoType -> TcM a
thing_inside [ExpPatType]
pat_tys (TcType -> ExpRhoType
mkCheckExpType TcType
rho_ty)
; return (idHsWrapper, res) }
DeepSubsumptionFlag
Deep -> DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
forall result.
DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> TcType
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseGeneral DeepSubsumptionFlag
Deep UserTypeCtxt
ctx TcType
top_ty TcType
rho_ty (([(Name, TcInvisTVBinder)] -> TcType -> TcM a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a))
-> ([(Name, TcInvisTVBinder)] -> TcType -> TcM a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$ \[(Name, TcInvisTVBinder)]
_ TcType
rho_ty ->
[ExpPatType] -> ExpRhoType -> TcM a
thing_inside [ExpPatType]
pat_tys (TcType -> ExpRhoType
mkCheckExpType TcType
rho_ty) }
check Int
n_req [ExpPatType]
rev_pat_tys (FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: TcType -> TcType
ft_mult = TcType
mult
, ft_arg :: TcType -> TcType
ft_arg = TcType
arg_ty, ft_res :: TcType -> TcType
ft_res = TcType
res_ty })
= Bool
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af) (IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a))
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$
do { let arg_pos :: Int
arg_pos = Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n_req Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
; (arg_co, arg_ty) <- HasDebugCallStack =>
FixedRuntimeRepContext -> TcType -> TcM (Coercion, TcType)
FixedRuntimeRepContext -> TcType -> TcM (Coercion, TcType)
hasFixedRuntimeRep (ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Int
arg_pos) TcType
arg_ty
; (wrap_res, result) <- check (n_req - 1)
(mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
res_ty
; let wrap_arg = Coercion -> HsWrapper
mkWpCastN Coercion
arg_co
fun_wrap = HsWrapper -> HsWrapper -> Scaled TcType -> TcType -> HsWrapper
mkWpFun HsWrapper
wrap_arg HsWrapper
wrap_res (TcType -> TcType -> Scaled TcType
forall a. TcType -> a -> Scaled a
Scaled TcType
mult TcType
arg_ty) TcType
res_ty
; return (fun_wrap, result) }
check Int
n_req [ExpPatType]
rev_pat_tys ty :: TcType
ty@(TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { cts <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
tv
; case cts of
Indirect TcType
ty' -> Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
check Int
n_req [ExpPatType]
rev_pat_tys TcType
ty'
MetaDetails
Flexi -> Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
defer Int
n_req [ExpPatType]
rev_pat_tys TcType
ty }
check Int
n_req [ExpPatType]
rev_pat_tys TcType
ty
| Just TcType
ty' <- TcType -> Maybe TcType
coreView TcType
ty = Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
check Int
n_req [ExpPatType]
rev_pat_tys TcType
ty'
check Int
n_req [ExpPatType]
rev_pat_tys TcType
res_ty
= (TidyEnv -> ZonkM (TidyEnv, SDoc))
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
forall a. (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (ExpectedFunTyOrigin
-> (Int, TcType) -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mkFunTysMsg ExpectedFunTyOrigin
herald (Int
arity, TcType
top_ty)) (IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a))
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$
Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
defer Int
n_req [ExpPatType]
rev_pat_tys TcType
res_ty
defer :: VisArity -> [ExpPatType] -> TcRhoType -> TcM (HsWrapper, a)
defer :: Int
-> [ExpPatType]
-> TcType
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, a)
defer Int
n_req [ExpPatType]
rev_pat_tys TcType
fun_ty
= do { more_arg_tys <- (Int -> TcM (Scaled TcType))
-> [Int] -> IOEnv (Env TcGblEnv TcLclEnv) [Scaled TcType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
new_check_arg_ty ExpectedFunTyOrigin
herald) [Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n_req Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 .. Int
arity]
; let all_pats = [ExpPatType] -> [ExpPatType]
forall a. [a] -> [a]
reverse [ExpPatType]
rev_pat_tys [ExpPatType] -> [ExpPatType] -> [ExpPatType]
forall a. [a] -> [a] -> [a]
++ (Scaled TcType -> ExpPatType) -> [Scaled TcType] -> [ExpPatType]
forall a b. (a -> b) -> [a] -> [b]
map Scaled TcType -> ExpPatType
mkCheckExpFunPatTy [Scaled TcType]
more_arg_tys
; res_ty <- newOpenFlexiTyVarTy
; result <- thing_inside all_pats (mkCheckExpType res_ty)
; co <- unifyType Nothing (mkScaledFunTys more_arg_tys res_ty) fun_ty
; return (mkWpCastN co, result) }
new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpSigmaTypeFRR)
new_infer_arg_ty :: ExpectedFunTyOrigin
-> Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
new_infer_arg_ty ExpectedFunTyOrigin
herald Int
arg_pos
= do { mult <- TcType -> TcM TcType
newFlexiTyVarTy TcType
multiplicityTy
; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
; return (mkScaled mult inf_hole) }
new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
new_check_arg_ty ExpectedFunTyOrigin
herald Int
arg_pos
= do { mult <- TcType -> TcM TcType
newFlexiTyVarTy TcType
multiplicityTy
; arg_ty <- newOpenFlexiFRRTyVarTy (FRRExpectedFunTy herald arg_pos)
; return (mkScaled mult arg_ty) }
mkFunTysMsg :: ExpectedFunTyOrigin
-> (VisArity, TcType)
-> TidyEnv -> ZonkM (TidyEnv, SDoc)
mkFunTysMsg :: ExpectedFunTyOrigin
-> (Int, TcType) -> TidyEnv -> ZonkM (TidyEnv, SDoc)
mkFunTysMsg ExpectedFunTyOrigin
herald (Int
n_vis_args_in_call, TcType
fun_ty) TidyEnv
env
= do { (env', fun_ty) <- TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
env TcType
fun_ty
; let (pi_ty_bndrs, _) = splitPiTys fun_ty
n_fun_args = (PiTyBinder -> Bool) -> [PiTyBinder] -> Int
forall a. (a -> Bool) -> [a] -> Int
count PiTyBinder -> Bool
isVisiblePiTyBinder [PiTyBinder]
pi_ty_bndrs
msg | Int
n_vis_args_in_call Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n_fun_args
= String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"In the result of a function call"
| Bool
otherwise
= SDoc -> Int -> SDoc -> SDoc
hang (SDoc
full_herald SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma)
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"but its type" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (TcType -> SDoc
pprSigmaType TcType
fun_ty)
, if Int
n_fun_args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has none"
else String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has only" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
speakN Int
n_fun_args])
; return (env', msg) }
where
full_herald :: SDoc
full_herald = ExpectedFunTyOrigin -> SDoc
pprExpectedFunTyHerald ExpectedFunTyOrigin
herald
SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc -> SDoc
speakNOf Int
n_vis_args_in_call (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"visible argument")
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
matchExpectedListTy :: TcType -> TcM (Coercion, TcType)
matchExpectedListTy TcType
exp_ty
= do { (co, [elt_ty]) <- TyCon -> TcType -> TcM (Coercion, [TcType])
matchExpectedTyConApp TyCon
listTyCon TcType
exp_ty
; return (co, elt_ty) }
matchExpectedTyConApp :: TyCon
-> TcRhoType
-> TcM (TcCoercionN,
[TcSigmaType])
matchExpectedTyConApp :: TyCon -> TcType -> TcM (Coercion, [TcType])
matchExpectedTyConApp TyCon
tc TcType
orig_ty
= Bool
-> SDoc -> TcM (Coercion, [TcType]) -> TcM (Coercion, [TcType])
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Bool
isAlgTyCon TyCon
tc) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc) (TcM (Coercion, [TcType]) -> TcM (Coercion, [TcType]))
-> TcM (Coercion, [TcType]) -> TcM (Coercion, [TcType])
forall a b. (a -> b) -> a -> b
$
TcType -> TcM (Coercion, [TcType])
go TcType
orig_ty
where
go :: TcType -> TcM (Coercion, [TcType])
go TcType
ty
| Just TcType
ty' <- TcType -> Maybe TcType
coreView TcType
ty
= TcType -> TcM (Coercion, [TcType])
go TcType
ty'
go ty :: TcType
ty@(TyConApp TyCon
tycon [TcType]
args)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tycon
= (Coercion, [TcType]) -> TcM (Coercion, [TcType])
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Coercion
mkNomReflCo TcType
ty, [TcType]
args)
go (TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { cts <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
tv
; case cts of
Indirect TcType
ty -> TcType -> TcM (Coercion, [TcType])
go TcType
ty
MetaDetails
Flexi -> TcM (Coercion, [TcType])
defer }
go TcType
_ = TcM (Coercion, [TcType])
defer
defer :: TcM (Coercion, [TcType])
defer
= do { (_, arg_tvs) <- [TcTyVar] -> TcM (Subst, [TcTyVar])
newMetaTyVars (TyCon -> [TcTyVar]
tyConTyVars TyCon
tc)
; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs)
; let args = [TcTyVar] -> [TcType]
mkTyVarTys [TcTyVar]
arg_tvs
tc_template = TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tc [TcType]
args
; co <- unifyType Nothing tc_template orig_ty
; return (co, args) }
matchExpectedAppTy :: TcRhoType
-> TcM (TcCoercion,
(TcSigmaType, TcSigmaType))
matchExpectedAppTy :: TcType -> TcM (Coercion, (TcType, TcType))
matchExpectedAppTy TcType
orig_ty
= TcType -> TcM (Coercion, (TcType, TcType))
go TcType
orig_ty
where
go :: TcType -> TcM (Coercion, (TcType, TcType))
go TcType
ty
| Just TcType
ty' <- TcType -> Maybe TcType
coreView TcType
ty = TcType -> TcM (Coercion, (TcType, TcType))
go TcType
ty'
| Just (TcType
fun_ty, TcType
arg_ty) <- TcType -> Maybe (TcType, TcType)
tcSplitAppTy_maybe TcType
ty
= (Coercion, (TcType, TcType)) -> TcM (Coercion, (TcType, TcType))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Coercion
mkNomReflCo TcType
orig_ty, (TcType
fun_ty, TcType
arg_ty))
go (TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { cts <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
tv
; case cts of
Indirect TcType
ty -> TcType -> TcM (Coercion, (TcType, TcType))
go TcType
ty
MetaDetails
Flexi -> TcM (Coercion, (TcType, TcType))
defer }
go TcType
_ = TcM (Coercion, (TcType, TcType))
defer
defer :: TcM (Coercion, (TcType, TcType))
defer
= do { ty1 <- TcType -> TcM TcType
newFlexiTyVarTy TcType
kind1
; ty2 <- newFlexiTyVarTy kind2
; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
; return (co, (ty1, ty2)) }
orig_kind :: TcType
orig_kind = HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
orig_ty
kind1 :: TcType
kind1 = HasDebugCallStack => TcType -> TcType -> TcType
TcType -> TcType -> TcType
mkVisFunTyMany TcType
liftedTypeKind TcType
orig_kind
kind2 :: TcType
kind2 = TcType
liftedTypeKind
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
fillInferResult :: TcType -> InferResult -> TcM Coercion
fillInferResult TcType
act_res_ty (IR { ir_uniq :: InferResult -> Unique
ir_uniq = Unique
u
, ir_lvl :: InferResult -> TcLevel
ir_lvl = TcLevel
res_lvl
, ir_frr :: InferResult -> Maybe FixedRuntimeRepContext
ir_frr = Maybe FixedRuntimeRepContext
mb_frr
, ir_ref :: InferResult -> IORef (Maybe TcType)
ir_ref = IORef (Maybe TcType)
ref })
= do { mb_exp_res_ty <- IORef (Maybe TcType)
-> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcType)
forall (m :: * -> *) a. MonadIO m => TcRef a -> m a
readTcRef IORef (Maybe TcType)
ref
; case mb_exp_res_ty of
Just TcType
exp_res_ty
-> do { String -> SDoc -> TcM ()
traceTc String
"Joining inferred ExpType" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
colon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
act_res_ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
exp_res_ty
; cur_lvl <- TcM TcLevel
getTcLevel
; unless (cur_lvl `sameDepthAs` res_lvl) $
ensureMonoType act_res_ty
; unifyType Nothing act_res_ty exp_res_ty }
Maybe TcType
Nothing
-> do { String -> SDoc -> TcM ()
traceTc String
"Filling inferred ExpType" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
act_res_ty
; (prom_co, act_res_ty) <- TcLevel -> TcType -> TcM (Coercion, TcType)
promoteTcType TcLevel
res_lvl TcType
act_res_ty
; (frr_co, act_res_ty) <-
case mb_frr of
Maybe FixedRuntimeRepContext
Nothing -> (Coercion, TcType) -> TcM (Coercion, TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Coercion
mkNomReflCo TcType
act_res_ty, TcType
act_res_ty)
Just FixedRuntimeRepContext
frr_orig -> HasDebugCallStack =>
FixedRuntimeRepContext -> TcType -> TcM (Coercion, TcType)
FixedRuntimeRepContext -> TcType -> TcM (Coercion, TcType)
hasFixedRuntimeRep FixedRuntimeRepContext
frr_orig TcType
act_res_ty
; let final_co = Coercion
prom_co HasDebugCallStack => Coercion -> Coercion -> Coercion
Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
frr_co
; writeTcRef ref (Just act_res_ty)
; return final_co }
}
tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResult :: HsExpr GhcRn
-> HsExpr GhcTc -> TcType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResult HsExpr GhcRn
rn_expr = CtOrigin
-> HsExpr GhcRn
-> HsExpr GhcTc
-> TcType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultO (HsExpr GhcRn -> CtOrigin
exprCtOrigin HsExpr GhcRn
rn_expr) HsExpr GhcRn
rn_expr
tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultO :: CtOrigin
-> HsExpr GhcRn
-> HsExpr GhcTc
-> TcType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultO CtOrigin
orig HsExpr GhcRn
rn_expr HsExpr GhcTc
expr TcType
actual_ty ExpRhoType
res_ty
= do { String -> SDoc -> TcM ()
traceTc String
"tcWrapResult" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Actual: " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
actual_ty
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Expected:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
res_ty ])
; wrap <- CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
orig UserTypeCtxt
GenSigCtxt (TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TypedThing -> Maybe TypedThing) -> TypedThing -> Maybe TypedThing
forall a b. (a -> b) -> a -> b
$ HsExpr GhcRn -> TypedThing
HsExprRnThing HsExpr GhcRn
rn_expr) TcType
actual_ty ExpRhoType
res_ty
; return (mkHsWrap wrap expr) }
tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
-> TcRhoType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultMono :: HsExpr GhcRn
-> HsExpr GhcTc -> TcType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
rn_expr HsExpr GhcTc
expr TcType
act_ty ExpRhoType
res_ty
= Bool -> SDoc -> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcType -> Bool
isRhoTy TcType
act_ty) (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
act_ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_expr) (TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc))
-> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
do { co <- HsExpr GhcRn -> TcType -> ExpRhoType -> TcM Coercion
unifyExpectedType HsExpr GhcRn
rn_expr TcType
act_ty ExpRhoType
res_ty
; return (mkHsWrapCo co expr) }
unifyExpectedType :: HsExpr GhcRn
-> TcRhoType
-> ExpRhoType
-> TcM TcCoercionN
unifyExpectedType :: HsExpr GhcRn -> TcType -> ExpRhoType -> TcM Coercion
unifyExpectedType HsExpr GhcRn
rn_expr TcType
act_ty ExpRhoType
exp_ty
= case ExpRhoType
exp_ty of
Infer InferResult
inf_res -> TcType -> InferResult -> TcM Coercion
fillInferResult TcType
act_ty InferResult
inf_res
Check TcType
exp_ty -> Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyType (TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TypedThing -> Maybe TypedThing) -> TypedThing -> Maybe TypedThing
forall a b. (a -> b) -> a -> b
$ HsExpr GhcRn -> TypedThing
HsExprRnThing HsExpr GhcRn
rn_expr) TcType
act_ty TcType
exp_ty
tcSubTypePat :: CtOrigin -> UserTypeCtxt
-> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypePat :: CtOrigin -> UserTypeCtxt -> ExpRhoType -> TcType -> TcM HsWrapper
tcSubTypePat CtOrigin
inst_orig UserTypeCtxt
ctxt (Check TcType
ty_actual) TcType
ty_expected
= (TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type TcType -> TcType -> TcM Coercion
unifyTypeET CtOrigin
inst_orig UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
tcSubTypePat CtOrigin
_ UserTypeCtxt
_ (Infer InferResult
inf_res) TcType
ty_expected
= do { co <- TcType -> InferResult -> TcM Coercion
fillInferResult TcType
ty_expected InferResult
inf_res
; return (mkWpCastN (mkSymCo co)) }
tcSubType :: CtOrigin -> UserTypeCtxt
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubType :: CtOrigin -> UserTypeCtxt -> TcType -> ExpRhoType -> TcM HsWrapper
tcSubType CtOrigin
orig UserTypeCtxt
ctxt TcType
ty_actual ExpRhoType
ty_expected
= TcType -> ExpRhoType -> TcM HsWrapper -> TcM HsWrapper
forall a. TcType -> ExpRhoType -> TcM a -> TcM a
addSubTypeCtxt TcType
ty_actual ExpRhoType
ty_expected (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"tcSubType" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt, TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_actual, ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
ty_expected])
; CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
orig UserTypeCtxt
ctxt Maybe TypedThing
forall a. Maybe a
Nothing TcType
ty_actual ExpRhoType
ty_expected }
tcSubTypeDS :: HsExpr GhcRn
-> TcRhoType
-> TcRhoType
-> TcM HsWrapper
tcSubTypeDS :: HsExpr GhcRn -> TcType -> TcType -> TcM HsWrapper
tcSubTypeDS HsExpr GhcRn
rn_expr TcType
act_rho TcType
exp_rho
= HasDebugCallStack =>
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type_deep (HsExpr GhcRn -> TcType -> TcType -> TcM Coercion
unifyExprType HsExpr GhcRn
rn_expr) CtOrigin
orig UserTypeCtxt
GenSigCtxt TcType
act_rho TcType
exp_rho
where
orig :: CtOrigin
orig = HsExpr GhcRn -> CtOrigin
exprCtOrigin HsExpr GhcRn
rn_expr
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
inst_orig UserTypeCtxt
ctxt Maybe TypedThing
m_thing TcType
ty_actual ExpRhoType
res_ty
= case ExpRhoType
res_ty of
Check TcType
ty_expected -> (TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type (Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyType Maybe TypedThing
m_thing) CtOrigin
inst_orig UserTypeCtxt
ctxt
TcType
ty_actual TcType
ty_expected
Infer InferResult
inf_res -> do { (wrap, rho) <- CtOrigin -> TcType -> TcM (HsWrapper, TcType)
topInstantiate CtOrigin
inst_orig TcType
ty_actual
; co <- fillInferResult rho inf_res
; return (mkWpCastN co <.> wrap) }
tcSubTypeSigma :: CtOrigin
-> UserTypeCtxt
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeSigma :: CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tcSubTypeSigma CtOrigin
orig UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
= (TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type (Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing) CtOrigin
orig UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
tcSubTypeAmbiguity :: UserTypeCtxt
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeAmbiguity :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tcSubTypeAmbiguity UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
= DeepSubsumptionFlag
-> (TcType -> TcType -> TcM Coercion)
-> CtOrigin
-> UserTypeCtxt
-> TcType
-> TcType
-> TcM HsWrapper
tc_sub_type_ds DeepSubsumptionFlag
Shallow (Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing)
(UserTypeCtxt -> CtOrigin
AmbiguityCheckOrigin UserTypeCtxt
ctxt)
UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
addSubTypeCtxt :: forall a. TcType -> ExpRhoType -> TcM a -> TcM a
addSubTypeCtxt TcType
ty_actual ExpRhoType
ty_expected TcM a
thing_inside
| TcType -> Bool
isRhoTy TcType
ty_actual
, ExpRhoType -> Bool
isRhoExpTy ExpRhoType
ty_expected
= TcM a
thing_inside
| Bool
otherwise
= (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM a -> TcM a
forall a. (TidyEnv -> ZonkM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_msg TcM a
thing_inside
where
mk_msg :: TidyEnv -> ZonkM (TidyEnv, SDoc)
mk_msg TidyEnv
tidy_env
= do { (tidy_env, ty_actual) <- TidyEnv -> TcType -> ZonkM (TidyEnv, TcType)
zonkTidyTcType TidyEnv
tidy_env TcType
ty_actual
; ty_expected <- readExpType ty_expected
; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected
; let msg = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"When checking that:")
Int
4 (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_actual)
, Int -> SDoc -> SDoc
nest Int
2 (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is more polymorphic than:")
Int
2 (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_expected)) ]
; return (tidy_env, msg) }
tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type :: (TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
= do { ds_flag <- TcM DeepSubsumptionFlag
getDeepSubsumptionFlag
; tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected }
tc_sub_type_ds :: DeepSubsumptionFlag
-> (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin -> UserTypeCtxt -> TcSigmaType
-> TcSigmaType -> TcM HsWrapper
tc_sub_type_ds :: DeepSubsumptionFlag
-> (TcType -> TcType -> TcM Coercion)
-> CtOrigin
-> UserTypeCtxt
-> TcType
-> TcType
-> TcM HsWrapper
tc_sub_type_ds DeepSubsumptionFlag
ds_flag TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
| TcType -> Bool
definitely_poly TcType
ty_expected
, DeepSubsumptionFlag -> TcType -> Bool
isRhoTyDS DeepSubsumptionFlag
ds_flag TcType
ty_actual
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type (drop to equality)" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_expected ]
; Coercion -> HsWrapper
mkWpCastN (Coercion -> HsWrapper) -> TcM Coercion -> TcM HsWrapper
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
TcType -> TcType -> TcM Coercion
unify TcType
ty_actual TcType
ty_expected }
| Bool
otherwise
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type (general case)" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_expected ]
; (sk_wrap, inner_wrap)
<- DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> (TcType -> TcM HsWrapper)
-> TcM (HsWrapper, HsWrapper)
forall result.
DeepSubsumptionFlag
-> UserTypeCtxt
-> TcType
-> (TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise DeepSubsumptionFlag
ds_flag UserTypeCtxt
ctxt TcType
ty_expected ((TcType -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper))
-> (TcType -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper)
forall a b. (a -> b) -> a -> b
$ \TcType
sk_rho ->
case DeepSubsumptionFlag
ds_flag of
DeepSubsumptionFlag
Deep -> HasDebugCallStack =>
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type_deep TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt TcType
ty_actual TcType
sk_rho
DeepSubsumptionFlag
Shallow -> (TcType -> TcType -> TcM Coercion)
-> CtOrigin -> TcType -> TcType -> TcM HsWrapper
tc_sub_type_shallow TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig TcType
ty_actual TcType
sk_rho
; return (sk_wrap <.> inner_wrap) }
tc_sub_type_shallow :: (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin
-> TcSigmaType
-> TcRhoType
-> TcM HsWrapper
tc_sub_type_shallow :: (TcType -> TcType -> TcM Coercion)
-> CtOrigin -> TcType -> TcType -> TcM HsWrapper
tc_sub_type_shallow TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig TcType
ty_actual TcType
sk_rho
= do { (wrap, rho_a) <- CtOrigin -> TcType -> TcM (HsWrapper, TcType)
topInstantiate CtOrigin
inst_orig TcType
ty_actual
; cow <- unify rho_a sk_rho
; return (mkWpCastN cow <.> wrap) }
definitely_poly :: TcType -> Bool
definitely_poly :: TcType -> Bool
definitely_poly TcType
ty
| ([TcTyVar]
tvs, [TcType]
theta, TcType
tau) <- TcType -> ([TcTyVar], [TcType], TcType)
tcSplitSigmaTy TcType
ty
, (TcTyVar
tv:[TcTyVar]
_) <- [TcTyVar]
tvs
, [TcType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcType]
theta
, TcTyVar
tv TcTyVar -> TcType -> Bool
`isInjectiveInType` TcType
tau
= Bool
True
| Bool
otherwise
= Bool
False
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM ()
tcSubMult :: CtOrigin -> TcType -> TcType -> TcM ()
tcSubMult CtOrigin
origin TcType
w_actual TcType
w_expected
| Just (TcType
w1, TcType
w2) <- TcType -> Maybe (TcType, TcType)
isMultMul TcType
w_actual =
do { CtOrigin -> TcType -> TcType -> TcM ()
tcSubMult CtOrigin
origin TcType
w1 TcType
w_expected
; CtOrigin -> TcType -> TcType -> TcM ()
tcSubMult CtOrigin
origin TcType
w2 TcType
w_expected }
tcSubMult CtOrigin
origin TcType
w_actual TcType
w_expected =
case TcType -> TcType -> IsSubmult
submult TcType
w_actual TcType
w_expected of
IsSubmult
Submult -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
IsSubmult
Unknown -> CtOrigin -> TcType -> TcType -> TcM ()
tcEqMult CtOrigin
origin TcType
w_actual TcType
w_expected
tcEqMult :: CtOrigin -> Mult -> Mult -> TcM ()
tcEqMult :: CtOrigin -> TcType -> TcType -> TcM ()
tcEqMult CtOrigin
origin TcType
w_actual TcType
w_expected = do
{
; coercion <- TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM Coercion
unifyTypeAndEmit TypeOrKind
TypeLevel CtOrigin
origin TcType
w_actual TcType
w_expected
; ensureReflMultiplicityCo coercion origin }
data DeepSubsumptionFlag = Deep | Shallow
instance Outputable DeepSubsumptionFlag where
ppr :: DeepSubsumptionFlag -> SDoc
ppr DeepSubsumptionFlag
Deep = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Deep"
ppr DeepSubsumptionFlag
Shallow = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Shallow"
getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag
getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag
getDeepSubsumptionFlag = do { ds <- Extension -> TcM Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DeepSubsumption
; if ds then return Deep else return Shallow }
tc_sub_type_deep :: HasDebugCallStack
=> (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcRhoType
-> TcM HsWrapper
tc_sub_type_deep :: HasDebugCallStack =>
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type_deep TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt TcType
ty_actual TcType
ty_expected
= Bool -> SDoc -> TcM HsWrapper -> TcM HsWrapper
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcType -> Bool
isDeepRhoTy TcType
ty_expected) (TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_expected) (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type_deep" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_expected ]
; TcType -> TcType -> TcM HsWrapper
go TcType
ty_actual TcType
ty_expected }
where
go :: TcType -> TcType -> TcM HsWrapper
go TcType
ty_a TcType
ty_e | Just TcType
ty_a' <- TcType -> Maybe TcType
coreView TcType
ty_a = TcType -> TcType -> TcM HsWrapper
go TcType
ty_a' TcType
ty_e
| Just TcType
ty_e' <- TcType -> Maybe TcType
coreView TcType
ty_e = TcType -> TcType -> TcM HsWrapper
go TcType
ty_a TcType
ty_e'
go (TyVarTy TcTyVar
tv_a) TcType
ty_e
= do { lookup_res <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcType)
isFilledMetaTyVar_maybe TcTyVar
tv_a
; case lookup_res of
Just TcType
ty_a' ->
do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type_deep following filled meta-tyvar:"
(TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv_a SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"-->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty_a')
; HasDebugCallStack =>
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
(TcType -> TcType -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
tc_sub_type_deep TcType -> TcType -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt TcType
ty_a' TcType
ty_e }
Maybe TcType
Nothing -> TcType -> TcType -> TcM HsWrapper
just_unify TcType
ty_actual TcType
ty_expected }
go ty_a :: TcType
ty_a@(FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af1, ft_mult :: TcType -> TcType
ft_mult = TcType
act_mult, ft_arg :: TcType -> TcType
ft_arg = TcType
act_arg, ft_res :: TcType -> TcType
ft_res = TcType
act_res })
ty_e :: TcType
ty_e@(FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af2, ft_mult :: TcType -> TcType
ft_mult = TcType
exp_mult, ft_arg :: TcType -> TcType
ft_arg = TcType
exp_arg, ft_res :: TcType -> TcType
ft_res = TcType
exp_res })
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af1, FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af2
= if (TcType -> Bool
isTauTy TcType
ty_a Bool -> Bool -> Bool
&& TcType -> Bool
isTauTy TcType
ty_e)
then TcType -> TcType -> TcM HsWrapper
just_unify TcType
ty_actual TcType
ty_expected
else
do { arg_wrap <- DeepSubsumptionFlag
-> (TcType -> TcType -> TcM Coercion)
-> CtOrigin
-> UserTypeCtxt
-> TcType
-> TcType
-> TcM HsWrapper
tc_sub_type_ds DeepSubsumptionFlag
Deep TcType -> TcType -> TcM Coercion
unify CtOrigin
given_orig UserTypeCtxt
GenSigCtxt TcType
exp_arg TcType
act_arg
; res_wrap <- tc_sub_type_deep unify inst_orig ctxt act_res exp_res
; tcEqMult inst_orig act_mult exp_mult
; return (mkWpFun arg_wrap res_wrap (Scaled exp_mult exp_arg) exp_res) }
where
given_orig :: CtOrigin
given_orig = SkolemInfoAnon -> CtOrigin
GivenOrigin (UserTypeCtxt -> TcType -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
GenSigCtxt TcType
exp_arg [])
go TcType
ty_a TcType
ty_e
| let ([TcTyVar]
tvs, [TcType]
theta, TcType
_) = TcType -> ([TcTyVar], [TcType], TcType)
tcSplitSigmaTy TcType
ty_a
, Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& [TcType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcType]
theta)
= do { (in_wrap, in_rho) <- CtOrigin -> TcType -> TcM (HsWrapper, TcType)
topInstantiate CtOrigin
inst_orig TcType
ty_a
; body_wrap <- tc_sub_type_deep unify inst_orig ctxt in_rho ty_e
; return (body_wrap <.> in_wrap) }
| Bool
otherwise
= do {
(inst_wrap, rho_a) <- CtOrigin -> TcType -> TcM (HsWrapper, TcType)
deeplyInstantiate CtOrigin
inst_orig TcType
ty_actual
; unify_wrap <- just_unify rho_a ty_expected
; return (unify_wrap <.> inst_wrap) }
just_unify :: TcType -> TcType -> TcM HsWrapper
just_unify TcType
ty_a TcType
ty_e = do { cow <- TcType -> TcType -> TcM Coercion
unify TcType
ty_a TcType
ty_e
; return (mkWpCastN cow) }
deeplySkolemise :: SkolemInfo -> TcSigmaType
-> TcM ( HsWrapper
, [(Name,TcInvisTVBinder)]
, [EvVar]
, TcRhoType )
deeplySkolemise :: SkolemInfo
-> TcType
-> IOEnv
(Env TcGblEnv TcLclEnv)
(HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
deeplySkolemise SkolemInfo
skol_info TcType
ty
= Subst
-> TcType
-> IOEnv
(Env TcGblEnv TcLclEnv)
(HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
go Subst
init_subst TcType
ty
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (TcType -> VarSet
tyCoVarsOfType TcType
ty))
go :: Subst
-> TcType
-> IOEnv
(Env TcGblEnv TcLclEnv)
(HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
go Subst
subst TcType
ty
| Just ([Scaled TcType]
arg_tys, [TcInvisTVBinder]
bndrs, [TcType]
theta, TcType
ty') <- TcType
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
tcDeepSplitSigmaTy_maybe TcType
ty
= do { let arg_tys' :: [Scaled TcType]
arg_tys' = HasDebugCallStack => Subst -> [Scaled TcType] -> [Scaled TcType]
Subst -> [Scaled TcType] -> [Scaled TcType]
substScaledTys Subst
subst [Scaled TcType]
arg_tys
; ids1 <- FastString -> [Scaled TcType] -> TcRnIf TcGblEnv TcLclEnv [TcTyVar]
forall gbl lcl.
FastString -> [Scaled TcType] -> TcRnIf gbl lcl [TcTyVar]
newSysLocalIds (String -> FastString
fsLit String
"dk") [Scaled TcType]
arg_tys'
; (subst', bndrs1) <- tcInstSkolTyVarBndrsX skol_info subst bndrs
; ev_vars1 <- newEvVars (substTheta subst' theta)
; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty'
; let tvs = [TcInvisTVBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs
tvs1 = [TcInvisTVBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs1
tv_prs1 = (TcTyVar -> Name) -> [TcTyVar] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> Name
tyVarName [TcTyVar]
tvs [Name] -> [TcInvisTVBinder] -> [(Name, TcInvisTVBinder)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcInvisTVBinder]
bndrs1
; return ( mkWpEta ids1 (mkWpTyLams tvs1
<.> mkWpEvLams ev_vars1
<.> wrap)
, tv_prs1 ++ tvs_prs2
, ev_vars1 ++ ev_vars2
, mkScaledFunTys arg_tys' rho ) }
| Bool
otherwise
= (HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
-> IOEnv
(Env TcGblEnv TcLclEnv)
(HsWrapper, [(Name, TcInvisTVBinder)], [TcTyVar], TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, [], [], HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst TcType
ty)
deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type)
deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, TcType)
deeplyInstantiate CtOrigin
orig TcType
ty
= Subst -> TcType -> TcM (HsWrapper, TcType)
go Subst
init_subst TcType
ty
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (TcType -> VarSet
tyCoVarsOfType TcType
ty))
go :: Subst -> TcType -> TcM (HsWrapper, TcType)
go Subst
subst TcType
ty
| Just ([Scaled TcType]
arg_tys, [TcInvisTVBinder]
bndrs, [TcType]
theta, TcType
rho) <- TcType
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
tcDeepSplitSigmaTy_maybe TcType
ty
= do { let tvs :: [TcTyVar]
tvs = [TcInvisTVBinder] -> [TcTyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TcInvisTVBinder]
bndrs
; (subst', tvs') <- Subst -> [TcTyVar] -> TcM (Subst, [TcTyVar])
newMetaTyVarsX Subst
subst [TcTyVar]
tvs
; let arg_tys' = HasDebugCallStack => Subst -> [Scaled TcType] -> [Scaled TcType]
Subst -> [Scaled TcType] -> [Scaled TcType]
substScaledTys Subst
subst' [Scaled TcType]
arg_tys
theta' = HasDebugCallStack => Subst -> [TcType] -> [TcType]
Subst -> [TcType] -> [TcType]
substTheta Subst
subst' [TcType]
theta
; ids1 <- newSysLocalIds (fsLit "di") arg_tys'
; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
; (wrap2, rho2) <- go subst' rho
; return (mkWpEta ids1 (wrap2 <.> wrap1),
mkScaledFunTys arg_tys' rho2) }
| Bool
otherwise
= do { let ty' :: TcType
ty' = HasDebugCallStack => Subst -> TcType -> TcType
Subst -> TcType -> TcType
substTy Subst
subst TcType
ty
; (HsWrapper, TcType) -> TcM (HsWrapper, TcType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, TcType
ty') }
tcDeepSplitSigmaTy_maybe
:: TcSigmaType -> Maybe ([Scaled TcType], [TcInvisTVBinder], ThetaType, TcSigmaType)
tcDeepSplitSigmaTy_maybe :: TcType
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
tcDeepSplitSigmaTy_maybe TcType
ty
= TcType
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
go TcType
ty
where
go :: TcType
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
go TcType
ty | Just (Scaled TcType
arg_ty, TcType
res_ty) <- TcType -> Maybe (Scaled TcType, TcType)
tcSplitFunTy_maybe TcType
ty
, Just ([Scaled TcType]
arg_tys, [TcInvisTVBinder]
tvs, [TcType]
theta, TcType
rho) <- TcType
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
go TcType
res_ty
= ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
forall a. a -> Maybe a
Just (Scaled TcType
arg_tyScaled TcType -> [Scaled TcType] -> [Scaled TcType]
forall a. a -> [a] -> [a]
:[Scaled TcType]
arg_tys, [TcInvisTVBinder]
tvs, [TcType]
theta, TcType
rho)
| ([TcInvisTVBinder]
tvs, [TcType]
theta, TcType
rho) <- TcType -> ([TcInvisTVBinder], [TcType], TcType)
tcSplitSigmaTyBndrs TcType
ty
, Bool -> Bool
not ([TcInvisTVBinder] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcInvisTVBinder]
tvs Bool -> Bool -> Bool
&& [TcType] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcType]
theta)
= ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
-> Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
forall a. a -> Maybe a
Just ([], [TcInvisTVBinder]
tvs, [TcType]
theta, TcType
rho)
| Bool
otherwise = Maybe ([Scaled TcType], [TcInvisTVBinder], [TcType], TcType)
forall a. Maybe a
Nothing
isDeepRhoTy :: TcType -> Bool
isDeepRhoTy :: TcType -> Bool
isDeepRhoTy TcType
ty
| Bool -> Bool
not (TcType -> Bool
isRhoTy TcType
ty) = Bool
False
| Just (Scaled TcType
_, TcType
res) <- TcType -> Maybe (Scaled TcType, TcType)
tcSplitFunTy_maybe TcType
ty = TcType -> Bool
isDeepRhoTy TcType
res
| Bool
otherwise = Bool
True
isRhoTyDS :: DeepSubsumptionFlag -> TcType -> Bool
isRhoTyDS :: DeepSubsumptionFlag -> TcType -> Bool
isRhoTyDS DeepSubsumptionFlag
ds_flag TcType
ty
= case DeepSubsumptionFlag
ds_flag of
DeepSubsumptionFlag
Shallow -> TcType -> Bool
isRhoTy TcType
ty
DeepSubsumptionFlag
Deep -> TcType -> Bool
isDeepRhoTy TcType
ty
unifyExprType :: HsExpr GhcRn -> TcType -> TcType -> TcM TcCoercionN
unifyExprType :: HsExpr GhcRn -> TcType -> TcType -> TcM Coercion
unifyExprType HsExpr GhcRn
rn_expr TcType
ty1 TcType
ty2
= Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyType (TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (HsExpr GhcRn -> TypedThing
HsExprRnThing HsExpr GhcRn
rn_expr)) TcType
ty1 TcType
ty2
unifyType :: Maybe TypedThing
-> TcTauType -> TcTauType
-> TcM TcCoercionN
unifyType :: Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyType Maybe TypedThing
thing TcType
ty1 TcType
ty2
= TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM Coercion
unifyTypeAndEmit TypeOrKind
TypeLevel CtOrigin
origin TcType
ty1 TcType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: TcType
uo_actual = TcType
ty1
, uo_expected :: TcType
uo_expected = TcType
ty2
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
thing
, uo_visible :: Bool
uo_visible = Bool
True }
unifyInvisibleType :: TcTauType -> TcTauType
-> TcM TcCoercionN
unifyInvisibleType :: TcType -> TcType -> TcM Coercion
unifyInvisibleType TcType
ty1 TcType
ty2
= TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM Coercion
unifyTypeAndEmit TypeOrKind
TypeLevel CtOrigin
origin TcType
ty1 TcType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: TcType
uo_actual = TcType
ty1
, uo_expected :: TcType
uo_expected = TcType
ty2
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
forall a. Maybe a
Nothing
, uo_visible :: Bool
uo_visible = Bool
False }
unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
unifyTypeET :: TcType -> TcType -> TcM Coercion
unifyTypeET TcType
ty1 TcType
ty2
= TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM Coercion
unifyTypeAndEmit TypeOrKind
TypeLevel CtOrigin
origin TcType
ty1 TcType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: TcType
uo_actual = TcType
ty2
, uo_expected :: TcType
uo_expected = TcType
ty1
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
forall a. Maybe a
Nothing
, uo_visible :: Bool
uo_visible = Bool
True }
unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN
unifyKind :: Maybe TypedThing -> TcType -> TcType -> TcM Coercion
unifyKind Maybe TypedThing
mb_thing TcType
ty1 TcType
ty2
= TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM Coercion
unifyTypeAndEmit TypeOrKind
KindLevel CtOrigin
origin TcType
ty1 TcType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: TcType
uo_actual = TcType
ty1
, uo_expected :: TcType
uo_expected = TcType
ty2
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
mb_thing
, uo_visible :: Bool
uo_visible = Bool
True }
unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN
unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM Coercion
unifyTypeAndEmit TypeOrKind
t_or_k CtOrigin
orig TcType
ty1 TcType
ty2
= do { ref <- Bag Ct -> IOEnv (Env TcGblEnv TcLclEnv) (TcRef (Bag Ct))
forall (m :: * -> *) a. MonadIO m => a -> m (TcRef a)
newTcRef Bag Ct
forall a. Bag a
emptyBag
; loc <- getCtLocM orig (Just t_or_k)
; let env = UE { u_loc :: CtLoc
u_loc = CtLoc
loc, u_role :: Role
u_role = Role
Nominal
, u_rewriters :: RewriterSet
u_rewriters = RewriterSet
emptyRewriterSet
, u_defer :: TcRef (Bag Ct)
u_defer = TcRef (Bag Ct)
ref, u_unified :: Maybe (TcRef [TcTyVar])
u_unified = Maybe (TcRef [TcTyVar])
forall a. Maybe a
Nothing }
; co <- uType env ty1 ty2
; cts <- readTcRef ref
; unless (null cts) (emitSimples cts)
; return co }
data UnifyEnv
= UE { UnifyEnv -> Role
u_role :: Role
, UnifyEnv -> CtLoc
u_loc :: CtLoc
, UnifyEnv -> RewriterSet
u_rewriters :: RewriterSet
, UnifyEnv -> TcRef (Bag Ct)
u_defer :: TcRef (Bag Ct)
, UnifyEnv -> Maybe (TcRef [TcTyVar])
u_unified :: Maybe (TcRef [TcTyVar])
}
setUEnvRole :: UnifyEnv -> Role -> UnifyEnv
setUEnvRole :: UnifyEnv -> Role -> UnifyEnv
setUEnvRole UnifyEnv
uenv Role
role = UnifyEnv
uenv { u_role = role }
updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv
updUEnvLoc uenv :: UnifyEnv
uenv@(UE { u_loc :: UnifyEnv -> CtLoc
u_loc = CtLoc
loc }) CtLoc -> CtLoc
upd = UnifyEnv
uenv { u_loc = upd loc }
mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
mkKindEnv env :: UnifyEnv
env@(UE { u_loc :: UnifyEnv -> CtLoc
u_loc = CtLoc
ctloc }) TcType
ty1 TcType
ty2
= UnifyEnv
env { u_role = Nominal, u_loc = mkKindEqLoc ty1 ty2 ctloc }
uType, uType_defer
:: UnifyEnv
-> TcType
-> TcType
-> TcM CoercionN
uType_defer :: UnifyEnv -> TcType -> TcType -> TcM Coercion
uType_defer (UE { u_loc :: UnifyEnv -> CtLoc
u_loc = CtLoc
loc, u_defer :: UnifyEnv -> TcRef (Bag Ct)
u_defer = TcRef (Bag Ct)
ref
, u_role :: UnifyEnv -> Role
u_role = Role
role, u_rewriters :: UnifyEnv -> RewriterSet
u_rewriters = RewriterSet
rewriters })
TcType
ty1 TcType
ty2
= do { let pred_ty :: TcType
pred_ty = Role -> TcType -> TcType -> TcType
mkEqPredRole Role
role TcType
ty1 TcType
ty2
; hole <- CtLoc -> TcType -> TcM CoercionHole
newCoercionHole CtLoc
loc TcType
pred_ty
; let ct = CtEvidence -> Ct
mkNonCanonical (CtEvidence -> Ct) -> CtEvidence -> Ct
forall a b. (a -> b) -> a -> b
$
CtWanted { ctev_pred :: TcType
ctev_pred = TcType
pred_ty
, ctev_dest :: TcEvDest
ctev_dest = CoercionHole -> TcEvDest
HoleDest CoercionHole
hole
, ctev_loc :: CtLoc
ctev_loc = CtLoc
loc
, ctev_rewriters :: RewriterSet
ctev_rewriters = RewriterSet
rewriters }
co = CoercionHole -> Coercion
HoleCo CoercionHole
hole
; updTcRef ref (`snocBag` ct)
; whenDOptM Opt_D_dump_tc_trace $
do { ctxt <- getErrCtxt
; doc <- mkErrInfo emptyTidyEnv ctxt
; traceTc "utype_defer" (vcat [ ppr role
, debugPprType ty1
, debugPprType ty2
, doc])
; traceTc "utype_defer2" (ppr co) }
; return co }
uType :: UnifyEnv -> TcType -> TcType -> TcM Coercion
uType env :: UnifyEnv
env@(UE { u_role :: UnifyEnv -> Role
u_role = Role
role }) TcType
orig_ty1 TcType
orig_ty2
| Role
Phantom <- Role
role
= do { kind_co <- UnifyEnv -> TcType -> TcType -> TcM Coercion
uType (UnifyEnv -> TcType -> TcType -> UnifyEnv
mkKindEnv UnifyEnv
env TcType
orig_ty1 TcType
orig_ty2)
(HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
orig_ty1) (HasDebugCallStack => TcType -> TcType
TcType -> TcType
typeKind TcType
orig_ty2)
; return (mkPhantomCo kind_co orig_ty1 orig_ty2) }
| Bool
otherwise
= do { tclvl <- TcM TcLevel
getTcLevel
; traceTc "u_tys" $ vcat
[ text "tclvl" <+> ppr tclvl
, sep [ ppr orig_ty1, text "~" <> ppr role, ppr orig_ty2] ]
; co <- go orig_ty1 orig_ty2
; if isReflCo co
then traceTc "u_tys yields no coercion" Outputable.empty
else traceTc "u_tys yields coercion:" (ppr co)
; return co }
where
go :: TcType -> TcType -> TcM CoercionN
go :: TcType -> TcType -> TcM Coercion
go (CastTy TcType
t1 Coercion
co1) TcType
t2
= do { co_tys <- UnifyEnv -> TcType -> TcType -> TcM Coercion
uType UnifyEnv
env TcType
t1 TcType
t2
; return (mkCoherenceLeftCo role t1 co1 co_tys) }
go TcType
t1 (CastTy TcType
t2 Coercion
co2)
= do { co_tys <- UnifyEnv -> TcType -> TcType -> TcM Coercion
uType UnifyEnv
env TcType
t1 TcType
t2
; return (mkCoherenceRightCo role t2 co2 co_tys) }
go (TyVarTy TcTyVar
tv1) TcType
ty2
= do { lookup_res <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcType)
isFilledMetaTyVar_maybe TcTyVar
tv1
; case lookup_res of
Just TcType
ty1 -> do { String -> SDoc -> TcM ()
traceTc String
"found filled tyvar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1)
; UnifyEnv -> TcType -> TcType -> TcM Coercion
uType UnifyEnv
env TcType
ty1 TcType
orig_ty2 }
Maybe TcType
Nothing -> UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar UnifyEnv
env SwapFlag
NotSwapped TcTyVar
tv1 TcType
ty2 }
go TcType
ty1 (TyVarTy TcTyVar
tv2)
= do { lookup_res <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcType)
isFilledMetaTyVar_maybe TcTyVar
tv2
; case lookup_res of
Just TcType
ty2 -> do { String -> SDoc -> TcM ()
traceTc String
"found filled tyvar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv2 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
; UnifyEnv -> TcType -> TcType -> TcM Coercion
uType UnifyEnv
env TcType
orig_ty1 TcType
ty2 }
Maybe TcType
Nothing -> UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar UnifyEnv
env SwapFlag
IsSwapped TcTyVar
tv2 TcType
ty1 }
go ty1 :: TcType
ty1@(TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Role -> TcType -> Coercion
mkReflCo Role
role TcType
ty1
go TcType
ty1 TcType
ty2
| Just TcType
ty1' <- TcType -> Maybe TcType
coreView TcType
ty1 = TcType -> TcType -> TcM Coercion
go TcType
ty1' TcType
ty2
| Just TcType
ty2' <- TcType -> Maybe TcType
coreView TcType
ty2 = TcType -> TcType -> TcM Coercion
go TcType
ty1 TcType
ty2'
go (FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af1, ft_mult :: TcType -> TcType
ft_mult = TcType
w1, ft_arg :: TcType -> TcType
ft_arg = TcType
arg1, ft_res :: TcType -> TcType
ft_res = TcType
res1 })
(FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af2, ft_mult :: TcType -> TcType
ft_mult = TcType
w2, ft_arg :: TcType -> TcType
ft_arg = TcType
arg2, ft_res :: TcType -> TcType
ft_res = TcType
res2 })
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af1
, FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2
= do { co_w <- UnifyEnv -> TcType -> TcType -> TcM Coercion
uType (UnifyEnv
env { u_role = funRole role SelMult }) TcType
w1 TcType
w2
; co_l <- uType (env { u_role = funRole role SelArg }) arg1 arg2
; co_r <- uType (env { u_role = funRole role SelRes }) res1 res2
; return $ mkNakedFunCo role af1 co_w co_l co_r }
go ty1 :: TcType
ty1@(TyConApp TyCon
tc1 [TcType]
_) TcType
ty2
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1 = TcType -> TcType -> TcM Coercion
defer TcType
ty1 TcType
ty2
go TcType
ty1 ty2 :: TcType
ty2@(TyConApp TyCon
tc2 [TcType]
_)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2 = TcType -> TcType -> TcM Coercion
defer TcType
ty1 TcType
ty2
go (TyConApp TyCon
tc1 [TcType]
tys1) (TyConApp TyCon
tc2 [TcType]
tys2)
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2, [TcType] -> [TcType] -> Bool
forall a b. [a] -> [b] -> Bool
equalLength [TcType]
tys1 [TcType]
tys2
, TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc1 Role
role
= Bool -> SDoc -> TcM Coercion -> TcM Coercion
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc1 Role
role) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1) (TcM Coercion -> TcM Coercion) -> TcM Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"go-tycon" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcType]
tys1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcType]
tys2 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [Role] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Int -> [Role] -> [Role]
forall a. Int -> [a] -> [a]
take Int
10 (Role -> TyCon -> [Role]
tyConRoleListX Role
role TyCon
tc1)))
; cos <- (Bool -> Role -> TcType -> TcType -> TcM Coercion)
-> [Bool]
-> [Role]
-> [TcType]
-> [TcType]
-> IOEnv (Env TcGblEnv TcLclEnv) [Coercion]
forall (m :: * -> *) a b c d e.
Monad m =>
(a -> b -> c -> d -> m e) -> [a] -> [b] -> [c] -> [d] -> m [e]
zipWith4M Bool -> Role -> TcType -> TcType -> TcM Coercion
u_tc_arg (TyCon -> [Bool]
tyConVisibilities TyCon
tc1)
(Role -> TyCon -> [Role]
tyConRoleListX Role
role TyCon
tc1)
[TcType]
tys1 [TcType]
tys2
; return $ mkTyConAppCo role tc1 cos }
go (LitTy TyLit
m) ty :: TcType
ty@(LitTy TyLit
n)
| TyLit
m TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
n
= Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Role -> TcType -> Coercion
mkReflCo Role
role TcType
ty
go ty1 :: TcType
ty1@(AppTy TcType
s1 TcType
t1) ty2 :: TcType
ty2@(AppTy TcType
s2 TcType
t2)
= Bool
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcM Coercion
go_app (TcType -> Bool
isNextArgVisible TcType
s1) TcType
ty1 TcType
s1 TcType
t1 TcType
ty2 TcType
s2 TcType
t2
go ty1 :: TcType
ty1@(AppTy TcType
s1 TcType
t1) ty2 :: TcType
ty2@(TyConApp TyCon
tc2 [TcType]
ts2)
| Just ([TcType]
ts2', TcType
t2') <- [TcType] -> Maybe ([TcType], TcType)
forall a. [a] -> Maybe ([a], a)
snocView [TcType]
ts2
= Bool -> TcM Coercion -> TcM Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc2)) (TcM Coercion -> TcM Coercion) -> TcM Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$
Bool
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcM Coercion
go_app (TyCon -> [TcType] -> Bool
isNextTyConArgVisible TyCon
tc2 [TcType]
ts2')
TcType
ty1 TcType
s1 TcType
t1 TcType
ty2 (TyCon -> [TcType] -> TcType
TyConApp TyCon
tc2 [TcType]
ts2') TcType
t2'
go ty1 :: TcType
ty1@(TyConApp TyCon
tc1 [TcType]
ts1) ty2 :: TcType
ty2@(AppTy TcType
s2 TcType
t2)
| Just ([TcType]
ts1', TcType
t1') <- [TcType] -> Maybe ([TcType], TcType)
forall a. [a] -> Maybe ([a], a)
snocView [TcType]
ts1
= Bool -> TcM Coercion -> TcM Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc1)) (TcM Coercion -> TcM Coercion) -> TcM Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$
Bool
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcM Coercion
go_app (TyCon -> [TcType] -> Bool
isNextTyConArgVisible TyCon
tc1 [TcType]
ts1')
TcType
ty1 (TyCon -> [TcType] -> TcType
TyConApp TyCon
tc1 [TcType]
ts1') TcType
t1' TcType
ty2 TcType
s2 TcType
t2
go ty1 :: TcType
ty1@(CoercionTy Coercion
co1) ty2 :: TcType
ty2@(CoercionTy Coercion
co2)
= do { kco <- UnifyEnv -> TcType -> TcType -> TcM Coercion
uType (UnifyEnv -> TcType -> TcType -> UnifyEnv
mkKindEnv UnifyEnv
env TcType
ty1 TcType
ty2)
(Coercion -> TcType
coercionType Coercion
co1) (Coercion -> TcType
coercionType Coercion
co2)
; return $ mkProofIrrelCo role kco co1 co2 }
go TcType
ty1 TcType
ty2 = TcType -> TcType -> TcM Coercion
defer TcType
ty1 TcType
ty2
defer :: TcType -> TcType -> TcM Coercion
defer TcType
ty1 TcType
ty2
| TcType
ty1 HasDebugCallStack => TcType -> TcType -> Bool
TcType -> TcType -> Bool
`tcEqType` TcType
ty2 = Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> TcType -> Coercion
mkReflCo Role
role TcType
ty1)
| Bool
otherwise = UnifyEnv -> TcType -> TcType -> TcM Coercion
uType_defer UnifyEnv
env TcType
orig_ty1 TcType
orig_ty2
u_tc_arg :: Bool -> Role -> TcType -> TcType -> TcM Coercion
u_tc_arg Bool
is_vis Role
role TcType
ty1 TcType
ty2
= do { String -> SDoc -> TcM ()
traceTc String
"u_tc_arg" (Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
role SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2)
; UnifyEnv -> TcType -> TcType -> TcM Coercion
uType UnifyEnv
env_arg TcType
ty1 TcType
ty2 }
where
env_arg :: UnifyEnv
env_arg = UnifyEnv
env { u_loc = adjustCtLoc is_vis False (u_loc env)
, u_role = role }
go_app :: Bool
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcType
-> TcM Coercion
go_app Bool
vis TcType
ty1 TcType
s1 TcType
t1 TcType
ty2 TcType
s2 TcType
t2
| Role
Nominal <- Role
role
=
do { let env_arg :: UnifyEnv
env_arg = UnifyEnv
env { u_loc = adjustCtLoc vis False (u_loc env) }
; co_t <- UnifyEnv -> TcType -> TcType -> TcM Coercion
uType UnifyEnv
env_arg TcType
t1 TcType
t2
; co_s <- uType env s1 s2
; return $ mkAppCo co_s co_t }
| Bool
otherwise
= TcType -> TcType -> TcM Coercion
defer TcType
ty1 TcType
ty2
uUnfilledVar, uUnfilledVar1
:: UnifyEnv
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM CoercionN
uUnfilledVar :: UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar UnifyEnv
env SwapFlag
swapped TcTyVar
tv1 TcType
ty2
| Role
Nominal <- UnifyEnv -> Role
u_role UnifyEnv
env
= do { ty2 <- ZonkM TcType -> TcM TcType
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TcType -> TcM TcType) -> ZonkM TcType -> TcM TcType
forall a b. (a -> b) -> a -> b
$ TcType -> ZonkM TcType
zonkTcType TcType
ty2
; uUnfilledVar1 env swapped tv1 ty2 }
| Bool
otherwise
= SwapFlag
-> (TcType -> TcType -> TcM Coercion)
-> TcType
-> TcType
-> TcM Coercion
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped (UnifyEnv -> TcType -> TcType -> TcM Coercion
uType_defer UnifyEnv
env) (TcTyVar -> TcType
mkTyVarTy TcTyVar
tv1) TcType
ty2
uUnfilledVar1 :: UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar1 UnifyEnv
env
SwapFlag
swapped
TcTyVar
tv1
TcType
ty2
| Just TcTyVar
tv2 <- TcType -> Maybe TcTyVar
getTyVar_maybe TcType
ty2
= TcTyVar -> TcM Coercion
go TcTyVar
tv2
| Bool
otherwise
= UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar2 UnifyEnv
env SwapFlag
swapped TcTyVar
tv1 TcType
ty2
where
go :: TcTyVar -> TcM Coercion
go TcTyVar
tv2 | TcTyVar
tv1 TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv2
= Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Coercion
mkNomReflCo (TcTyVar -> TcType
mkTyVarTy TcTyVar
tv1))
| Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars Bool
False TcTyVar
tv1 TcTyVar
tv2
= do { tv1 <- ZonkM TcTyVar -> TcM TcTyVar
forall a. ZonkM a -> TcM a
liftZonkM (ZonkM TcTyVar -> TcM TcTyVar) -> ZonkM TcTyVar -> TcM TcTyVar
forall a b. (a -> b) -> a -> b
$ TcTyVar -> ZonkM TcTyVar
zonkTyCoVarKind TcTyVar
tv1
; uUnfilledVar2 env (flipSwap swapped) tv2 (mkTyVarTy tv1) }
| Bool
otherwise
= UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar2 UnifyEnv
env SwapFlag
swapped TcTyVar
tv1 TcType
ty2
uUnfilledVar2 :: UnifyEnv
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM CoercionN
uUnfilledVar2 :: UnifyEnv -> SwapFlag -> TcTyVar -> TcType -> TcM Coercion
uUnfilledVar2 env :: UnifyEnv
env@(UE { u_defer :: UnifyEnv -> TcRef (Bag Ct)
u_defer = TcRef (Bag Ct)
def_eq_ref }) SwapFlag
swapped TcTyVar
tv1 TcType
ty2
= do { cur_lvl <- TcM TcLevel
getTcLevel
; if not (touchabilityAndShapeTest cur_lvl tv1 ty2
&& simpleUnifyCheck UC_OnTheFly tv1 ty2)
then not_ok_so_defer cur_lvl
else
do { def_eqs <- readTcRef def_eq_ref
; co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
, ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
, ppr (isReflCo co_k), ppr co_k ]
; if isReflCo co_k
then do { liftZonkM $ writeMetaTyVar tv1 ty2
; case u_unified env of
Maybe (TcRef [TcTyVar])
Nothing -> () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just TcRef [TcTyVar]
uref -> TcRef [TcTyVar] -> ([TcTyVar] -> [TcTyVar]) -> TcM ()
forall (m :: * -> *) a. MonadIO m => TcRef a -> (a -> a) -> m ()
updTcRef TcRef [TcTyVar]
uref (TcTyVar
tv1 TcTyVar -> [TcTyVar] -> [TcTyVar]
forall a. a -> [a] -> [a]
:)
; return (mkNomReflCo ty2) }
else
do { writeTcRef def_eq_ref def_eqs
; defer }
}}
where
ty1 :: TcType
ty1 = TcTyVar -> TcType
mkTyVarTy TcTyVar
tv1
defer :: TcM Coercion
defer = SwapFlag
-> (TcType -> TcType -> TcM Coercion)
-> TcType
-> TcType
-> TcM Coercion
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped (UnifyEnv -> TcType -> TcType -> TcM Coercion
uType_defer UnifyEnv
env) TcType
ty1 TcType
ty2
not_ok_so_defer :: TcLevel -> TcM Coercion
not_ok_so_defer TcLevel
cur_lvl =
do { String -> SDoc -> TcM ()
traceTc String
"uUnfilledVar2 not ok" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tv1:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty2:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcType
ty2
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"simple-unify-chk:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (UnifyCheckCaller -> TcTyVar -> TcType -> Bool
simpleUnifyCheck UnifyCheckCaller
UC_OnTheFly TcTyVar
tv1 TcType
ty2)
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"touchability:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcLevel -> TcTyVar -> TcType -> Bool
touchabilityAndShapeTest TcLevel
cur_lvl TcTyVar
tv1 TcType
ty2)]
; TcM Coercion
defer }
swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars Bool
is_given TcTyVar
tv1 TcTyVar
tv2
| Bool -> Bool
not Bool
is_given, Int
pri1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0, Int
pri2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Bool
True
| Bool -> Bool
not Bool
is_given, Int
pri2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0, Int
pri1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Bool
False
| TcLevel
lvl1 TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl2 = Bool
False
| TcLevel
lvl2 TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl1 = Bool
True
| Int
pri1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pri2 = Bool
False
| Int
pri2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pri1 = Bool
True
| Name -> Bool
isSystemName Name
tv2_name, Bool -> Bool
not (Name -> Bool
isSystemName Name
tv1_name) = Bool
True
| Bool
otherwise = Bool
False
where
lvl1 :: TcLevel
lvl1 = TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv1
lvl2 :: TcLevel
lvl2 = TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv2
pri1 :: Int
pri1 = TcTyVar -> Int
lhsPriority TcTyVar
tv1
pri2 :: Int
pri2 = TcTyVar -> Int
lhsPriority TcTyVar
tv2
tv1_name :: Name
tv1_name = TcTyVar -> Name
Var.varName TcTyVar
tv1
tv2_name :: Name
tv2_name = TcTyVar -> Name
Var.varName TcTyVar
tv2
lhsPriority :: TcTyVar -> Int
lhsPriority :: TcTyVar -> Int
lhsPriority TcTyVar
tv
= Bool -> SDoc -> Int -> Int
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcTyVar -> Bool
isTyVar TcTyVar
tv) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
TcTyVarDetails
RuntimeUnk -> Int
0
SkolemTv {} -> Int
0
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
lvl }
| TcLevel
QLInstVar <- TcLevel
lvl
-> Int
5
| Bool
otherwise
-> case MetaInfo
info of
MetaInfo
CycleBreakerTv -> Int
0
MetaInfo
TyVarTv -> Int
1
ConcreteTv {} -> Int
2
MetaInfo
TauTv -> Int
3
MetaInfo
RuntimeUnkTv -> Int
4
matchExpectedFunKind
:: TypedThing
-> Arity
-> TcKind
-> TcM Coercion
matchExpectedFunKind :: TypedThing -> Int -> TcType -> TcM Coercion
matchExpectedFunKind TypedThing
hs_ty Int
n TcType
k = Int -> TcType -> TcM Coercion
go Int
n TcType
k
where
go :: Int -> TcType -> TcM Coercion
go Int
0 TcType
k = Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcType -> Coercion
mkNomReflCo TcType
k)
go Int
n TcType
k | Just TcType
k' <- TcType -> Maybe TcType
coreView TcType
k = Int -> TcType -> TcM Coercion
go Int
n TcType
k'
go Int
n k :: TcType
k@(TyVarTy TcTyVar
kvar)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
kvar
= do { maybe_kind <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) MetaDetails
forall (m :: * -> *). MonadIO m => TcTyVar -> m MetaDetails
readMetaTyVar TcTyVar
kvar
; case maybe_kind of
Indirect TcType
fun_kind -> Int -> TcType -> TcM Coercion
go Int
n TcType
fun_kind
MetaDetails
Flexi -> Int -> TcType -> TcM Coercion
defer Int
n TcType
k }
go Int
n (FunTy { ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: TcType -> TcType
ft_mult = TcType
w, ft_arg :: TcType -> TcType
ft_arg = TcType
arg, ft_res :: TcType -> TcType
ft_res = TcType
res })
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af
= do { co <- Int -> TcType -> TcM Coercion
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) TcType
res
; return (mkNakedFunCo Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) }
go Int
n TcType
other
= Int -> TcType -> TcM Coercion
defer Int
n TcType
other
defer :: Int -> TcType -> TcM Coercion
defer Int
n TcType
k
= do { arg_kinds <- Int -> TcM [TcType]
newMetaKindVars Int
n
; res_kind <- newMetaKindVar
; let new_fun = [TcType] -> TcType -> TcType
mkVisFunTysMany [TcType]
arg_kinds TcType
res_kind
origin = TypeEqOrigin { uo_actual :: TcType
uo_actual = TcType
k
, uo_expected :: TcType
uo_expected = TcType
new_fun
, uo_thing :: Maybe TypedThing
uo_thing = TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just TypedThing
hs_ty
, uo_visible :: Bool
uo_visible = Bool
True
}
; unifyTypeAndEmit KindLevel origin k new_fun }
data UnifyCheckCaller
= UC_OnTheFly
| UC_QuickLook
| UC_Solver
| UC_Defaulting
simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
simpleUnifyCheck :: UnifyCheckCaller -> TcTyVar -> TcType -> Bool
simpleUnifyCheck UnifyCheckCaller
caller TcTyVar
lhs_tv TcType
rhs
= TcType -> Bool
go TcType
rhs
where
!(TcType -> Bool
occ_in_ty, Coercion -> Bool
occ_in_co) = TcTyVar -> (TcType -> Bool, Coercion -> Bool)
mkOccFolders TcTyVar
lhs_tv
lhs_tv_lvl :: TcLevel
lhs_tv_lvl = TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
lhs_tv
lhs_tv_is_concrete :: Bool
lhs_tv_is_concrete = TcTyVar -> Bool
isConcreteTyVar TcTyVar
lhs_tv
forall_ok :: Bool
forall_ok = case UnifyCheckCaller
caller of
UnifyCheckCaller
UC_QuickLook -> TcTyVar -> Bool
isQLInstTyVar TcTyVar
lhs_tv
UnifyCheckCaller
_ -> TcTyVar -> Bool
isRuntimeUnkTyVar TcTyVar
lhs_tv
fam_ok :: Bool
fam_ok = case UnifyCheckCaller
caller of
UnifyCheckCaller
UC_Solver -> Bool
True
UnifyCheckCaller
UC_QuickLook -> Bool
True
UnifyCheckCaller
UC_OnTheFly -> Bool
False
UnifyCheckCaller
UC_Defaulting -> Bool
True
go :: TcType -> Bool
go (TyVarTy TcTyVar
tv)
| TcTyVar
lhs_tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv = Bool
False
| TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lhs_tv_lvl = Bool
False
| Bool
lhs_tv_is_concrete, Bool -> Bool
not (TcTyVar -> Bool
isConcreteTyVar TcTyVar
tv) = Bool
False
| TcType -> Bool
occ_in_ty (TcType -> Bool) -> TcType -> Bool
forall a b. (a -> b) -> a -> b
$! (TcTyVar -> TcType
tyVarKind TcTyVar
tv) = Bool
False
| Bool
otherwise = Bool
True
go (FunTy {ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: TcType -> TcType
ft_mult = TcType
w, ft_arg :: TcType -> TcType
ft_arg = TcType
a, ft_res :: TcType -> TcType
ft_res = TcType
r})
| Bool -> Bool
not Bool
forall_ok, FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af = Bool
False
| Bool
otherwise = TcType -> Bool
go TcType
w Bool -> Bool -> Bool
&& TcType -> Bool
go TcType
a Bool -> Bool -> Bool
&& TcType -> Bool
go TcType
r
go (TyConApp TyCon
tc [TcType]
tys)
| Bool
lhs_tv_is_concrete, Bool -> Bool
not (TyCon -> Bool
isConcreteTyCon TyCon
tc) = Bool
False
| Bool -> Bool
not Bool
forall_ok, Bool -> Bool
not (TyCon -> Bool
isTauTyCon TyCon
tc) = Bool
False
| Bool -> Bool
not Bool
fam_ok, Bool -> Bool
not (TyCon -> Bool
isFamFreeTyCon TyCon
tc) = Bool
False
| Bool
otherwise = (TcType -> Bool) -> [TcType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all TcType -> Bool
go [TcType]
tys
go (ForAllTy (Bndr TcTyVar
tv ForAllTyFlag
_) TcType
ty)
| Bool
forall_ok = TcType -> Bool
go (TcTyVar -> TcType
tyVarKind TcTyVar
tv) Bool -> Bool -> Bool
&& (TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
lhs_tv Bool -> Bool -> Bool
|| TcType -> Bool
go TcType
ty)
| Bool
otherwise = Bool
False
go (AppTy TcType
t1 TcType
t2) = TcType -> Bool
go TcType
t1 Bool -> Bool -> Bool
&& TcType -> Bool
go TcType
t2
go (CastTy TcType
ty Coercion
co) = Bool -> Bool
not (Coercion -> Bool
occ_in_co Coercion
co) Bool -> Bool -> Bool
&& TcType -> Bool
go TcType
ty
go (CoercionTy Coercion
co) = Bool -> Bool
not (Coercion -> Bool
occ_in_co Coercion
co)
go (LitTy {}) = Bool
True
mkOccFolders :: TcTyVar -> (TcType -> Bool, TcCoercion -> Bool)
mkOccFolders :: TcTyVar -> (TcType -> Bool, Coercion -> Bool)
mkOccFolders TcTyVar
lhs_tv = (Any -> Bool
getAny (Any -> Bool) -> (TcType -> Any) -> TcType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcType -> Any
check_ty, Any -> Bool
getAny (Any -> Bool) -> (Coercion -> Any) -> Coercion -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Any
check_co)
where
!(TcType -> Any
check_ty, [TcType] -> Any
_, Coercion -> Any
check_co, [Coercion] -> Any
_) = TyCoFolder VarSet Any
-> VarSet
-> (TcType -> Any, [TcType] -> Any, Coercion -> Any,
[Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env
-> (TcType -> a, [TcType] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder VarSet Any
occ_folder VarSet
emptyVarSet
occ_folder :: TyCoFolder VarSet Any
occ_folder = TyCoFolder { tcf_view :: TcType -> Maybe TcType
tcf_view = TcType -> Maybe TcType
noView
, tcf_tyvar :: VarSet -> TcTyVar -> Any
tcf_tyvar = VarSet -> TcTyVar -> Any
do_tcv, tcf_covar :: VarSet -> TcTyVar -> Any
tcf_covar = VarSet -> TcTyVar -> Any
do_tcv
, tcf_hole :: VarSet -> CoercionHole -> Any
tcf_hole = VarSet -> CoercionHole -> Any
forall {p} {p}. p -> p -> Any
do_hole
, tcf_tycobinder :: VarSet -> TcTyVar -> ForAllTyFlag -> VarSet
tcf_tycobinder = VarSet -> TcTyVar -> ForAllTyFlag -> VarSet
forall {p}. VarSet -> TcTyVar -> p -> VarSet
do_bndr }
do_tcv :: VarSet -> TcTyVar -> Any
do_tcv VarSet
is TcTyVar
v = Bool -> Any
Any (Bool -> Bool
not (TcTyVar
v TcTyVar -> VarSet -> Bool
`elemVarSet` VarSet
is) Bool -> Bool -> Bool
&& TcTyVar
v TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
lhs_tv)
Any -> Any -> Any
forall a. Monoid a => a -> a -> a
`mappend` TcType -> Any
check_ty (TcTyVar -> TcType
varType TcTyVar
v)
do_bndr :: VarSet -> TcTyVar -> p -> VarSet
do_bndr VarSet
is TcTyVar
tcv p
_faf = VarSet -> TcTyVar -> VarSet
extendVarSet VarSet
is TcTyVar
tcv
do_hole :: p -> p -> Any
do_hole p
_is p
_hole = Bool -> Any
DM.Any Bool
True
data PuResult a b = PuFail CheckTyEqResult
| PuOK (Bag a) b
instance Functor (PuResult a) where
fmap :: forall a b. (a -> b) -> PuResult a a -> PuResult a b
fmap a -> b
_ (PuFail CheckTyEqResult
prob) = CheckTyEqResult -> PuResult a b
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
prob
fmap a -> b
f (PuOK Bag a
cts a
x) = Bag a -> b -> PuResult a b
forall a b. Bag a -> b -> PuResult a b
PuOK Bag a
cts (a -> b
f a
x)
instance Applicative (PuResult a) where
pure :: forall a. a -> PuResult a a
pure a
x = Bag a -> a -> PuResult a a
forall a b. Bag a -> b -> PuResult a b
PuOK Bag a
forall a. Bag a
emptyBag a
x
PuFail CheckTyEqResult
p1 <*> :: forall a b. PuResult a (a -> b) -> PuResult a a -> PuResult a b
<*> PuFail CheckTyEqResult
p2 = CheckTyEqResult -> PuResult a b
forall a b. CheckTyEqResult -> PuResult a b
PuFail (CheckTyEqResult
p1 CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> CheckTyEqResult
p2)
PuFail CheckTyEqResult
p1 <*> PuOK {} = CheckTyEqResult -> PuResult a b
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
p1
PuOK {} <*> PuFail CheckTyEqResult
p2 = CheckTyEqResult -> PuResult a b
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
p2
PuOK Bag a
c1 a -> b
f <*> PuOK Bag a
c2 a
x = Bag a -> b -> PuResult a b
forall a b. Bag a -> b -> PuResult a b
PuOK (Bag a
c1 Bag a -> Bag a -> Bag a
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag a
c2) (a -> b
f a
x)
instance (Outputable a, Outputable b) => Outputable (PuResult a b) where
ppr :: PuResult a b -> SDoc
ppr (PuFail CheckTyEqResult
prob) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"PuFail" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (CheckTyEqResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr CheckTyEqResult
prob)
ppr (PuOK Bag a
cts b
x) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"PuOK" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces
([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"redn:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> b -> SDoc
forall a. Outputable a => a -> SDoc
ppr b
x
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"cts:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bag a -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag a
cts ])
pprPur :: PuResult a b -> SDoc
pprPur :: forall a b. PuResult a b -> SDoc
pprPur (PuFail CheckTyEqResult
prob) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"PuFail:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> CheckTyEqResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr CheckTyEqResult
prob
pprPur (PuOK {}) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"PuOK"
okCheckRefl :: TcType -> TcM (PuResult a Reduction)
okCheckRefl :: forall a. TcType -> TcM (PuResult a Reduction)
okCheckRefl TcType
ty = PuResult a Reduction
-> IOEnv (Env TcGblEnv TcLclEnv) (PuResult a Reduction)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag a -> Reduction -> PuResult a Reduction
forall a b. Bag a -> b -> PuResult a b
PuOK Bag a
forall a. Bag a
emptyBag (Role -> TcType -> Reduction
mkReflRedn Role
Nominal TcType
ty))
failCheckWith :: CheckTyEqResult -> TcM (PuResult a b)
failCheckWith :: forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith CheckTyEqResult
p = PuResult a b -> IOEnv (Env TcGblEnv TcLclEnv) (PuResult a b)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqResult -> PuResult a b
forall a b. CheckTyEqResult -> PuResult a b
PuFail CheckTyEqResult
p)
mapCheck :: (x -> TcM (PuResult a Reduction))
-> [x]
-> TcM (PuResult a Reductions)
mapCheck :: forall x a.
(x -> TcM (PuResult a Reduction))
-> [x] -> TcM (PuResult a Reductions)
mapCheck x -> TcM (PuResult a Reduction)
f [x]
xs
= do { (ress :: [PuResult a Reduction]) <- (x -> TcM (PuResult a Reduction))
-> [x] -> IOEnv (Env TcGblEnv TcLclEnv) [PuResult a Reduction]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM x -> TcM (PuResult a Reduction)
f [x]
xs
; return (unzipRedns <$> sequenceA ress) }
data TyEqFlags a
= TEF { forall a. TyEqFlags a -> Bool
tef_foralls :: Bool
, forall a. TyEqFlags a -> CanEqLHS
tef_lhs :: CanEqLHS
, forall a. TyEqFlags a -> AreUnifying
tef_unifying :: AreUnifying
, forall a. TyEqFlags a -> TyEqFamApp a
tef_fam_app :: TyEqFamApp a
, forall a. TyEqFlags a -> CheckTyEqProblem
tef_occurs :: CheckTyEqProblem }
data TyEqFamApp a
= TEFA_Fail
| TEFA_Recurse
| TEFA_Break (FamAppBreaker a)
data AreUnifying
= Unifying
MetaInfo
TcLevel
LevelCheck
| NotUnifying
data LevelCheck
= LC_None
| LC_Check
| LC_Promote
Bool
instance Outputable (TyEqFlags a) where
ppr :: TyEqFlags a -> SDoc
ppr (TEF { Bool
CheckTyEqProblem
CanEqLHS
AreUnifying
TyEqFamApp a
tef_foralls :: forall a. TyEqFlags a -> Bool
tef_lhs :: forall a. TyEqFlags a -> CanEqLHS
tef_unifying :: forall a. TyEqFlags a -> AreUnifying
tef_fam_app :: forall a. TyEqFlags a -> TyEqFamApp a
tef_occurs :: forall a. TyEqFlags a -> CheckTyEqProblem
tef_foralls :: Bool
tef_lhs :: CanEqLHS
tef_unifying :: AreUnifying
tef_fam_app :: TyEqFamApp a
tef_occurs :: CheckTyEqProblem
.. }) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TEF" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tef_foralls =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
tef_foralls
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tef_lhs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CanEqLHS -> SDoc
forall a. Outputable a => a -> SDoc
ppr CanEqLHS
tef_lhs
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tef_unifying =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> AreUnifying -> SDoc
forall a. Outputable a => a -> SDoc
ppr AreUnifying
tef_unifying
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tef_fam_app =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TyEqFamApp a -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyEqFamApp a
tef_fam_app
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tef_occurs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CheckTyEqProblem -> SDoc
forall a. Outputable a => a -> SDoc
ppr CheckTyEqProblem
tef_occurs ])
instance Outputable (TyEqFamApp a) where
ppr :: TyEqFamApp a -> SDoc
ppr TyEqFamApp a
TEFA_Fail = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TEFA_Fail"
ppr TyEqFamApp a
TEFA_Recurse = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TEFA_Recurse"
ppr (TEFA_Break {}) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"TEFA_Break"
instance Outputable AreUnifying where
ppr :: AreUnifying -> SDoc
ppr AreUnifying
NotUnifying = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NotUnifying"
ppr (Unifying MetaInfo
mi TcLevel
lvl LevelCheck
lc) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Unifying" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+>
SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces (MetaInfo -> SDoc
forall a. Outputable a => a -> SDoc
ppr MetaInfo
mi SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
lvl SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> LevelCheck -> SDoc
forall a. Outputable a => a -> SDoc
ppr LevelCheck
lc)
instance Outputable LevelCheck where
ppr :: LevelCheck -> SDoc
ppr LevelCheck
LC_None = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LC_None"
ppr LevelCheck
LC_Check = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LC_Check"
ppr (LC_Promote Bool
b) = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"LC_Promote" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppWhen Bool
b (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"(deep)")
famAppArgFlags :: TyEqFlags a -> TyEqFlags a
famAppArgFlags :: forall a. TyEqFlags a -> TyEqFlags a
famAppArgFlags flags :: TyEqFlags a
flags@(TEF { tef_unifying :: forall a. TyEqFlags a -> AreUnifying
tef_unifying = AreUnifying
unifying })
= TyEqFlags a
flags { tef_fam_app = TEFA_Recurse
, tef_unifying = zap_promotion unifying
, tef_occurs = cteSolubleOccurs }
where
zap_promotion :: AreUnifying -> AreUnifying
zap_promotion (Unifying MetaInfo
info TcLevel
lvl (LC_Promote Bool
deeply))
| Bool -> Bool
not Bool
deeply = MetaInfo -> TcLevel -> LevelCheck -> AreUnifying
Unifying MetaInfo
info TcLevel
lvl LevelCheck
LC_Check
zap_promotion AreUnifying
unifying = AreUnifying
unifying
type FamAppBreaker a = TcType -> TcM (PuResult a Reduction)
checkTyEqRhs :: forall a. TyEqFlags a
-> TcType
-> TcM (PuResult a Reduction)
checkTyEqRhs :: forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
flags TcType
ty
= case TcType
ty of
LitTy {} -> TcType -> TcM (PuResult a Reduction)
forall a. TcType -> TcM (PuResult a Reduction)
okCheckRefl TcType
ty
TyConApp TyCon
tc [TcType]
tys -> TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
forall a.
TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
checkTyConApp TyEqFlags a
flags TcType
ty TyCon
tc [TcType]
tys
TyVarTy TcTyVar
tv -> TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
checkTyVar TyEqFlags a
flags TcTyVar
tv
FunTy {ft_af :: TcType -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: TcType -> TcType
ft_mult = TcType
w, ft_arg :: TcType -> TcType
ft_arg = TcType
a, ft_res :: TcType -> TcType
ft_res = TcType
r}
| FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af
, Bool -> Bool
not (TyEqFlags a -> Bool
forall a. TyEqFlags a -> Bool
tef_foralls TyEqFlags a
flags)
-> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith CheckTyEqResult
impredicativeProblem
| Bool
otherwise
-> do { w_res <- TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
flags TcType
w
; a_res <- checkTyEqRhs flags a
; r_res <- checkTyEqRhs flags r
; return (mkFunRedn Nominal af <$> w_res <*> a_res <*> r_res) }
AppTy TcType
fun TcType
arg -> do { fun_res <- TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
flags TcType
fun
; arg_res <- checkTyEqRhs flags arg
; return (mkAppRedn <$> fun_res <*> arg_res) }
CastTy TcType
ty Coercion
co -> do { ty_res <- TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
flags TcType
ty
; co_res <- checkCo flags co
; return (mkCastRedn1 Nominal ty <$> co_res <*> ty_res) }
CoercionTy Coercion
co -> do { co_res <- TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
forall a. TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
checkCo TyEqFlags a
flags Coercion
co
; return (mkReflCoRedn Nominal <$> co_res) }
ForAllTy {}
| TyEqFlags a -> Bool
forall a. TyEqFlags a -> Bool
tef_foralls TyEqFlags a
flags -> TcType -> TcM (PuResult a Reduction)
forall a. TcType -> TcM (PuResult a Reduction)
okCheckRefl TcType
ty
| Bool
otherwise -> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith CheckTyEqResult
impredicativeProblem
checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
checkCo :: forall a. TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
checkCo (TEF { tef_lhs :: forall a. TyEqFlags a -> CanEqLHS
tef_lhs = TyFamLHS {} }) Coercion
co
= PuResult a Coercion
-> IOEnv (Env TcGblEnv TcLclEnv) (PuResult a Coercion)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> PuResult a Coercion
forall a. a -> PuResult a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
co)
checkCo (TEF { tef_lhs :: forall a. TyEqFlags a -> CanEqLHS
tef_lhs = TyVarLHS TcTyVar
lhs_tv
, tef_unifying :: forall a. TyEqFlags a -> AreUnifying
tef_unifying = AreUnifying
unifying
, tef_occurs :: forall a. TyEqFlags a -> CheckTyEqProblem
tef_occurs = CheckTyEqProblem
occ_prob }) Coercion
co
| Coercion -> Bool
hasCoercionHoleCo Coercion
co
= CheckTyEqResult
-> IOEnv (Env TcGblEnv TcLclEnv) (PuResult a Coercion)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteCoercionHole)
| Unifying MetaInfo
_ TcLevel
lhs_tv_lvl (LC_Promote {}) <- AreUnifying
unifying
= do { reason <- CheckTyEqProblem
-> TcTyVar -> TcLevel -> VarSet -> TcM CheckTyEqResult
checkPromoteFreeVars CheckTyEqProblem
occ_prob TcTyVar
lhs_tv TcLevel
lhs_tv_lvl (Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
; if cterHasNoProblem reason
then return (pure co)
else failCheckWith reason }
| TcTyVar
lhs_tv TcTyVar -> VarSet -> Bool
`elemVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
co
= CheckTyEqResult
-> IOEnv (Env TcGblEnv TcLclEnv) (PuResult a Coercion)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
occ_prob)
| Bool
otherwise
= PuResult a Coercion
-> IOEnv (Env TcGblEnv TcLclEnv) (PuResult a Coercion)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> PuResult a Coercion
forall a. a -> PuResult a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
co)
checkTyConApp :: TyEqFlags a
-> TcType -> TyCon -> [TcType]
-> TcM (PuResult a Reduction)
checkTyConApp :: forall a.
TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
checkTyConApp flags :: TyEqFlags a
flags@(TEF { tef_unifying :: forall a. TyEqFlags a -> AreUnifying
tef_unifying = AreUnifying
unifying, tef_foralls :: forall a. TyEqFlags a -> Bool
tef_foralls = Bool
foralls_ok })
TcType
tc_app TyCon
tc [TcType]
tys
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
, let arity :: Int
arity = TyCon -> Int
tyConArity TyCon
tc
= if [TcType]
tys [TcType] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Int
arity
then TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
forall a.
TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
checkFamApp TyEqFlags a
flags TcType
tc_app TyCon
tc [TcType]
tys
else do { let ([TcType]
fun_args, [TcType]
extra_args) = Int -> [TcType] -> ([TcType], [TcType])
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) [TcType]
tys
fun_app :: TcType
fun_app = TyCon -> [TcType] -> TcType
mkTyConApp TyCon
tc [TcType]
fun_args
; fun_res <- TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
forall a.
TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
checkFamApp TyEqFlags a
flags TcType
fun_app TyCon
tc [TcType]
fun_args
; extra_res <- mapCheck (checkTyEqRhs flags) extra_args
; traceTc "Over-sat" (ppr tc <+> ppr tys $$ ppr arity $$ pprPur fun_res $$ pprPur extra_res)
; return (mkAppRedns <$> fun_res <*> extra_res) }
| Just TcType
ty' <- TcType -> Maybe TcType
rewriterView TcType
tc_app
= TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
flags TcType
ty'
| Bool -> Bool
not (TyCon -> Bool
isTauTyCon TyCon
tc Bool -> Bool -> Bool
|| Bool
foralls_ok)
= CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith CheckTyEqResult
impredicativeProblem
| Unifying MetaInfo
info TcLevel
_ LevelCheck
_ <- AreUnifying
unifying
, MetaInfo -> Bool
isConcreteInfo MetaInfo
info
, Bool -> Bool
not (TyCon -> Bool
isConcreteTyCon TyCon
tc)
= CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteConcrete)
| Bool
otherwise
= TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
forall a.
TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
recurseIntoTyConApp TyEqFlags a
flags TyCon
tc [TcType]
tys
recurseIntoTyConApp :: TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
recurseIntoTyConApp :: forall a.
TyEqFlags a -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
recurseIntoTyConApp TyEqFlags a
flags TyCon
tc [TcType]
tys
= do { tys_res <- (TcType -> TcM (PuResult a Reduction))
-> [TcType] -> TcM (PuResult a Reductions)
forall x a.
(x -> TcM (PuResult a Reduction))
-> [x] -> TcM (PuResult a Reductions)
mapCheck (TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
flags) [TcType]
tys
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
checkFamApp :: TyEqFlags a
-> TcType -> TyCon -> [TcType]
-> TcM (PuResult a Reduction)
checkFamApp :: forall a.
TyEqFlags a
-> TcType -> TyCon -> [TcType] -> TcM (PuResult a Reduction)
checkFamApp flags :: TyEqFlags a
flags@(TEF { tef_unifying :: forall a. TyEqFlags a -> AreUnifying
tef_unifying = AreUnifying
unifying, tef_occurs :: forall a. TyEqFlags a -> CheckTyEqProblem
tef_occurs = CheckTyEqProblem
occ_prob
, tef_fam_app :: forall a. TyEqFlags a -> TyEqFamApp a
tef_fam_app = TyEqFamApp a
fam_app_flag, tef_lhs :: forall a. TyEqFlags a -> CanEqLHS
tef_lhs = CanEqLHS
lhs })
TcType
fam_app TyCon
tc [TcType]
tys
= case TyEqFamApp a
fam_app_flag of
TyEqFamApp a
TEFA_Fail -> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteTypeFamily)
TyEqFamApp a
_ | TyFamLHS TyCon
lhs_tc [TcType]
lhs_tys <- CanEqLHS
lhs
, TyCon -> [TcType] -> TyCon -> [TcType] -> Bool
tcEqTyConApps TyCon
lhs_tc [TcType]
lhs_tys TyCon
tc [TcType]
tys
-> case TyEqFamApp a
fam_app_flag of
TyEqFamApp a
TEFA_Recurse -> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
occ_prob)
TEFA_Break FamAppBreaker a
breaker -> FamAppBreaker a
breaker TcType
fam_app
TyEqFamApp a
_ | Unifying MetaInfo
lhs_info TcLevel
_ LevelCheck
_ <- AreUnifying
unifying
, MetaInfo -> Bool
isConcreteInfo MetaInfo
lhs_info
-> case TyEqFamApp a
fam_app_flag of
TyEqFamApp a
TEFA_Recurse -> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteConcrete)
TEFA_Break FamAppBreaker a
breaker -> FamAppBreaker a
breaker TcType
fam_app
TyEqFamApp a
TEFA_Recurse
-> do { tys_res <- FamAppBreaker a -> [TcType] -> TcM (PuResult a Reductions)
forall x a.
(x -> TcM (PuResult a Reduction))
-> [x] -> TcM (PuResult a Reductions)
mapCheck (TyEqFlags a -> FamAppBreaker a
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
arg_flags) [TcType]
tys
; traceTc "under" (ppr tc $$ pprPur tys_res $$ ppr flags)
; return (mkTyConAppRedn Nominal tc <$> tys_res) }
TEFA_Break FamAppBreaker a
breaker
-> do { tys_res <- FamAppBreaker a -> [TcType] -> TcM (PuResult a Reductions)
forall x a.
(x -> TcM (PuResult a Reduction))
-> [x] -> TcM (PuResult a Reductions)
mapCheck (TyEqFlags a -> FamAppBreaker a
forall a. TyEqFlags a -> TcType -> TcM (PuResult a Reduction)
checkTyEqRhs TyEqFlags a
arg_flags) [TcType]
tys
; case tys_res of
PuOK Bag a
cts Reductions
redns -> PuResult a Reduction -> TcM (PuResult a Reduction)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag a -> Reduction -> PuResult a Reduction
forall a b. Bag a -> b -> PuResult a b
PuOK Bag a
cts (Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
Nominal TyCon
tc Reductions
redns))
PuFail {} -> FamAppBreaker a
breaker TcType
fam_app }
where
arg_flags :: TyEqFlags a
arg_flags = TyEqFlags a -> TyEqFlags a
forall a. TyEqFlags a -> TyEqFlags a
famAppArgFlags TyEqFlags a
flags
checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
checkTyVar :: forall a. TyEqFlags a -> TcTyVar -> TcM (PuResult a Reduction)
checkTyVar (TEF { tef_lhs :: forall a. TyEqFlags a -> CanEqLHS
tef_lhs = CanEqLHS
lhs, tef_unifying :: forall a. TyEqFlags a -> AreUnifying
tef_unifying = AreUnifying
unifying, tef_occurs :: forall a. TyEqFlags a -> CheckTyEqProblem
tef_occurs = CheckTyEqProblem
occ_prob }) TcTyVar
occ_tv
= case CanEqLHS
lhs of
TyFamLHS {} -> TcM (PuResult a Reduction)
success
TyVarLHS TcTyVar
lhs_tv -> AreUnifying -> TcTyVar -> TcM (PuResult a Reduction)
check_tv AreUnifying
unifying TcTyVar
lhs_tv
where
lvl_occ :: TcLevel
lvl_occ = TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
occ_tv
success :: TcM (PuResult a Reduction)
success = TcType -> TcM (PuResult a Reduction)
forall a. TcType -> TcM (PuResult a Reduction)
okCheckRefl (TcTyVar -> TcType
mkTyVarTy TcTyVar
occ_tv)
check_tv :: AreUnifying -> TcTyVar -> TcM (PuResult a Reduction)
check_tv AreUnifying
NotUnifying TcTyVar
lhs_tv
= TcTyVar -> TcM (PuResult a Reduction)
simple_occurs_check TcTyVar
lhs_tv
check_tv (Unifying MetaInfo
info TcLevel
lvl LevelCheck
prom) TcTyVar
lhs_tv
= do { mb_done <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcType)
isFilledMetaTyVar_maybe TcTyVar
occ_tv
; case mb_done of
Just {} -> TcM (PuResult a Reduction)
success
Maybe TcType
Nothing -> MetaInfo
-> TcLevel -> LevelCheck -> TcTyVar -> TcM (PuResult a Reduction)
check_unif MetaInfo
info TcLevel
lvl LevelCheck
prom TcTyVar
lhs_tv }
check_unif :: MetaInfo -> TcLevel -> LevelCheck
-> TcTyVar -> TcM (PuResult a Reduction)
check_unif :: MetaInfo
-> TcLevel -> LevelCheck -> TcTyVar -> TcM (PuResult a Reduction)
check_unif MetaInfo
lhs_tv_info TcLevel
lhs_tv_lvl LevelCheck
prom TcTyVar
lhs_tv
| MetaInfo -> Bool
isConcreteInfo MetaInfo
lhs_tv_info
, Bool -> Bool
not (TcTyVar -> Bool
isConcreteTyVar TcTyVar
occ_tv)
= if TcTyVar -> Bool
can_make_concrete TcTyVar
occ_tv
then TcTyVar -> MetaInfo -> TcLevel -> TcM (PuResult a Reduction)
promote TcTyVar
lhs_tv MetaInfo
lhs_tv_info TcLevel
lhs_tv_lvl
else CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteConcrete)
| TcLevel
lvl_occ TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lhs_tv_lvl
= case LevelCheck
prom of
LevelCheck
LC_None -> String -> SDoc -> TcM (PuResult a Reduction)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"check_unif" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
lhs_tv SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
occ_tv)
LevelCheck
LC_Check -> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteSkolemEscape)
LC_Promote {}
| TcTyVar -> Bool
isSkolemTyVar TcTyVar
occ_tv -> CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteSkolemEscape)
| Bool
otherwise -> TcTyVar -> MetaInfo -> TcLevel -> TcM (PuResult a Reduction)
promote TcTyVar
lhs_tv MetaInfo
lhs_tv_info TcLevel
lhs_tv_lvl
| Bool
otherwise
= TcTyVar -> TcM (PuResult a Reduction)
simple_occurs_check TcTyVar
lhs_tv
simple_occurs_check :: TcTyVar -> TcM (PuResult a Reduction)
simple_occurs_check TcTyVar
lhs_tv
| TcTyVar
lhs_tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
occ_tv Bool -> Bool -> Bool
|| TcType -> Bool
check_kind (TcTyVar -> TcType
tyVarKind TcTyVar
occ_tv)
= CheckTyEqResult -> TcM (PuResult a Reduction)
forall a b. CheckTyEqResult -> TcM (PuResult a b)
failCheckWith (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
occ_prob)
| Bool
otherwise
= TcM (PuResult a Reduction)
success
where
(TcType -> Bool
check_kind, Coercion -> Bool
_) = TcTyVar -> (TcType -> Bool, Coercion -> Bool)
mkOccFolders TcTyVar
lhs_tv
can_make_concrete :: TcTyVar -> Bool
can_make_concrete TcTyVar
occ_tv = case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
occ_tv of
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } -> case MetaInfo
info of
ConcreteTv {} -> Bool
True
TauTv {} -> Bool
True
MetaInfo
_ -> Bool
False
TcTyVarDetails
_ -> Bool
False
promote :: TcTyVar -> MetaInfo -> TcLevel -> TcM (PuResult a Reduction)
promote TcTyVar
lhs_tv MetaInfo
lhs_tv_info TcLevel
lhs_tv_lvl
| MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info_occ, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
lvl_occ } <- TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
occ_tv
= do { let new_info :: MetaInfo
new_info | MetaInfo -> Bool
isConcreteInfo MetaInfo
lhs_tv_info = MetaInfo
lhs_tv_info
| Bool
otherwise = MetaInfo
info_occ
new_lvl :: TcLevel
new_lvl = TcLevel
lhs_tv_lvl TcLevel -> TcLevel -> TcLevel
`minTcLevel` TcLevel
lvl_occ
; reason <- CheckTyEqProblem
-> TcTyVar -> TcLevel -> VarSet -> TcM CheckTyEqResult
checkPromoteFreeVars CheckTyEqProblem
occ_prob TcTyVar
lhs_tv TcLevel
lhs_tv_lvl (TcType -> VarSet
tyCoVarsOfType (TcTyVar -> TcType
tyVarKind TcTyVar
occ_tv))
; if cterHasNoProblem reason
then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv
; okCheckRefl new_tv_ty }
else failCheckWith reason }
| Bool
otherwise = String -> SDoc -> TcM (PuResult a Reduction)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"promote" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
occ_tv)
checkPromoteFreeVars :: CheckTyEqProblem
-> TcTyVar -> TcLevel
-> TyCoVarSet -> TcM CheckTyEqResult
checkPromoteFreeVars :: CheckTyEqProblem
-> TcTyVar -> TcLevel -> VarSet -> TcM CheckTyEqResult
checkPromoteFreeVars CheckTyEqProblem
occ_prob TcTyVar
lhs_tv TcLevel
lhs_tv_lvl VarSet
vs
= do { oks <- (TcTyVar -> TcM CheckTyEqResult)
-> [TcTyVar] -> IOEnv (Env TcGblEnv TcLclEnv) [CheckTyEqResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TcTyVar -> TcM CheckTyEqResult
do_one (VarSet -> [TcTyVar]
forall elt. UniqSet elt -> [elt]
nonDetEltsUniqSet VarSet
vs)
; return (mconcat oks) }
where
do_one :: TyCoVar -> TcM CheckTyEqResult
do_one :: TcTyVar -> TcM CheckTyEqResult
do_one TcTyVar
v | TcTyVar -> Bool
isCoVar TcTyVar
v = CheckTyEqResult -> TcM CheckTyEqResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return CheckTyEqResult
cteOK
| TcTyVar
lhs_tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
v = CheckTyEqResult -> TcM CheckTyEqResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
occ_prob)
| Bool
no_promotion = CheckTyEqResult -> TcM CheckTyEqResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return CheckTyEqResult
cteOK
| Bool -> Bool
not (TcTyVar -> Bool
isMetaTyVar TcTyVar
v) = CheckTyEqResult -> TcM CheckTyEqResult
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteSkolemEscape)
| Bool
otherwise = TcTyVar -> TcM CheckTyEqResult
promote_one TcTyVar
v
where
no_promotion :: Bool
no_promotion = Bool -> Bool
not (TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
v TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lhs_tv_lvl)
promote_one :: TcTyVar -> TcM CheckTyEqResult
promote_one TcTyVar
tv = do { _ <- MetaInfo -> TcLevel -> TcTyVar -> TcM TcType
promote_meta_tyvar MetaInfo
TauTv TcLevel
lhs_tv_lvl TcTyVar
tv
; return cteOK }
promote_meta_tyvar :: MetaInfo -> TcLevel -> TcTyVar -> TcM TcType
promote_meta_tyvar :: MetaInfo -> TcLevel -> TcTyVar -> TcM TcType
promote_meta_tyvar MetaInfo
info TcLevel
dest_lvl TcTyVar
occ_tv
= do {
mb_filled <- TcTyVar -> IOEnv (Env TcGblEnv TcLclEnv) (Maybe TcType)
isFilledMetaTyVar_maybe TcTyVar
occ_tv
; case mb_filled of {
Just TcType
ty -> TcType -> TcM TcType
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return TcType
ty ;
Maybe TcType
Nothing ->
do { new_tv <- MetaInfo -> TcLevel -> TcTyVar -> TcM TcTyVar
cloneMetaTyVarWithInfo MetaInfo
info TcLevel
dest_lvl TcTyVar
occ_tv
; liftZonkM $ writeMetaTyVar occ_tv (mkTyVarTy new_tv)
; traceTc "promoteTyVar" (ppr occ_tv <+> text "-->" <+> ppr new_tv)
; return (mkTyVarTy new_tv) } } }
touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
touchabilityAndShapeTest TcLevel
given_eq_lvl TcTyVar
tv TcType
rhs
| MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info, mtv_tclvl :: TcTyVarDetails -> TcLevel
mtv_tclvl = TcLevel
tv_lvl } <- TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv
, TcLevel
tv_lvl TcLevel -> TcLevel -> Bool
`deeperThanOrSame` TcLevel
given_eq_lvl
, MetaInfo -> TcType -> Bool
checkTopShape MetaInfo
info TcType
rhs
= Bool
True
| Bool
otherwise
= Bool
False
checkTopShape :: MetaInfo -> TcType -> Bool
checkTopShape :: MetaInfo -> TcType -> Bool
checkTopShape MetaInfo
info TcType
xi
= case MetaInfo
info of
MetaInfo
TyVarTv ->
case TcType -> Maybe TcTyVar
getTyVar_maybe TcType
xi of
Maybe TcTyVar
Nothing -> Bool
False
Just TcTyVar
tv -> case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
SkolemTv {} -> Bool
True
TcTyVarDetails
RuntimeUnk -> Bool
True
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
TyVarTv } -> Bool
True
TcTyVarDetails
_ -> Bool
False
MetaInfo
CycleBreakerTv -> Bool
False
MetaInfo
_ -> Bool
True