{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Utils.Unify (
tcWrapResult, tcWrapResultO, tcWrapResultMono,
tcSkolemise, tcSkolemiseScoped, tcSkolemiseET,
tcSubType, tcSubTypeSigma, tcSubTypePat,
tcSubMult,
checkConstraints, checkTvConstraints,
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
unifyType, unifyKind,
uType, promoteTcType,
swapOverTyVars, canSolveByUnification,
tcInfer,
matchExpectedListTy,
matchExpectedTyConApp,
matchExpectedAppTy,
matchExpectedFunTys,
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
) where
#include "GhclibHsVersions.h"
import GHC.Prelude
import GHC.Hs
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr( debugPprType )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.TcType
import GHC.Tc.Utils.Env
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.Multiplicity
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Types.Origin
import GHC.Types.Name( isSystemName )
import GHC.Tc.Utils.Instantiate
import GHC.Core.TyCon
import GHC.Builtin.Types
import GHC.Types.Var as Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Utils.Error
import GHC.Driver.Session
import GHC.Types.Basic
import GHC.Data.Bag
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import Control.Monad
import Control.Arrow ( second )
matchActualFunTySigma
:: SDoc
-> Maybe SDoc
-> (Arity, [Scaled TcSigmaType])
-> TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma :: SDoc
-> Maybe SDoc
-> (Arity, [Scaled TcSigmaType])
-> TcSigmaType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma SDoc
herald Maybe SDoc
mb_thing (Arity, [Scaled TcSigmaType])
err_info TcSigmaType
fun_ty
= ASSERT2( isRhoTy fun_ty, ppr fun_ty )
TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
go TcSigmaType
fun_ty
where
go :: TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
go :: TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
go TcSigmaType
ty | Just TcSigmaType
ty' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
ty = TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
go TcSigmaType
ty'
go (FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
w, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg_ty, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res_ty })
= ASSERT( af == VisArg )
(HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
w TcSigmaType
arg_ty, TcSigmaType
res_ty)
go ty :: TcSigmaType
ty@(TyVarTy Var
tv)
| Var -> Bool
isMetaTyVar Var
tv
= do { MetaDetails
cts <- Var -> TcM MetaDetails
readMetaTyVar Var
tv
; case MetaDetails
cts of
Indirect TcSigmaType
ty' -> TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
go TcSigmaType
ty'
MetaDetails
Flexi -> TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
defer TcSigmaType
ty }
go TcSigmaType
ty = (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (TcSigmaType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt TcSigmaType
ty) (TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
defer TcSigmaType
ty)
defer :: TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
defer TcSigmaType
fun_ty
= do { TcSigmaType
arg_ty <- TcM TcSigmaType
newOpenFlexiTyVarTy
; TcSigmaType
res_ty <- TcM TcSigmaType
newOpenFlexiTyVarTy
; let unif_fun_ty :: TcSigmaType
unif_fun_ty = TcSigmaType -> TcSigmaType -> TcSigmaType
mkVisFunTyMany TcSigmaType
arg_ty TcSigmaType
res_ty
; TcCoercionN
co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
mb_thing TcSigmaType
fun_ty TcSigmaType
unif_fun_ty
; (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> HsWrapper
mkWpCastN TcCoercionN
co, TcSigmaType -> Scaled TcSigmaType
forall a. a -> Scaled a
unrestricted TcSigmaType
arg_ty, TcSigmaType
res_ty) }
mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
mk_ctxt :: TcSigmaType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt TcSigmaType
res_ty TidyEnv
env = TidyEnv
-> SDoc
-> [Scaled TcSigmaType]
-> TcSigmaType
-> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env SDoc
herald ([Scaled TcSigmaType] -> [Scaled TcSigmaType]
forall a. [a] -> [a]
reverse [Scaled TcSigmaType]
arg_tys_so_far)
TcSigmaType
res_ty Arity
n_val_args_in_call
(Arity
n_val_args_in_call, [Scaled TcSigmaType]
arg_tys_so_far) = (Arity, [Scaled TcSigmaType])
err_info
matchActualFunTysRho :: SDoc
-> CtOrigin
-> Maybe SDoc
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType)
matchActualFunTysRho :: SDoc
-> CtOrigin
-> Maybe SDoc
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
matchActualFunTysRho SDoc
herald CtOrigin
ct_orig Maybe SDoc
mb_thing Arity
n_val_args_wanted TcSigmaType
fun_ty
= Arity
-> [Scaled TcSigmaType]
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
go Arity
n_val_args_wanted [] TcSigmaType
fun_ty
where
go :: Arity
-> [Scaled TcSigmaType]
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
go Arity
n [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty
| Bool -> Bool
not (TcSigmaType -> Bool
isRhoTy TcSigmaType
fun_ty)
= do { (HsWrapper
wrap1, TcSigmaType
rho) <- CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcSigmaType)
topInstantiate CtOrigin
ct_orig TcSigmaType
fun_ty
; (HsWrapper
wrap2, [Scaled TcSigmaType]
arg_tys, TcSigmaType
res_ty) <- Arity
-> [Scaled TcSigmaType]
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
go Arity
n [Scaled TcSigmaType]
so_far TcSigmaType
rho
; (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1, [Scaled TcSigmaType]
arg_tys, TcSigmaType
res_ty) }
go Arity
0 [Scaled TcSigmaType]
_ TcSigmaType
fun_ty = (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, [], TcSigmaType
fun_ty)
go Arity
n [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty
= do { (HsWrapper
wrap_fun1, Scaled TcSigmaType
arg_ty1, TcSigmaType
res_ty1) <- SDoc
-> Maybe SDoc
-> (Arity, [Scaled TcSigmaType])
-> TcSigmaType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma
SDoc
herald Maybe SDoc
mb_thing
(Arity
n_val_args_wanted, [Scaled TcSigmaType]
so_far)
TcSigmaType
fun_ty
; (HsWrapper
wrap_res, [Scaled TcSigmaType]
arg_tys, TcSigmaType
res_ty) <- Arity
-> [Scaled TcSigmaType]
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
go (Arity
nArity -> Arity -> Arity
forall a. Num a => a -> a -> a
-Arity
1) (Scaled TcSigmaType
arg_ty1Scaled TcSigmaType -> [Scaled TcSigmaType] -> [Scaled TcSigmaType]
forall a. a -> [a] -> [a]
:[Scaled TcSigmaType]
so_far) TcSigmaType
res_ty1
; let wrap_fun2 :: HsWrapper
wrap_fun2 = HsWrapper
-> HsWrapper
-> Scaled TcSigmaType
-> TcSigmaType
-> SDoc
-> HsWrapper
mkWpFun HsWrapper
idHsWrapper HsWrapper
wrap_res Scaled TcSigmaType
arg_ty1 TcSigmaType
res_ty SDoc
doc
; (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap_fun2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap_fun1, Scaled TcSigmaType
arg_ty1Scaled TcSigmaType -> [Scaled TcSigmaType] -> [Scaled TcSigmaType]
forall a. a -> [a] -> [a]
:[Scaled TcSigmaType]
arg_tys, TcSigmaType
res_ty) }
where
doc :: SDoc
doc = String -> SDoc
text String
"When inferring the argument type of a function with type" SDoc -> SDoc -> SDoc
<+>
SDoc -> SDoc
quotes (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_ty)
matchExpectedFunTys :: forall a.
SDoc
-> UserTypeCtxt
-> Arity
-> ExpRhoType
-> ([Scaled ExpSigmaType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys :: SDoc
-> UserTypeCtxt
-> Arity
-> ExpRhoType
-> ([Scaled ExpRhoType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys SDoc
herald UserTypeCtxt
ctx Arity
arity ExpRhoType
orig_ty [Scaled ExpRhoType] -> ExpRhoType -> TcM a
thing_inside
= case ExpRhoType
orig_ty of
Check TcSigmaType
ty -> [Scaled ExpRhoType] -> Arity -> TcSigmaType -> TcM (HsWrapper, a)
go [] Arity
arity TcSigmaType
ty
ExpRhoType
_ -> [Scaled ExpRhoType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer [] Arity
arity ExpRhoType
orig_ty
where
go :: [Scaled ExpRhoType] -> Arity -> TcSigmaType -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Arity
n TcSigmaType
ty
| ([Var]
tvs, ThetaType
theta, TcSigmaType
_) <- TcSigmaType -> ([Var], ThetaType, TcSigmaType)
tcSplitSigmaTy TcSigmaType
ty
, Bool -> Bool
not ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= do { (HsWrapper
wrap_gen, (HsWrapper
wrap_res, a
result)) <- UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM (HsWrapper, a))
-> TcM (HsWrapper, (HsWrapper, a))
forall result.
UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise UserTypeCtxt
ctx TcSigmaType
ty ((TcSigmaType -> TcM (HsWrapper, a))
-> TcM (HsWrapper, (HsWrapper, a)))
-> (TcSigmaType -> TcM (HsWrapper, a))
-> TcM (HsWrapper, (HsWrapper, a))
forall a b. (a -> b) -> a -> b
$ \TcSigmaType
ty' ->
[Scaled ExpRhoType] -> Arity -> TcSigmaType -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Arity
n TcSigmaType
ty'
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap_gen HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap_res, a
result) }
go [Scaled ExpRhoType]
acc_arg_tys Arity
0 TcSigmaType
rho_ty
= do { a
result <- [Scaled ExpRhoType] -> ExpRhoType -> TcM a
thing_inside ([Scaled ExpRhoType] -> [Scaled ExpRhoType]
forall a. [a] -> [a]
reverse [Scaled ExpRhoType]
acc_arg_tys) (TcSigmaType -> ExpRhoType
mkCheckExpType TcSigmaType
rho_ty)
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, a
result) }
go [Scaled ExpRhoType]
acc_arg_tys Arity
n TcSigmaType
ty
| Just TcSigmaType
ty' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
ty = [Scaled ExpRhoType] -> Arity -> TcSigmaType -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Arity
n TcSigmaType
ty'
go [Scaled ExpRhoType]
acc_arg_tys Arity
n (FunTy { ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
mult, ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg_ty, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res_ty })
= ASSERT( af == VisArg )
do { (HsWrapper
wrap_res, a
result) <- [Scaled ExpRhoType] -> Arity -> TcSigmaType -> TcM (HsWrapper, a)
go ((TcSigmaType -> ExpRhoType -> Scaled ExpRhoType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
mult (ExpRhoType -> Scaled ExpRhoType)
-> ExpRhoType -> Scaled ExpRhoType
forall a b. (a -> b) -> a -> b
$ TcSigmaType -> ExpRhoType
mkCheckExpType TcSigmaType
arg_ty) Scaled ExpRhoType -> [Scaled ExpRhoType] -> [Scaled ExpRhoType]
forall a. a -> [a] -> [a]
: [Scaled ExpRhoType]
acc_arg_tys)
(Arity
nArity -> Arity -> Arity
forall a. Num a => a -> a -> a
-Arity
1) TcSigmaType
res_ty
; let fun_wrap :: HsWrapper
fun_wrap = HsWrapper
-> HsWrapper
-> Scaled TcSigmaType
-> TcSigmaType
-> SDoc
-> HsWrapper
mkWpFun HsWrapper
idHsWrapper HsWrapper
wrap_res (TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
mult TcSigmaType
arg_ty) TcSigmaType
res_ty SDoc
doc
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall (m :: * -> *) a. Monad m => a -> m a
return ( HsWrapper
fun_wrap, a
result ) }
where
doc :: SDoc
doc = String -> SDoc
text String
"When inferring the argument type of a function with type" SDoc -> SDoc -> SDoc
<+>
SDoc -> SDoc
quotes (ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
orig_ty)
go [Scaled ExpRhoType]
acc_arg_tys Arity
n ty :: TcSigmaType
ty@(TyVarTy Var
tv)
| Var -> Bool
isMetaTyVar Var
tv
= do { MetaDetails
cts <- Var -> TcM MetaDetails
readMetaTyVar Var
tv
; case MetaDetails
cts of
Indirect TcSigmaType
ty' -> [Scaled ExpRhoType] -> Arity -> TcSigmaType -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Arity
n TcSigmaType
ty'
MetaDetails
Flexi -> [Scaled ExpRhoType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer [Scaled ExpRhoType]
acc_arg_tys Arity
n (TcSigmaType -> ExpRhoType
mkCheckExpType TcSigmaType
ty) }
go [Scaled ExpRhoType]
acc_arg_tys Arity
n TcSigmaType
ty = (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM ([Scaled ExpRhoType]
-> TcSigmaType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt [Scaled ExpRhoType]
acc_arg_tys TcSigmaType
ty) (TcM (HsWrapper, a) -> TcM (HsWrapper, a))
-> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$
[Scaled ExpRhoType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer [Scaled ExpRhoType]
acc_arg_tys Arity
n (TcSigmaType -> ExpRhoType
mkCheckExpType TcSigmaType
ty)
defer :: [Scaled ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer :: [Scaled ExpRhoType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer [Scaled ExpRhoType]
acc_arg_tys Arity
n ExpRhoType
fun_ty
= do { [ExpRhoType]
more_arg_tys <- Arity
-> IOEnv (Env TcGblEnv TcLclEnv) ExpRhoType
-> IOEnv (Env TcGblEnv TcLclEnv) [ExpRhoType]
forall (m :: * -> *) a. Applicative m => Arity -> m a -> m [a]
replicateM Arity
n IOEnv (Env TcGblEnv TcLclEnv) ExpRhoType
newInferExpType
; ExpRhoType
res_ty <- IOEnv (Env TcGblEnv TcLclEnv) ExpRhoType
newInferExpType
; a
result <- [Scaled ExpRhoType] -> ExpRhoType -> TcM a
thing_inside ([Scaled ExpRhoType] -> [Scaled ExpRhoType]
forall a. [a] -> [a]
reverse [Scaled ExpRhoType]
acc_arg_tys [Scaled ExpRhoType] -> [Scaled ExpRhoType] -> [Scaled ExpRhoType]
forall a. [a] -> [a] -> [a]
++ ((ExpRhoType -> Scaled ExpRhoType)
-> [ExpRhoType] -> [Scaled ExpRhoType]
forall a b. (a -> b) -> [a] -> [b]
map ExpRhoType -> Scaled ExpRhoType
forall a. a -> Scaled a
unrestricted [ExpRhoType]
more_arg_tys)) ExpRhoType
res_ty
; ThetaType
more_arg_tys <- (ExpRhoType -> TcM TcSigmaType)
-> [ExpRhoType] -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ExpRhoType -> TcM TcSigmaType
readExpType [ExpRhoType]
more_arg_tys
; TcSigmaType
res_ty <- ExpRhoType -> TcM TcSigmaType
readExpType ExpRhoType
res_ty
; let unif_fun_ty :: TcSigmaType
unif_fun_ty = ThetaType -> TcSigmaType -> TcSigmaType
mkVisFunTysMany ThetaType
more_arg_tys TcSigmaType
res_ty
; HsWrapper
wrap <- CtOrigin
-> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
tcSubType CtOrigin
AppOrigin UserTypeCtxt
ctx TcSigmaType
unif_fun_ty ExpRhoType
fun_ty
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap, a
result) }
mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
mk_ctxt :: [Scaled ExpRhoType]
-> TcSigmaType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt [Scaled ExpRhoType]
arg_tys TcSigmaType
res_ty TidyEnv
env
= TidyEnv
-> SDoc
-> [Scaled TcSigmaType]
-> TcSigmaType
-> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env SDoc
herald [Scaled TcSigmaType]
arg_tys' TcSigmaType
res_ty Arity
arity
where
arg_tys' :: [Scaled TcSigmaType]
arg_tys' = (Scaled ExpRhoType -> Scaled TcSigmaType)
-> [Scaled ExpRhoType] -> [Scaled TcSigmaType]
forall a b. (a -> b) -> [a] -> [b]
map (\(Scaled TcSigmaType
u ExpRhoType
v) -> TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
u (String -> ExpRhoType -> TcSigmaType
checkingExpType String
"matchExpectedFunTys" ExpRhoType
v)) ([Scaled ExpRhoType] -> [Scaled TcSigmaType])
-> [Scaled ExpRhoType] -> [Scaled TcSigmaType]
forall a b. (a -> b) -> a -> b
$
[Scaled ExpRhoType] -> [Scaled ExpRhoType]
forall a. [a] -> [a]
reverse [Scaled ExpRhoType]
arg_tys
mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity
-> TcM (TidyEnv, MsgDoc)
mkFunTysMsg :: TidyEnv
-> SDoc
-> [Scaled TcSigmaType]
-> TcSigmaType
-> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env SDoc
herald [Scaled TcSigmaType]
arg_tys TcSigmaType
res_ty Arity
n_val_args_in_call
= do { (TidyEnv
env', TcSigmaType
fun_rho) <- TidyEnv -> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
zonkTidyTcType TidyEnv
env (TcSigmaType -> TcM (TidyEnv, TcSigmaType))
-> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
[Scaled TcSigmaType] -> TcSigmaType -> TcSigmaType
mkVisFunTys [Scaled TcSigmaType]
arg_tys TcSigmaType
res_ty
; let ([Scaled TcSigmaType]
all_arg_tys, TcSigmaType
_) = TcSigmaType -> ([Scaled TcSigmaType], TcSigmaType)
splitFunTys TcSigmaType
fun_rho
n_fun_args :: Arity
n_fun_args = [Scaled TcSigmaType] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Scaled TcSigmaType]
all_arg_tys
msg :: SDoc
msg | Arity
n_val_args_in_call Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
<= Arity
n_fun_args
= String -> SDoc
text String
"In the result of a function call"
| Bool
otherwise
= SDoc -> Arity -> SDoc -> SDoc
hang (SDoc
full_herald SDoc -> SDoc -> SDoc
<> SDoc
comma)
Arity
2 ([SDoc] -> SDoc
sep [ String -> SDoc
text String
"but its type" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcSigmaType -> SDoc
pprType TcSigmaType
fun_rho)
, if Arity
n_fun_args Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
0 then String -> SDoc
text String
"has none"
else String -> SDoc
text String
"has only" SDoc -> SDoc -> SDoc
<+> Arity -> SDoc
speakN Arity
n_fun_args])
; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
env', SDoc
msg) }
where
full_herald :: SDoc
full_herald = SDoc
herald SDoc -> SDoc -> SDoc
<+> Arity -> SDoc -> SDoc
speakNOf Arity
n_val_args_in_call (String -> SDoc
text String
"value argument")
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
matchExpectedListTy :: TcSigmaType -> TcM (TcCoercionN, TcSigmaType)
matchExpectedListTy TcSigmaType
exp_ty
= do { (TcCoercionN
co, [TcSigmaType
elt_ty]) <- TyCon -> TcSigmaType -> TcM (TcCoercionN, ThetaType)
matchExpectedTyConApp TyCon
listTyCon TcSigmaType
exp_ty
; (TcCoercionN, TcSigmaType) -> TcM (TcCoercionN, TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN
co, TcSigmaType
elt_ty) }
matchExpectedTyConApp :: TyCon
-> TcRhoType
-> TcM (TcCoercionN,
[TcSigmaType])
matchExpectedTyConApp :: TyCon -> TcSigmaType -> TcM (TcCoercionN, ThetaType)
matchExpectedTyConApp TyCon
tc TcSigmaType
orig_ty
= ASSERT(not $ isFunTyCon tc) go orig_ty
where
go :: TcSigmaType -> TcM (TcCoercionN, ThetaType)
go TcSigmaType
ty
| Just TcSigmaType
ty' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
ty
= TcSigmaType -> TcM (TcCoercionN, ThetaType)
go TcSigmaType
ty'
go ty :: TcSigmaType
ty@(TyConApp TyCon
tycon ThetaType
args)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tycon
= (TcCoercionN, ThetaType) -> TcM (TcCoercionN, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkTcNomReflCo TcSigmaType
ty, ThetaType
args)
go (TyVarTy Var
tv)
| Var -> Bool
isMetaTyVar Var
tv
= do { MetaDetails
cts <- Var -> TcM MetaDetails
readMetaTyVar Var
tv
; case MetaDetails
cts of
Indirect TcSigmaType
ty -> TcSigmaType -> TcM (TcCoercionN, ThetaType)
go TcSigmaType
ty
MetaDetails
Flexi -> TcM (TcCoercionN, ThetaType)
defer }
go TcSigmaType
_ = TcM (TcCoercionN, ThetaType)
defer
defer :: TcM (TcCoercionN, ThetaType)
defer
= do { (TCvSubst
_, [Var]
arg_tvs) <- [Var] -> TcM (TCvSubst, [Var])
newMetaTyVars (TyCon -> [Var]
tyConTyVars TyCon
tc)
; String -> SDoc -> TcRn ()
traceTc String
"matchExpectedTyConApp" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
$$ [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [Var]
tyConTyVars TyCon
tc) SDoc -> SDoc -> SDoc
$$ [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
arg_tvs)
; let args :: ThetaType
args = [Var] -> ThetaType
mkTyVarTys [Var]
arg_tvs
tc_template :: TcSigmaType
tc_template = TyCon -> ThetaType -> TcSigmaType
mkTyConApp TyCon
tc ThetaType
args
; TcCoercionN
co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
forall a. Maybe a
Nothing TcSigmaType
tc_template TcSigmaType
orig_ty
; (TcCoercionN, ThetaType) -> TcM (TcCoercionN, ThetaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN
co, ThetaType
args) }
matchExpectedAppTy :: TcRhoType
-> TcM (TcCoercion,
(TcSigmaType, TcSigmaType))
matchExpectedAppTy :: TcSigmaType -> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
matchExpectedAppTy TcSigmaType
orig_ty
= TcSigmaType -> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
go TcSigmaType
orig_ty
where
go :: TcSigmaType -> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
go TcSigmaType
ty
| Just TcSigmaType
ty' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
ty = TcSigmaType -> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
go TcSigmaType
ty'
| Just (TcSigmaType
fun_ty, TcSigmaType
arg_ty) <- TcSigmaType -> Maybe (TcSigmaType, TcSigmaType)
tcSplitAppTy_maybe TcSigmaType
ty
= (TcCoercionN, (TcSigmaType, TcSigmaType))
-> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkTcNomReflCo TcSigmaType
orig_ty, (TcSigmaType
fun_ty, TcSigmaType
arg_ty))
go (TyVarTy Var
tv)
| Var -> Bool
isMetaTyVar Var
tv
= do { MetaDetails
cts <- Var -> TcM MetaDetails
readMetaTyVar Var
tv
; case MetaDetails
cts of
Indirect TcSigmaType
ty -> TcSigmaType -> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
go TcSigmaType
ty
MetaDetails
Flexi -> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
defer }
go TcSigmaType
_ = TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
defer
defer :: TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
defer
= do { TcSigmaType
ty1 <- TcSigmaType -> TcM TcSigmaType
newFlexiTyVarTy TcSigmaType
kind1
; TcSigmaType
ty2 <- TcSigmaType -> TcM TcSigmaType
newFlexiTyVarTy TcSigmaType
kind2
; TcCoercionN
co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
forall a. Maybe a
Nothing (TcSigmaType -> TcSigmaType -> TcSigmaType
mkAppTy TcSigmaType
ty1 TcSigmaType
ty2) TcSigmaType
orig_ty
; (TcCoercionN, (TcSigmaType, TcSigmaType))
-> TcM (TcCoercionN, (TcSigmaType, TcSigmaType))
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN
co, (TcSigmaType
ty1, TcSigmaType
ty2)) }
orig_kind :: TcSigmaType
orig_kind = HasDebugCallStack => TcSigmaType -> TcSigmaType
TcSigmaType -> TcSigmaType
tcTypeKind TcSigmaType
orig_ty
kind1 :: TcSigmaType
kind1 = TcSigmaType -> TcSigmaType -> TcSigmaType
mkVisFunTyMany TcSigmaType
liftedTypeKind TcSigmaType
orig_kind
kind2 :: TcSigmaType
kind2 = TcSigmaType
liftedTypeKind
tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResult :: HsExpr GhcRn
-> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResult HsExpr GhcRn
rn_expr = CtOrigin
-> HsExpr GhcRn
-> HsExpr GhcTc
-> TcSigmaType
-> 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
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultO CtOrigin
orig HsExpr GhcRn
rn_expr HsExpr GhcTc
expr TcSigmaType
actual_ty ExpRhoType
res_ty
= do { String -> SDoc -> TcRn ()
traceTc String
"tcWrapResult" ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Actual: " SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
actual_ty
, String -> SDoc
text String
"Expected:" SDoc -> SDoc -> SDoc
<+> ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
res_ty ])
; HsWrapper
wrap <- CtOrigin
-> UserTypeCtxt
-> Maybe SDoc
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
orig UserTypeCtxt
GenSigCtxt (SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_expr)) TcSigmaType
actual_ty ExpRhoType
res_ty
; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
wrap HsExpr GhcTc
expr) }
tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
-> TcRhoType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultMono :: HsExpr GhcRn
-> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
rn_expr HsExpr GhcTc
expr TcSigmaType
act_ty ExpRhoType
res_ty
= ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr )
do { TcCoercionN
co <- case ExpRhoType
res_ty of
Infer InferResult
inf_res -> TcSigmaType -> InferResult -> TcM TcCoercionN
fillInferResult TcSigmaType
act_ty InferResult
inf_res
Check TcSigmaType
exp_ty -> Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType (SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_expr)) TcSigmaType
act_ty TcSigmaType
exp_ty
; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrapCo TcCoercionN
co HsExpr GhcTc
expr) }
tcSubTypePat :: CtOrigin -> UserTypeCtxt
-> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypePat :: CtOrigin
-> UserTypeCtxt -> ExpRhoType -> TcSigmaType -> TcM HsWrapper
tcSubTypePat CtOrigin
inst_orig UserTypeCtxt
ctxt (Check TcSigmaType
ty_actual) TcSigmaType
ty_expected
= (TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyTypeET CtOrigin
inst_orig UserTypeCtxt
ctxt TcSigmaType
ty_actual TcSigmaType
ty_expected
tcSubTypePat CtOrigin
_ UserTypeCtxt
_ (Infer InferResult
inf_res) TcSigmaType
ty_expected
= do { TcCoercionN
co <- TcSigmaType -> InferResult -> TcM TcCoercionN
fillInferResult TcSigmaType
ty_expected InferResult
inf_res
; HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> HsWrapper
mkWpCastN (TcCoercionN -> TcCoercionN
mkTcSymCo TcCoercionN
co)) }
tcSubType :: CtOrigin -> UserTypeCtxt
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubType :: CtOrigin
-> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
tcSubType CtOrigin
orig UserTypeCtxt
ctxt TcSigmaType
ty_actual ExpRhoType
ty_expected
= TcSigmaType -> ExpRhoType -> TcM HsWrapper -> TcM HsWrapper
forall a. TcSigmaType -> ExpRhoType -> TcM a -> TcM a
addSubTypeCtxt TcSigmaType
ty_actual ExpRhoType
ty_expected (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcRn ()
traceTc String
"tcSubType" ([SDoc] -> SDoc
vcat [UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt, TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_actual, ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
ty_expected])
; CtOrigin
-> UserTypeCtxt
-> Maybe SDoc
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
orig UserTypeCtxt
ctxt Maybe SDoc
forall a. Maybe a
Nothing TcSigmaType
ty_actual ExpRhoType
ty_expected }
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe SDoc
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe SDoc
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
inst_orig UserTypeCtxt
ctxt Maybe SDoc
m_thing TcSigmaType
ty_actual ExpRhoType
res_ty
= case ExpRhoType
res_ty of
Check TcSigmaType
ty_expected -> (TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type (Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
m_thing) CtOrigin
inst_orig UserTypeCtxt
ctxt
TcSigmaType
ty_actual TcSigmaType
ty_expected
Infer InferResult
inf_res -> do { (HsWrapper
wrap, TcSigmaType
rho) <- CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcSigmaType)
topInstantiate CtOrigin
inst_orig TcSigmaType
ty_actual
; TcCoercionN
co <- TcSigmaType -> InferResult -> TcM TcCoercionN
fillInferResult TcSigmaType
rho InferResult
inf_res
; HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> HsWrapper
mkWpCastN TcCoercionN
co HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap) }
tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeSigma UserTypeCtxt
ctxt TcSigmaType
ty_actual TcSigmaType
ty_expected
= (TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type (Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
forall a. Maybe a
Nothing) CtOrigin
eq_orig UserTypeCtxt
ctxt TcSigmaType
ty_actual TcSigmaType
ty_expected
where
eq_orig :: CtOrigin
eq_orig = TypeEqOrigin :: TcSigmaType -> TcSigmaType -> Maybe SDoc -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty_actual
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
ty_expected
, uo_thing :: Maybe SDoc
uo_thing = Maybe SDoc
forall a. Maybe a
Nothing
, uo_visible :: Bool
uo_visible = Bool
True }
tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type :: (TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unify CtOrigin
inst_orig UserTypeCtxt
ctxt TcSigmaType
ty_actual TcSigmaType
ty_expected
| TcSigmaType -> Bool
definitely_poly TcSigmaType
ty_expected
, Bool -> Bool
not (TcSigmaType -> Bool
possibly_poly TcSigmaType
ty_actual)
= do { String -> SDoc -> TcRn ()
traceTc String
"tc_sub_type (drop to equality)" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_actual
, String -> SDoc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_expected ]
; TcCoercionN -> HsWrapper
mkWpCastN (TcCoercionN -> HsWrapper) -> TcM TcCoercionN -> TcM HsWrapper
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unify TcSigmaType
ty_actual TcSigmaType
ty_expected }
| Bool
otherwise
= do { String -> SDoc -> TcRn ()
traceTc String
"tc_sub_type (general case)" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_actual
, String -> SDoc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_expected ]
; (HsWrapper
sk_wrap, HsWrapper
inner_wrap)
<- UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM HsWrapper)
-> TcM (HsWrapper, HsWrapper)
forall result.
UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise UserTypeCtxt
ctxt TcSigmaType
ty_expected ((TcSigmaType -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper))
-> (TcSigmaType -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper)
forall a b. (a -> b) -> a -> b
$ \ TcSigmaType
sk_rho ->
do { (HsWrapper
wrap, TcSigmaType
rho_a) <- CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcSigmaType)
topInstantiate CtOrigin
inst_orig TcSigmaType
ty_actual
; TcCoercionN
cow <- TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unify TcSigmaType
rho_a TcSigmaType
sk_rho
; HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> HsWrapper
mkWpCastN TcCoercionN
cow HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap) }
; HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
sk_wrap HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
inner_wrap) }
where
possibly_poly :: TcSigmaType -> Bool
possibly_poly TcSigmaType
ty = Bool -> Bool
not (TcSigmaType -> Bool
isRhoTy TcSigmaType
ty)
definitely_poly :: TcSigmaType -> Bool
definitely_poly TcSigmaType
ty
| ([Var]
tvs, ThetaType
theta, TcSigmaType
tau) <- TcSigmaType -> ([Var], ThetaType, TcSigmaType)
tcSplitSigmaTy TcSigmaType
ty
, (Var
tv:[Var]
_) <- [Var]
tvs
, ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta
, EqRel -> Var -> TcSigmaType -> Bool
isInsolubleOccursCheck EqRel
NomEq Var
tv TcSigmaType
tau
= Bool
True
| Bool
otherwise
= Bool
False
addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
addSubTypeCtxt :: TcSigmaType -> ExpRhoType -> TcM a -> TcM a
addSubTypeCtxt TcSigmaType
ty_actual ExpRhoType
ty_expected TcM a
thing_inside
| TcSigmaType -> Bool
isRhoTy TcSigmaType
ty_actual
, ExpRhoType -> Bool
isRhoExpTy ExpRhoType
ty_expected
= TcM a
thing_inside
| Bool
otherwise
= (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM TidyEnv -> TcM (TidyEnv, SDoc)
mk_msg TcM a
thing_inside
where
mk_msg :: TidyEnv -> TcM (TidyEnv, SDoc)
mk_msg TidyEnv
tidy_env
= do { (TidyEnv
tidy_env, TcSigmaType
ty_actual) <- TidyEnv -> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
zonkTidyTcType TidyEnv
tidy_env TcSigmaType
ty_actual
; Maybe TcSigmaType
mb_ty_expected <- ExpRhoType -> TcM (Maybe TcSigmaType)
readExpType_maybe ExpRhoType
ty_expected
; (TidyEnv
tidy_env, ExpRhoType
ty_expected) <- case Maybe TcSigmaType
mb_ty_expected of
Just TcSigmaType
ty -> (TcSigmaType -> ExpRhoType)
-> (TidyEnv, TcSigmaType) -> (TidyEnv, ExpRhoType)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second TcSigmaType -> ExpRhoType
mkCheckExpType ((TidyEnv, TcSigmaType) -> (TidyEnv, ExpRhoType))
-> TcM (TidyEnv, TcSigmaType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, ExpRhoType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
TidyEnv -> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
zonkTidyTcType TidyEnv
tidy_env TcSigmaType
ty
Maybe TcSigmaType
Nothing -> (TidyEnv, ExpRhoType)
-> IOEnv (Env TcGblEnv TcLclEnv) (TidyEnv, ExpRhoType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, ExpRhoType
ty_expected)
; TcSigmaType
ty_expected <- ExpRhoType -> TcM TcSigmaType
readExpType ExpRhoType
ty_expected
; (TidyEnv
tidy_env, TcSigmaType
ty_expected) <- TidyEnv -> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
zonkTidyTcType TidyEnv
tidy_env TcSigmaType
ty_expected
; let msg :: SDoc
msg = [SDoc] -> SDoc
vcat [ SDoc -> Arity -> SDoc -> SDoc
hang (String -> SDoc
text String
"When checking that:")
Arity
4 (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_actual)
, Arity -> SDoc -> SDoc
nest Arity
2 (SDoc -> Arity -> SDoc -> SDoc
hang (String -> SDoc
text String
"is more polymorphic than:")
Arity
2 (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty_expected)) ]
; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
msg) }
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
tcSubMult :: CtOrigin -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubMult CtOrigin
origin TcSigmaType
w_actual TcSigmaType
w_expected
| Just (TcSigmaType
w1, TcSigmaType
w2) <- TcSigmaType -> Maybe (TcSigmaType, TcSigmaType)
isMultMul TcSigmaType
w_actual =
do { HsWrapper
w1 <- CtOrigin -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubMult CtOrigin
origin TcSigmaType
w1 TcSigmaType
w_expected
; HsWrapper
w2 <- CtOrigin -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubMult CtOrigin
origin TcSigmaType
w2 TcSigmaType
w_expected
; HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
w1 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
w2) }
tcSubMult CtOrigin
origin TcSigmaType
w_actual TcSigmaType
w_expected =
case TcSigmaType -> TcSigmaType -> IsSubmult
submult TcSigmaType
w_actual TcSigmaType
w_expected of
IsSubmult
Submult -> HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return HsWrapper
WpHole
IsSubmult
Unknown -> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcEqMult CtOrigin
origin TcSigmaType
w_actual TcSigmaType
w_expected
tcEqMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
tcEqMult :: CtOrigin -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcEqMult CtOrigin
origin TcSigmaType
w_actual TcSigmaType
w_expected = do
{
; TcCoercionN
coercion <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
TypeLevel CtOrigin
origin TcSigmaType
w_actual TcSigmaType
w_expected
; HsWrapper -> TcM HsWrapper
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> TcM HsWrapper) -> HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$ if TcCoercionN -> Bool
isReflCo TcCoercionN
coercion then HsWrapper
WpHole else TcCoercionN -> HsWrapper
WpMultCoercion TcCoercionN
coercion }
tcSkolemise, tcSkolemiseScoped
:: UserTypeCtxt -> TcSigmaType
-> (TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseScoped :: UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseScoped UserTypeCtxt
ctxt TcSigmaType
expected_ty TcSigmaType -> TcM result
thing_inside
= do { (HsWrapper
wrap, [(Name, Var)]
tv_prs, [Var]
given, TcSigmaType
rho_ty) <- TcSigmaType -> TcM (HsWrapper, [(Name, Var)], [Var], TcSigmaType)
topSkolemise TcSigmaType
expected_ty
; let skol_tvs :: [Var]
skol_tvs = ((Name, Var) -> Var) -> [(Name, Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Var) -> Var
forall a b. (a, b) -> b
snd [(Name, Var)]
tv_prs
skol_info :: SkolemInfo
skol_info = UserTypeCtxt -> TcSigmaType -> [(Name, Var)] -> SkolemInfo
SigSkol UserTypeCtxt
ctxt TcSigmaType
expected_ty [(Name, Var)]
tv_prs
; (TcEvBinds
ev_binds, result
res)
<- SkolemInfo
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfo
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfo
skol_info [Var]
skol_tvs [Var]
given (TcM result -> TcM (TcEvBinds, result))
-> TcM result -> TcM (TcEvBinds, result)
forall a b. (a -> b) -> a -> b
$
[(Name, Var)] -> TcM result -> TcM result
forall r. [(Name, Var)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, Var)]
tv_prs (TcM result -> TcM result) -> TcM result -> TcM result
forall a b. (a -> b) -> a -> b
$
TcSigmaType -> TcM result
thing_inside TcSigmaType
rho_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> TcEvBinds -> HsWrapper
mkWpLet TcEvBinds
ev_binds, result
res) }
tcSkolemise :: UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise UserTypeCtxt
ctxt TcSigmaType
expected_ty TcSigmaType -> TcM result
thing_inside
| TcSigmaType -> Bool
isRhoTy TcSigmaType
expected_ty
= do { result
res <- TcSigmaType -> TcM result
thing_inside TcSigmaType
expected_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, result
res) }
| Bool
otherwise
= do { (HsWrapper
wrap, [(Name, Var)]
tv_prs, [Var]
given, TcSigmaType
rho_ty) <- TcSigmaType -> TcM (HsWrapper, [(Name, Var)], [Var], TcSigmaType)
topSkolemise TcSigmaType
expected_ty
; let skol_tvs :: [Var]
skol_tvs = ((Name, Var) -> Var) -> [(Name, Var)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Var) -> Var
forall a b. (a, b) -> b
snd [(Name, Var)]
tv_prs
skol_info :: SkolemInfo
skol_info = UserTypeCtxt -> TcSigmaType -> [(Name, Var)] -> SkolemInfo
SigSkol UserTypeCtxt
ctxt TcSigmaType
expected_ty [(Name, Var)]
tv_prs
; (TcEvBinds
ev_binds, result
result)
<- SkolemInfo
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfo
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfo
skol_info [Var]
skol_tvs [Var]
given (TcM result -> TcM (TcEvBinds, result))
-> TcM result -> TcM (TcEvBinds, result)
forall a b. (a -> b) -> a -> b
$
TcSigmaType -> TcM result
thing_inside TcSigmaType
rho_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> TcEvBinds -> HsWrapper
mkWpLet TcEvBinds
ev_binds, result
result) }
tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType
-> (ExpRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseET :: UserTypeCtxt
-> ExpRhoType
-> (ExpRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseET UserTypeCtxt
_ et :: ExpRhoType
et@(Infer {}) ExpRhoType -> TcM result
thing_inside
= (HsWrapper
idHsWrapper, ) (result -> (HsWrapper, result))
-> TcM result -> TcM (HsWrapper, result)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpRhoType -> TcM result
thing_inside ExpRhoType
et
tcSkolemiseET UserTypeCtxt
ctxt (Check TcSigmaType
ty) ExpRhoType -> TcM result
thing_inside
= UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM result)
-> TcM (HsWrapper, result)
forall result.
UserTypeCtxt
-> TcSigmaType
-> (TcSigmaType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemise UserTypeCtxt
ctxt TcSigmaType
ty ((TcSigmaType -> TcM result) -> TcM (HsWrapper, result))
-> (TcSigmaType -> TcM result) -> TcM (HsWrapper, result)
forall a b. (a -> b) -> a -> b
$ \TcSigmaType
rho_ty ->
ExpRhoType -> TcM result
thing_inside (TcSigmaType -> ExpRhoType
mkCheckExpType TcSigmaType
rho_ty)
checkConstraints :: SkolemInfo
-> [TcTyVar]
-> [EvVar]
-> TcM result
-> TcM (TcEvBinds, result)
checkConstraints :: SkolemInfo
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfo
skol_info [Var]
skol_tvs [Var]
given TcM result
thing_inside
= do { Bool
implication_needed <- SkolemInfo -> [Var] -> [Var] -> TcM Bool
implicationNeeded SkolemInfo
skol_info [Var]
skol_tvs [Var]
given
; if Bool
implication_needed
then do { (TcLevel
tclvl, WantedConstraints
wanted, result
result) <- TcM result -> TcM (TcLevel, WantedConstraints, result)
forall a. TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndCaptureConstraints TcM result
thing_inside
; (Bag Implication
implics, TcEvBinds
ev_binds) <- TcLevel
-> SkolemInfo
-> [Var]
-> [Var]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfo
skol_info [Var]
skol_tvs [Var]
given WantedConstraints
wanted
; String -> SDoc -> TcRn ()
traceTc String
"checkConstraints" (TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl SDoc -> SDoc -> SDoc
$$ [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
skol_tvs)
; Bag Implication -> TcRn ()
emitImplications Bag Implication
implics
; (TcEvBinds, result) -> TcM (TcEvBinds, result)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcEvBinds
ev_binds, result
result) }
else
do { result
res <- TcM result
thing_inside
; (TcEvBinds, result) -> TcM (TcEvBinds, result)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcEvBinds
emptyTcEvBinds, result
res) } }
checkTvConstraints :: SkolemInfo
-> [TcTyVar]
-> TcM result
-> TcM result
checkTvConstraints :: SkolemInfo -> [Var] -> TcM result -> TcM result
checkTvConstraints SkolemInfo
skol_info [Var]
skol_tvs TcM result
thing_inside
= do { (TcLevel
tclvl, WantedConstraints
wanted, result
result) <- TcM result -> TcM (TcLevel, WantedConstraints, result)
forall a. TcM a -> TcM (TcLevel, WantedConstraints, a)
pushLevelAndCaptureConstraints TcM result
thing_inside
; SkolemInfo -> [Var] -> TcLevel -> WantedConstraints -> TcRn ()
emitResidualTvConstraint SkolemInfo
skol_info [Var]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; result -> TcM result
forall (m :: * -> *) a. Monad m => a -> m a
return result
result }
emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint :: SkolemInfo -> [Var] -> TcLevel -> WantedConstraints -> TcRn ()
emitResidualTvConstraint SkolemInfo
skol_info [Var]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
| WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted
= () -> TcRn ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise
= do { Implication
implic <- SkolemInfo
-> [Var] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfo
skol_info [Var]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; Implication -> TcRn ()
emitImplication Implication
implic }
buildTvImplication :: SkolemInfo -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication :: SkolemInfo
-> [Var] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfo
skol_info [Var]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
= do { EvBindsVar
ev_binds <- TcM EvBindsVar
newNoTcEvBinds
; Implication
implic <- TcM Implication
newImplication
; Implication -> TcM Implication
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication
implic { ic_tclvl :: TcLevel
ic_tclvl = TcLevel
tclvl
, ic_skols :: [Var]
ic_skols = [Var]
skol_tvs
, ic_no_eqs :: Bool
ic_no_eqs = Bool
True
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wanted
, ic_binds :: EvBindsVar
ic_binds = EvBindsVar
ev_binds
, ic_info :: SkolemInfo
ic_info = SkolemInfo
skol_info }) }
implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
implicationNeeded :: SkolemInfo -> [Var] -> [Var] -> TcM Bool
implicationNeeded SkolemInfo
skol_info [Var]
skol_tvs [Var]
given
| [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
skol_tvs
, [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
given
, Bool -> Bool
not (SkolemInfo -> Bool
alwaysBuildImplication SkolemInfo
skol_info)
=
do { TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
; if Bool -> Bool
not (TcLevel -> Bool
isTopTcLevel TcLevel
tc_lvl)
then Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
else
do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DeferTypeErrors DynFlags
dflags Bool -> Bool -> Bool
||
GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DeferTypedHoles DynFlags
dflags Bool -> Bool -> Bool
||
GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DeferOutOfScopeVariables DynFlags
dflags) } }
| Bool
otherwise
= Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
alwaysBuildImplication :: SkolemInfo -> Bool
alwaysBuildImplication :: SkolemInfo -> Bool
alwaysBuildImplication SkolemInfo
_ = Bool
False
buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
-> [EvVar] -> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor :: TcLevel
-> SkolemInfo
-> [Var]
-> [Var]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfo
skol_info [Var]
skol_tvs [Var]
given WantedConstraints
wanted
| WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted Bool -> Bool -> Bool
&& [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
given
= (Bag Implication, TcEvBinds) -> TcM (Bag Implication, TcEvBinds)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag Implication
forall a. Bag a
emptyBag, TcEvBinds
emptyTcEvBinds)
| Bool
otherwise
= ASSERT2( all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs, ppr skol_tvs )
do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
newTcEvBinds
; Implication
implic <- TcM Implication
newImplication
; let implic' :: Implication
implic' = Implication
implic { ic_tclvl :: TcLevel
ic_tclvl = TcLevel
tclvl
, ic_skols :: [Var]
ic_skols = [Var]
skol_tvs
, ic_given :: [Var]
ic_given = [Var]
given
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wanted
, ic_binds :: EvBindsVar
ic_binds = EvBindsVar
ev_binds_var
, ic_info :: SkolemInfo
ic_info = SkolemInfo
skol_info }
; (Bag Implication, TcEvBinds) -> TcM (Bag Implication, TcEvBinds)
forall (m :: * -> *) a. Monad m => a -> m a
return (Implication -> Bag Implication
forall a. a -> Bag a
unitBag Implication
implic', EvBindsVar -> TcEvBinds
TcEvBinds EvBindsVar
ev_binds_var) }
unifyType :: Maybe SDoc
-> TcTauType -> TcTauType
-> TcM TcCoercionN
unifyType :: Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
thing TcSigmaType
ty1 TcSigmaType
ty2
= TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
TypeLevel CtOrigin
origin TcSigmaType
ty1 TcSigmaType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin :: TcSigmaType -> TcSigmaType -> Maybe SDoc -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty1
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
ty2
, uo_thing :: Maybe SDoc
uo_thing = SDoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SDoc -> SDoc) -> Maybe SDoc -> Maybe SDoc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe SDoc
thing
, uo_visible :: Bool
uo_visible = Bool
True }
unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
unifyTypeET :: TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyTypeET TcSigmaType
ty1 TcSigmaType
ty2
= TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
TypeLevel CtOrigin
origin TcSigmaType
ty1 TcSigmaType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin :: TcSigmaType -> TcSigmaType -> Maybe SDoc -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty2
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
ty1
, uo_thing :: Maybe SDoc
uo_thing = Maybe SDoc
forall a. Maybe a
Nothing
, uo_visible :: Bool
uo_visible = Bool
True }
unifyKind :: Maybe SDoc -> TcKind -> TcKind -> TcM CoercionN
unifyKind :: Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyKind Maybe SDoc
mb_thing TcSigmaType
ty1 TcSigmaType
ty2
= TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
KindLevel CtOrigin
origin TcSigmaType
ty1 TcSigmaType
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin :: TcSigmaType -> TcSigmaType -> Maybe SDoc -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty1
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
ty2
, uo_thing :: Maybe SDoc
uo_thing = Maybe SDoc
mb_thing
, uo_visible :: Bool
uo_visible = Bool
True }
uType, uType_defer
:: TypeOrKind
-> CtOrigin
-> TcType
-> TcType
-> TcM CoercionN
uType_defer :: TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType_defer TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
ty1 TcSigmaType
ty2
= do { TcCoercionN
co <- CtOrigin
-> TypeOrKind
-> Role
-> TcSigmaType
-> TcSigmaType
-> TcM TcCoercionN
emitWantedEq CtOrigin
origin TypeOrKind
t_or_k Role
Nominal TcSigmaType
ty1 TcSigmaType
ty2
; DumpFlag -> TcRn () -> TcRn ()
forall gbl lcl. DumpFlag -> TcRnIf gbl lcl () -> TcRnIf gbl lcl ()
whenDOptM DumpFlag
Opt_D_dump_tc_trace (TcRn () -> TcRn ()) -> TcRn () -> TcRn ()
forall a b. (a -> b) -> a -> b
$ do
{ [ErrCtxt]
ctxt <- TcM [ErrCtxt]
getErrCtxt
; SDoc
doc <- TidyEnv -> [ErrCtxt] -> TcM SDoc
mkErrInfo TidyEnv
emptyTidyEnv [ErrCtxt]
ctxt
; String -> SDoc -> TcRn ()
traceTc String
"utype_defer" ([SDoc] -> SDoc
vcat [ TcSigmaType -> SDoc
debugPprType TcSigmaType
ty1
, TcSigmaType -> SDoc
debugPprType TcSigmaType
ty2
, CtOrigin -> SDoc
pprCtOrigin CtOrigin
origin
, SDoc
doc])
; String -> SDoc -> TcRn ()
traceTc String
"utype_defer2" (TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co)
}
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return TcCoercionN
co }
uType :: TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
orig_ty1 TcSigmaType
orig_ty2
= do { TcLevel
tclvl <- TcM TcLevel
getTcLevel
; String -> SDoc -> TcRn ()
traceTc String
"u_tys" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ String -> SDoc
text String
"tclvl" SDoc -> SDoc -> SDoc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl
, [SDoc] -> SDoc
sep [ TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
orig_ty1, String -> SDoc
text String
"~", TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
orig_ty2]
, CtOrigin -> SDoc
pprCtOrigin CtOrigin
origin]
; TcCoercionN
co <- TcSigmaType -> TcSigmaType -> TcM TcCoercionN
go TcSigmaType
orig_ty1 TcSigmaType
orig_ty2
; if TcCoercionN -> Bool
isReflCo TcCoercionN
co
then String -> SDoc -> TcRn ()
traceTc String
"u_tys yields no coercion" SDoc
Outputable.empty
else String -> SDoc -> TcRn ()
traceTc String
"u_tys yields coercion:" (TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co)
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return TcCoercionN
co }
where
go :: TcType -> TcType -> TcM CoercionN
go :: TcSigmaType -> TcSigmaType -> TcM TcCoercionN
go (CastTy TcSigmaType
t1 TcCoercionN
co1) TcSigmaType
t2
= do { TcCoercionN
co_tys <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
t1 TcSigmaType
t2
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> TcSigmaType -> TcCoercionN -> TcCoercionN -> TcCoercionN
mkCoherenceLeftCo Role
Nominal TcSigmaType
t1 TcCoercionN
co1 TcCoercionN
co_tys) }
go TcSigmaType
t1 (CastTy TcSigmaType
t2 TcCoercionN
co2)
= do { TcCoercionN
co_tys <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
t1 TcSigmaType
t2
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> TcSigmaType -> TcCoercionN -> TcCoercionN -> TcCoercionN
mkCoherenceRightCo Role
Nominal TcSigmaType
t2 TcCoercionN
co2 TcCoercionN
co_tys) }
go (TyVarTy Var
tv1) TcSigmaType
ty2
= do { LookupTyVarResult
lookup_res <- Var -> TcM LookupTyVarResult
lookupTcTyVar Var
tv1
; case LookupTyVarResult
lookup_res of
Filled TcSigmaType
ty1 -> do { String -> SDoc -> TcRn ()
traceTc String
"found filled tyvar" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv1 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":->" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty1)
; TcSigmaType -> TcSigmaType -> TcM TcCoercionN
go TcSigmaType
ty1 TcSigmaType
ty2 }
Unfilled TcTyVarDetails
_ -> CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar CtOrigin
origin TypeOrKind
t_or_k SwapFlag
NotSwapped Var
tv1 TcSigmaType
ty2 }
go TcSigmaType
ty1 (TyVarTy Var
tv2)
= do { LookupTyVarResult
lookup_res <- Var -> TcM LookupTyVarResult
lookupTcTyVar Var
tv2
; case LookupTyVarResult
lookup_res of
Filled TcSigmaType
ty2 -> do { String -> SDoc -> TcRn ()
traceTc String
"found filled tyvar" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv2 SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
":->" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2)
; TcSigmaType -> TcSigmaType -> TcM TcCoercionN
go TcSigmaType
ty1 TcSigmaType
ty2 }
Unfilled TcTyVarDetails
_ -> CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar CtOrigin
origin TypeOrKind
t_or_k SwapFlag
IsSwapped Var
tv2 TcSigmaType
ty1 }
go ty1 :: TcSigmaType
ty1@(TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> TcM TcCoercionN) -> TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$ TcSigmaType -> TcCoercionN
mkNomReflCo TcSigmaType
ty1
go TcSigmaType
ty1 TcSigmaType
ty2
| Just TcSigmaType
ty1' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
ty1 = TcSigmaType -> TcSigmaType -> TcM TcCoercionN
go TcSigmaType
ty1' TcSigmaType
ty2
| Just TcSigmaType
ty2' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
ty2 = TcSigmaType -> TcSigmaType -> TcM TcCoercionN
go TcSigmaType
ty1 TcSigmaType
ty2'
go (FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
VisArg, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
w1, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg1, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res1 })
(FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
VisArg, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
w2, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg2, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res2 })
= do { TcCoercionN
co_l <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
arg1 TcSigmaType
arg2
; TcCoercionN
co_r <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
res1 TcSigmaType
res2
; TcCoercionN
co_w <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
w1 TcSigmaType
w2
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> TcM TcCoercionN) -> TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$ Role -> TcCoercionN -> TcCoercionN -> TcCoercionN -> TcCoercionN
mkFunCo Role
Nominal TcCoercionN
co_w TcCoercionN
co_l TcCoercionN
co_r }
go ty1 :: TcSigmaType
ty1@(TyConApp TyCon
tc1 ThetaType
_) TcSigmaType
ty2
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1 = TcSigmaType -> TcSigmaType -> TcM TcCoercionN
defer TcSigmaType
ty1 TcSigmaType
ty2
go TcSigmaType
ty1 ty2 :: TcSigmaType
ty2@(TyConApp TyCon
tc2 ThetaType
_)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2 = TcSigmaType -> TcSigmaType -> TcM TcCoercionN
defer TcSigmaType
ty1 TcSigmaType
ty2
go (TyConApp TyCon
tc1 ThetaType
tys1) (TyConApp TyCon
tc2 ThetaType
tys2)
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2, ThetaType -> ThetaType -> Bool
forall a b. [a] -> [b] -> Bool
equalLength ThetaType
tys1 ThetaType
tys2
= ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 )
do { [TcCoercionN]
cos <- (CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> [CtOrigin]
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) [TcCoercionN]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M (TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k) [CtOrigin]
origins' ThetaType
tys1 ThetaType
tys2
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> TcM TcCoercionN) -> TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> TyCon -> [TcCoercionN] -> TcCoercionN
Role -> TyCon -> [TcCoercionN] -> TcCoercionN
mkTyConAppCo Role
Nominal TyCon
tc1 [TcCoercionN]
cos }
where
origins' :: [CtOrigin]
origins' = (Bool -> CtOrigin) -> [Bool] -> [CtOrigin]
forall a b. (a -> b) -> [a] -> [b]
map (\Bool
is_vis -> if Bool
is_vis then CtOrigin
origin else CtOrigin -> CtOrigin
toInvisibleOrigin CtOrigin
origin)
(TyCon -> [Bool]
tcTyConVisibilities TyCon
tc1)
go (LitTy TyLit
m) ty :: TcSigmaType
ty@(LitTy TyLit
n)
| TyLit
m TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
n
= TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> TcM TcCoercionN) -> TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$ TcSigmaType -> TcCoercionN
mkNomReflCo TcSigmaType
ty
go (AppTy TcSigmaType
s1 TcSigmaType
t1) (AppTy TcSigmaType
s2 TcSigmaType
t2)
= Bool
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcM TcCoercionN
go_app (TcSigmaType -> Bool
isNextArgVisible TcSigmaType
s1) TcSigmaType
s1 TcSigmaType
t1 TcSigmaType
s2 TcSigmaType
t2
go (AppTy TcSigmaType
s1 TcSigmaType
t1) (TyConApp TyCon
tc2 ThetaType
ts2)
| Just (ThetaType
ts2', TcSigmaType
t2') <- ThetaType -> Maybe (ThetaType, TcSigmaType)
forall a. [a] -> Maybe ([a], a)
snocView ThetaType
ts2
= ASSERT( not (mustBeSaturated tc2) )
Bool
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcM TcCoercionN
go_app (TyCon -> ThetaType -> Bool
isNextTyConArgVisible TyCon
tc2 ThetaType
ts2') TcSigmaType
s1 TcSigmaType
t1 (TyCon -> ThetaType -> TcSigmaType
TyConApp TyCon
tc2 ThetaType
ts2') TcSigmaType
t2'
go (TyConApp TyCon
tc1 ThetaType
ts1) (AppTy TcSigmaType
s2 TcSigmaType
t2)
| Just (ThetaType
ts1', TcSigmaType
t1') <- ThetaType -> Maybe (ThetaType, TcSigmaType)
forall a. [a] -> Maybe ([a], a)
snocView ThetaType
ts1
= ASSERT( not (mustBeSaturated tc1) )
Bool
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcM TcCoercionN
go_app (TyCon -> ThetaType -> Bool
isNextTyConArgVisible TyCon
tc1 ThetaType
ts1') (TyCon -> ThetaType -> TcSigmaType
TyConApp TyCon
tc1 ThetaType
ts1') TcSigmaType
t1' TcSigmaType
s2 TcSigmaType
t2
go (CoercionTy TcCoercionN
co1) (CoercionTy TcCoercionN
co2)
= do { let ty1 :: TcSigmaType
ty1 = TcCoercionN -> TcSigmaType
coercionType TcCoercionN
co1
ty2 :: TcSigmaType
ty2 = TcCoercionN -> TcSigmaType
coercionType TcCoercionN
co2
; TcCoercionN
kco <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
KindLevel
(TcSigmaType
-> Maybe TcSigmaType -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin TcSigmaType
orig_ty1 (TcSigmaType -> Maybe TcSigmaType
forall a. a -> Maybe a
Just TcSigmaType
orig_ty2) CtOrigin
origin
(TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
t_or_k))
TcSigmaType
ty1 TcSigmaType
ty2
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> TcM TcCoercionN) -> TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$ Role -> TcCoercionN -> TcCoercionN -> TcCoercionN -> TcCoercionN
mkProofIrrelCo Role
Nominal TcCoercionN
kco TcCoercionN
co1 TcCoercionN
co2 }
go TcSigmaType
ty1 TcSigmaType
ty2 = TcSigmaType -> TcSigmaType -> TcM TcCoercionN
defer TcSigmaType
ty1 TcSigmaType
ty2
defer :: TcSigmaType -> TcSigmaType -> TcM TcCoercionN
defer TcSigmaType
ty1 TcSigmaType
ty2
| TcSigmaType
ty1 HasDebugCallStack => TcSigmaType -> TcSigmaType -> Bool
TcSigmaType -> TcSigmaType -> Bool
`tcEqType` TcSigmaType
ty2 = TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkNomReflCo TcSigmaType
ty1)
| Bool
otherwise = TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType_defer TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
ty1 TcSigmaType
ty2
go_app :: Bool
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcSigmaType
-> TcM TcCoercionN
go_app Bool
vis TcSigmaType
s1 TcSigmaType
t1 TcSigmaType
s2 TcSigmaType
t2
= do { TcCoercionN
co_s <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
origin TcSigmaType
s1 TcSigmaType
s2
; let arg_origin :: CtOrigin
arg_origin
| Bool
vis = CtOrigin
origin
| Bool
otherwise = CtOrigin -> CtOrigin
toInvisibleOrigin CtOrigin
origin
; TcCoercionN
co_t <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
t_or_k CtOrigin
arg_origin TcSigmaType
t1 TcSigmaType
t2
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcCoercionN -> TcM TcCoercionN) -> TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$ TcCoercionN -> TcCoercionN -> TcCoercionN
mkAppCo TcCoercionN
co_s TcCoercionN
co_t }
uUnfilledVar :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM Coercion
uUnfilledVar :: CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped Var
tv1 TcSigmaType
ty2
= do { TcSigmaType
ty2 <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
ty2
; CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar1 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped Var
tv1 TcSigmaType
ty2 }
uUnfilledVar1 :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM Coercion
uUnfilledVar1 :: CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar1 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped Var
tv1 TcSigmaType
ty2
| Just Var
tv2 <- TcSigmaType -> Maybe Var
tcGetTyVar_maybe TcSigmaType
ty2
= Var -> TcM TcCoercionN
go Var
tv2
| Bool
otherwise
= CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped Var
tv1 TcSigmaType
ty2
where
go :: Var -> TcM TcCoercionN
go Var
tv2 | Var
tv1 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
tv2
= TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkNomReflCo (Var -> TcSigmaType
mkTyVarTy Var
tv1))
| Bool -> Var -> Var -> Bool
swapOverTyVars Bool
False Var
tv1 Var
tv2
= do { Var
tv1 <- Var -> TcM Var
zonkTyCoVarKind Var
tv1
; CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k (SwapFlag -> SwapFlag
flipSwap SwapFlag
swapped)
Var
tv2 (Var -> TcSigmaType
mkTyVarTy Var
tv1) }
| Bool
otherwise
= CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped Var
tv1 TcSigmaType
ty2
uUnfilledVar2 :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM Coercion
uUnfilledVar2 :: CtOrigin
-> TypeOrKind -> SwapFlag -> Var -> TcSigmaType -> TcM TcCoercionN
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped Var
tv1 TcSigmaType
ty2
= do { DynFlags
dflags <- IOEnv (Env TcGblEnv TcLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
; TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; DynFlags -> TcLevel -> TcM TcCoercionN
go DynFlags
dflags TcLevel
cur_lvl }
where
go :: DynFlags -> TcLevel -> TcM TcCoercionN
go DynFlags
dflags TcLevel
cur_lvl
| TcLevel -> Var -> TcSigmaType -> Bool
canSolveByUnification TcLevel
cur_lvl Var
tv1 TcSigmaType
ty2
, MTVU_OK TcSigmaType
ty2' <- DynFlags -> Var -> TcSigmaType -> MetaTyVarUpdateResult TcSigmaType
metaTyVarUpdateOK DynFlags
dflags Var
tv1 TcSigmaType
ty2
= do { TcCoercionN
co_k <- TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
KindLevel CtOrigin
kind_origin (HasDebugCallStack => TcSigmaType -> TcSigmaType
TcSigmaType -> TcSigmaType
tcTypeKind TcSigmaType
ty2') (Var -> TcSigmaType
tyVarKind Var
tv1)
; String -> SDoc -> TcRn ()
traceTc String
"uUnfilledVar2 ok" (SDoc -> TcRn ()) -> SDoc -> TcRn ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv1 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> TcSigmaType
tyVarKind Var
tv1)
, TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => TcSigmaType -> TcSigmaType
TcSigmaType -> TcSigmaType
tcTypeKind TcSigmaType
ty2)
, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcCoercionN -> Bool
isTcReflCo TcCoercionN
co_k), TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co_k ]
; if TcCoercionN -> Bool
isTcReflCo TcCoercionN
co_k
then do { Var -> TcSigmaType -> TcRn ()
writeMetaTyVar Var
tv1 TcSigmaType
ty2'
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkTcNomReflCo TcSigmaType
ty2') }
else TcM TcCoercionN
defer }
| Bool
otherwise
= do { String -> SDoc -> TcRn ()
traceTc String
"uUnfilledVar2 not ok" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv1 SDoc -> SDoc -> SDoc
$$ TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2)
; TcM TcCoercionN
defer }
ty1 :: TcSigmaType
ty1 = Var -> TcSigmaType
mkTyVarTy Var
tv1
kind_origin :: CtOrigin
kind_origin = TcSigmaType
-> Maybe TcSigmaType -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin TcSigmaType
ty1 (TcSigmaType -> Maybe TcSigmaType
forall a. a -> Maybe a
Just TcSigmaType
ty2) CtOrigin
origin (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
t_or_k)
defer :: TcM TcCoercionN
defer = SwapFlag
-> (TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> TcSigmaType
-> TcSigmaType
-> TcM TcCoercionN
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped (TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType_defer TypeOrKind
t_or_k CtOrigin
origin) TcSigmaType
ty1 TcSigmaType
ty2
swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars :: Bool -> Var -> Var -> Bool
swapOverTyVars Bool
is_given Var
tv1 Var
tv2
| Bool -> Bool
not Bool
is_given, Arity
pri1 Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
0, Arity
pri2 Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
> Arity
0 = Bool
True
| Bool -> Bool
not Bool
is_given, Arity
pri2 Arity -> Arity -> Bool
forall a. Eq a => a -> a -> Bool
== Arity
0, Arity
pri1 Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
> Arity
0 = Bool
False
| TcLevel
lvl1 TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl2 = Bool
False
| TcLevel
lvl2 TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl1 = Bool
True
| Arity
pri1 Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
> Arity
pri2 = Bool
False
| Arity
pri2 Arity -> Arity -> Bool
forall a. Ord a => a -> a -> Bool
> Arity
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 = Var -> TcLevel
tcTyVarLevel Var
tv1
lvl2 :: TcLevel
lvl2 = Var -> TcLevel
tcTyVarLevel Var
tv2
pri1 :: Arity
pri1 = Var -> Arity
lhsPriority Var
tv1
pri2 :: Arity
pri2 = Var -> Arity
lhsPriority Var
tv2
tv1_name :: Name
tv1_name = Var -> Name
Var.varName Var
tv1
tv2_name :: Name
tv2_name = Var -> Name
Var.varName Var
tv2
lhsPriority :: TcTyVar -> Int
lhsPriority :: Var -> Arity
lhsPriority Var
tv
= ASSERT2( isTyVar tv, ppr tv)
case Var -> TcTyVarDetails
tcTyVarDetails Var
tv of
TcTyVarDetails
RuntimeUnk -> Arity
0
SkolemTv {} -> Arity
0
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } -> case MetaInfo
info of
MetaInfo
FlatSkolTv -> Arity
1
MetaInfo
TyVarTv -> Arity
2
MetaInfo
TauTv -> Arity
3
MetaInfo
FlatMetaTv -> Arity
4
MetaInfo
RuntimeUnkTv -> Arity
5
canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool
canSolveByUnification :: TcLevel -> Var -> TcSigmaType -> Bool
canSolveByUnification TcLevel
tclvl Var
tv TcSigmaType
xi
| TcLevel -> Var -> Bool
isTouchableMetaTyVar TcLevel
tclvl Var
tv
= case Var -> MetaInfo
metaTyVarInfo Var
tv of
MetaInfo
TyVarTv -> TcSigmaType -> Bool
is_tyvar TcSigmaType
xi
MetaInfo
_ -> Bool
True
| Bool
otherwise
= Bool
False
where
is_tyvar :: TcSigmaType -> Bool
is_tyvar TcSigmaType
xi
= case TcSigmaType -> Maybe Var
tcGetTyVar_maybe TcSigmaType
xi of
Maybe Var
Nothing -> Bool
False
Just Var
tv -> case Var -> TcTyVarDetails
tcTyVarDetails Var
tv of
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info }
-> case MetaInfo
info of
MetaInfo
TyVarTv -> Bool
True
MetaInfo
_ -> Bool
False
SkolemTv {} -> Bool
True
TcTyVarDetails
RuntimeUnk -> Bool
True
data LookupTyVarResult
= Unfilled TcTyVarDetails
| Filled TcType
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
lookupTcTyVar :: Var -> TcM LookupTyVarResult
lookupTcTyVar Var
tyvar
| MetaTv { mtv_ref :: TcTyVarDetails -> IORef MetaDetails
mtv_ref = IORef MetaDetails
ref } <- TcTyVarDetails
details
= do { MetaDetails
meta_details <- IORef MetaDetails -> TcM MetaDetails
forall a env. IORef a -> IOEnv env a
readMutVar IORef MetaDetails
ref
; case MetaDetails
meta_details of
Indirect TcSigmaType
ty -> LookupTyVarResult -> TcM LookupTyVarResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> LookupTyVarResult
Filled TcSigmaType
ty)
MetaDetails
Flexi -> do { Bool
is_touchable <- Var -> TcM Bool
isTouchableTcM Var
tyvar
; if Bool
is_touchable then
LookupTyVarResult -> TcM LookupTyVarResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVarDetails -> LookupTyVarResult
Unfilled TcTyVarDetails
details)
else
LookupTyVarResult -> TcM LookupTyVarResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVarDetails -> LookupTyVarResult
Unfilled TcTyVarDetails
vanillaSkolemTv) } }
| Bool
otherwise
= LookupTyVarResult -> TcM LookupTyVarResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcTyVarDetails -> LookupTyVarResult
Unfilled TcTyVarDetails
details)
where
details :: TcTyVarDetails
details = Var -> TcTyVarDetails
tcTyVarDetails Var
tyvar
matchExpectedFunKind
:: Outputable fun
=> fun
-> Arity
-> TcKind
-> TcM Coercion
matchExpectedFunKind :: fun -> Arity -> TcSigmaType -> TcM TcCoercionN
matchExpectedFunKind fun
hs_ty Arity
n TcSigmaType
k = Arity -> TcSigmaType -> TcM TcCoercionN
go Arity
n TcSigmaType
k
where
go :: Arity -> TcSigmaType -> TcM TcCoercionN
go Arity
0 TcSigmaType
k = TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkNomReflCo TcSigmaType
k)
go Arity
n TcSigmaType
k | Just TcSigmaType
k' <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
k = Arity -> TcSigmaType -> TcM TcCoercionN
go Arity
n TcSigmaType
k'
go Arity
n k :: TcSigmaType
k@(TyVarTy Var
kvar)
| Var -> Bool
isMetaTyVar Var
kvar
= do { MetaDetails
maybe_kind <- Var -> TcM MetaDetails
readMetaTyVar Var
kvar
; case MetaDetails
maybe_kind of
Indirect TcSigmaType
fun_kind -> Arity -> TcSigmaType -> TcM TcCoercionN
go Arity
n TcSigmaType
fun_kind
MetaDetails
Flexi -> Arity -> TcSigmaType -> TcM TcCoercionN
defer Arity
n TcSigmaType
k }
go Arity
n (FunTy { ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
w, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res })
= do { TcCoercionN
co <- Arity -> TcSigmaType -> TcM TcCoercionN
go (Arity
nArity -> Arity -> Arity
forall a. Num a => a -> a -> a
-Arity
1) TcSigmaType
res
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> TcCoercionN -> TcCoercionN -> TcCoercionN -> TcCoercionN
mkTcFunCo Role
Nominal (TcSigmaType -> TcCoercionN
mkTcNomReflCo TcSigmaType
w) (TcSigmaType -> TcCoercionN
mkTcNomReflCo TcSigmaType
arg) TcCoercionN
co) }
go Arity
n TcSigmaType
other
= Arity -> TcSigmaType -> TcM TcCoercionN
defer Arity
n TcSigmaType
other
defer :: Arity -> TcSigmaType -> TcM TcCoercionN
defer Arity
n TcSigmaType
k
= do { ThetaType
arg_kinds <- Arity -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
newMetaKindVars Arity
n
; TcSigmaType
res_kind <- TcM TcSigmaType
newMetaKindVar
; let new_fun :: TcSigmaType
new_fun = ThetaType -> TcSigmaType -> TcSigmaType
mkVisFunTysMany ThetaType
arg_kinds TcSigmaType
res_kind
origin :: CtOrigin
origin = TypeEqOrigin :: TcSigmaType -> TcSigmaType -> Maybe SDoc -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
k
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
new_fun
, uo_thing :: Maybe SDoc
uo_thing = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (fun -> SDoc
forall a. Outputable a => a -> SDoc
ppr fun
hs_ty)
, uo_visible :: Bool
uo_visible = Bool
True
}
; TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
KindLevel CtOrigin
origin TcSigmaType
k TcSigmaType
new_fun }
data MetaTyVarUpdateResult a
= MTVU_OK a
| MTVU_Bad
| MTVU_HoleBlocker
| MTVU_Occurs
deriving (a -> MetaTyVarUpdateResult b -> MetaTyVarUpdateResult a
(a -> b) -> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b
(forall a b.
(a -> b) -> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b)
-> (forall a b.
a -> MetaTyVarUpdateResult b -> MetaTyVarUpdateResult a)
-> Functor MetaTyVarUpdateResult
forall a b. a -> MetaTyVarUpdateResult b -> MetaTyVarUpdateResult a
forall a b.
(a -> b) -> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> MetaTyVarUpdateResult b -> MetaTyVarUpdateResult a
$c<$ :: forall a b. a -> MetaTyVarUpdateResult b -> MetaTyVarUpdateResult a
fmap :: (a -> b) -> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b
$cfmap :: forall a b.
(a -> b) -> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b
Functor)
instance Applicative MetaTyVarUpdateResult where
pure :: a -> MetaTyVarUpdateResult a
pure = a -> MetaTyVarUpdateResult a
forall a. a -> MetaTyVarUpdateResult a
MTVU_OK
<*> :: MetaTyVarUpdateResult (a -> b)
-> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b
(<*>) = MetaTyVarUpdateResult (a -> b)
-> MetaTyVarUpdateResult a -> MetaTyVarUpdateResult b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Monad MetaTyVarUpdateResult where
MTVU_OK a
x >>= :: MetaTyVarUpdateResult a
-> (a -> MetaTyVarUpdateResult b) -> MetaTyVarUpdateResult b
>>= a -> MetaTyVarUpdateResult b
k = a -> MetaTyVarUpdateResult b
k a
x
MetaTyVarUpdateResult a
MTVU_Bad >>= a -> MetaTyVarUpdateResult b
_ = MetaTyVarUpdateResult b
forall a. MetaTyVarUpdateResult a
MTVU_Bad
MetaTyVarUpdateResult a
MTVU_HoleBlocker >>= a -> MetaTyVarUpdateResult b
_ = MetaTyVarUpdateResult b
forall a. MetaTyVarUpdateResult a
MTVU_HoleBlocker
MetaTyVarUpdateResult a
MTVU_Occurs >>= a -> MetaTyVarUpdateResult b
_ = MetaTyVarUpdateResult b
forall a. MetaTyVarUpdateResult a
MTVU_Occurs
instance Outputable a => Outputable (MetaTyVarUpdateResult a) where
ppr :: MetaTyVarUpdateResult a -> SDoc
ppr (MTVU_OK a
a) = String -> SDoc
text String
"MTVU_OK" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
a
ppr MetaTyVarUpdateResult a
MTVU_Bad = String -> SDoc
text String
"MTVU_Bad"
ppr MetaTyVarUpdateResult a
MTVU_HoleBlocker = String -> SDoc
text String
"MTVU_HoleBlocker"
ppr MetaTyVarUpdateResult a
MTVU_Occurs = String -> SDoc
text String
"MTVU_Occurs"
occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
occCheckForErrors :: DynFlags -> Var -> TcSigmaType -> MetaTyVarUpdateResult ()
occCheckForErrors DynFlags
dflags Var
tv TcSigmaType
ty
= case DynFlags -> Bool -> Var -> TcSigmaType -> MetaTyVarUpdateResult ()
mtvu_check DynFlags
dflags Bool
True Var
tv TcSigmaType
ty of
MTVU_OK ()
_ -> () -> MetaTyVarUpdateResult ()
forall a. a -> MetaTyVarUpdateResult a
MTVU_OK ()
MetaTyVarUpdateResult ()
MTVU_Bad -> MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Bad
MetaTyVarUpdateResult ()
MTVU_HoleBlocker -> MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_HoleBlocker
MetaTyVarUpdateResult ()
MTVU_Occurs -> case [Var] -> TcSigmaType -> Maybe TcSigmaType
occCheckExpand [Var
tv] TcSigmaType
ty of
Maybe TcSigmaType
Nothing -> MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Occurs
Just TcSigmaType
_ -> () -> MetaTyVarUpdateResult ()
forall a. a -> MetaTyVarUpdateResult a
MTVU_OK ()
metaTyVarUpdateOK :: DynFlags
-> TcTyVar
-> TcType
-> MetaTyVarUpdateResult TcType
metaTyVarUpdateOK :: DynFlags -> Var -> TcSigmaType -> MetaTyVarUpdateResult TcSigmaType
metaTyVarUpdateOK DynFlags
dflags Var
tv TcSigmaType
ty
= case DynFlags -> Bool -> Var -> TcSigmaType -> MetaTyVarUpdateResult ()
mtvu_check DynFlags
dflags Bool
False Var
tv TcSigmaType
ty of
MTVU_OK ()
_ -> TcSigmaType -> MetaTyVarUpdateResult TcSigmaType
forall a. a -> MetaTyVarUpdateResult a
MTVU_OK TcSigmaType
ty
MetaTyVarUpdateResult ()
MTVU_Bad -> MetaTyVarUpdateResult TcSigmaType
forall a. MetaTyVarUpdateResult a
MTVU_Bad
MetaTyVarUpdateResult ()
MTVU_HoleBlocker -> MetaTyVarUpdateResult TcSigmaType
forall a. MetaTyVarUpdateResult a
MTVU_HoleBlocker
MetaTyVarUpdateResult ()
MTVU_Occurs -> case [Var] -> TcSigmaType -> Maybe TcSigmaType
occCheckExpand [Var
tv] TcSigmaType
ty of
Just TcSigmaType
expanded_ty -> TcSigmaType -> MetaTyVarUpdateResult TcSigmaType
forall a. a -> MetaTyVarUpdateResult a
MTVU_OK TcSigmaType
expanded_ty
Maybe TcSigmaType
Nothing -> MetaTyVarUpdateResult TcSigmaType
forall a. MetaTyVarUpdateResult a
MTVU_Occurs
mtvu_check :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
mtvu_check :: DynFlags -> Bool -> Var -> TcSigmaType -> MetaTyVarUpdateResult ()
mtvu_check DynFlags
dflags Bool
ty_fam_ok Var
tv TcSigmaType
ty
= TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
ty
where
ok :: MetaTyVarUpdateResult ()
ok :: MetaTyVarUpdateResult ()
ok = () -> MetaTyVarUpdateResult ()
forall a. a -> MetaTyVarUpdateResult a
MTVU_OK ()
ghci_tv :: Bool
ghci_tv = case Var -> TcTyVarDetails
tcTyVarDetails Var
tv of
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
RuntimeUnkTv } -> Bool
True
TcTyVarDetails
_ -> Bool
False
fast_check :: TcType -> MetaTyVarUpdateResult ()
fast_check :: TcSigmaType -> MetaTyVarUpdateResult ()
fast_check (TyVarTy Var
tv')
| Var
tv Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
tv' = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Occurs
| Bool
otherwise = TcSigmaType -> MetaTyVarUpdateResult ()
fast_check_occ (Var -> TcSigmaType
tyVarKind Var
tv')
fast_check (TyConApp TyCon
tc ThetaType
tys)
| TyCon -> Bool
bad_tc TyCon
tc, Bool -> Bool
not Bool
ghci_tv = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Bad
| Bool
otherwise = (TcSigmaType -> MetaTyVarUpdateResult ())
-> ThetaType -> MetaTyVarUpdateResult [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TcSigmaType -> MetaTyVarUpdateResult ()
fast_check ThetaType
tys MetaTyVarUpdateResult [()]
-> MetaTyVarUpdateResult () -> MetaTyVarUpdateResult ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MetaTyVarUpdateResult ()
ok
fast_check (LitTy {}) = MetaTyVarUpdateResult ()
ok
fast_check (FunTy{ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
w, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
a, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
r})
| AnonArgFlag
InvisArg <- AnonArgFlag
af
, Bool -> Bool
not Bool
ghci_tv = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Bad
| Bool
otherwise = TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
w MetaTyVarUpdateResult ()
-> MetaTyVarUpdateResult () -> MetaTyVarUpdateResult ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
a MetaTyVarUpdateResult ()
-> MetaTyVarUpdateResult () -> MetaTyVarUpdateResult ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
r
fast_check (AppTy TcSigmaType
fun TcSigmaType
arg) = TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
fun MetaTyVarUpdateResult ()
-> MetaTyVarUpdateResult () -> MetaTyVarUpdateResult ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
arg
fast_check (CastTy TcSigmaType
ty TcCoercionN
co) = TcSigmaType -> MetaTyVarUpdateResult ()
fast_check TcSigmaType
ty MetaTyVarUpdateResult ()
-> MetaTyVarUpdateResult () -> MetaTyVarUpdateResult ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TcCoercionN -> MetaTyVarUpdateResult ()
fast_check_co TcCoercionN
co
fast_check (CoercionTy TcCoercionN
co) = TcCoercionN -> MetaTyVarUpdateResult ()
fast_check_co TcCoercionN
co
fast_check (ForAllTy (Bndr Var
tv' ArgFlag
_) TcSigmaType
ty)
| Bool -> Bool
not Bool
ghci_tv = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Bad
| Var
tv Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
tv' = MetaTyVarUpdateResult ()
ok
| Bool
otherwise = do { TcSigmaType -> MetaTyVarUpdateResult ()
fast_check_occ (Var -> TcSigmaType
tyVarKind Var
tv')
; TcSigmaType -> MetaTyVarUpdateResult ()
fast_check_occ TcSigmaType
ty }
fast_check_occ :: TcSigmaType -> MetaTyVarUpdateResult ()
fast_check_occ TcSigmaType
k | Var
tv Var -> VarSet -> Bool
`elemVarSet` TcSigmaType -> VarSet
tyCoVarsOfType TcSigmaType
k = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Occurs
| Bool
otherwise = MetaTyVarUpdateResult ()
ok
fast_check_co :: TcCoercionN -> MetaTyVarUpdateResult ()
fast_check_co TcCoercionN
co | Bool -> Bool
not (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DeferTypeErrors DynFlags
dflags)
, TcCoercionN -> Bool
badCoercionHoleCo TcCoercionN
co = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_HoleBlocker
| Var
tv Var -> VarSet -> Bool
`elemVarSet` TcCoercionN -> VarSet
tyCoVarsOfCo TcCoercionN
co = MetaTyVarUpdateResult ()
forall a. MetaTyVarUpdateResult a
MTVU_Occurs
| Bool
otherwise = MetaTyVarUpdateResult ()
ok
bad_tc :: TyCon -> Bool
bad_tc :: TyCon -> Bool
bad_tc TyCon
tc
| Bool -> Bool
not (TyCon -> Bool
isTauTyCon TyCon
tc) = Bool
True
| Bool -> Bool
not (Bool
ty_fam_ok Bool -> Bool -> Bool
|| TyCon -> Bool
isFamFreeTyCon TyCon
tc) = Bool
True
| Bool
otherwise = Bool
False