{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
{-# 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, unifyExpectedType,
uType, promoteTcType,
swapOverTyVars, startSolvingByUnification,
tcInfer,
matchExpectedListTy,
matchExpectedTyConApp,
matchExpectedAppTy,
matchExpectedFunTys,
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
checkTyVarEq, checkTyFamEq, checkTypeEq
) where
import GHC.Prelude
import GHC.Hs
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr( debugPprType )
import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, makeTypeConcrete, 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.Core.Type
import GHC.Core.Coercion
import GHC.Core.Multiplicity
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Types.Name( isSystemName )
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 GHC.Utils.Panic.Plain
import GHC.Exts ( inline )
import Control.Monad
import Control.Arrow ( second )
import qualified Data.Semigroup as S ( (<>) )
matchActualFunTySigma
:: ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Arity, [Scaled TcSigmaType])
-> TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
matchActualFunTySigma :: ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Arity, [Scaled TcSigmaType])
-> TcSigmaType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma ExpectedFunTyOrigin
herald Maybe TypedThing
mb_thing (Arity, [Scaled TcSigmaType])
err_info TcSigmaType
fun_ty
= Bool
-> SDoc
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcSigmaType -> Bool
isRhoTy TcSigmaType
fun_ty) (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_ty) (TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType))
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
TcSigmaType -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
go TcSigmaType
fun_ty
where
go :: TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, 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 })
= Bool
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall a. HasCallStack => Bool -> a -> a
assert (AnonArgFlag
af AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
VisArg) (TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType))
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
do { HasDebugCallStack =>
FixedRuntimeRepContext -> TcSigmaType -> TcM ()
FixedRuntimeRepContext -> TcSigmaType -> TcM ()
hasFixedRuntimeRep_syntactic (ExpectedFunTyOrigin -> Arity -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Arity
1) TcSigmaType
arg_ty
; (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
; TcSigmaType
mult <- TcSigmaType -> TcM TcSigmaType
newFlexiTyVarTy TcSigmaType
multiplicityTy
; let unif_fun_ty :: TcSigmaType
unif_fun_ty = TcSigmaType -> TcSigmaType -> TcSigmaType -> TcSigmaType
mkVisFunTy TcSigmaType
mult TcSigmaType
arg_ty TcSigmaType
res_ty
; TcCoercionN
co <- Maybe TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
mb_thing TcSigmaType
fun_ty TcSigmaType
unif_fun_ty
; HasDebugCallStack =>
FixedRuntimeRepContext -> TcSigmaType -> TcM ()
FixedRuntimeRepContext -> TcSigmaType -> TcM ()
hasFixedRuntimeRep_syntactic (ExpectedFunTyOrigin -> Arity -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Arity
1) TcSigmaType
arg_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 -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
mult TcSigmaType
arg_ty, TcSigmaType
res_ty) }
mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt :: TcSigmaType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt TcSigmaType
res_ty TidyEnv
env = TidyEnv
-> ExpectedFunTyOrigin
-> [Scaled TcSigmaType]
-> TcSigmaType
-> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env ExpectedFunTyOrigin
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 :: ExpectedFunTyOrigin
-> CtOrigin
-> Maybe TypedThing
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
matchActualFunTysRho :: ExpectedFunTyOrigin
-> CtOrigin
-> Maybe TypedThing
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaType], TcSigmaType)
matchActualFunTysRho ExpectedFunTyOrigin
herald CtOrigin
ct_orig Maybe TypedThing
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) <- ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Arity, [Scaled TcSigmaType])
-> TcSigmaType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma
ExpectedFunTyOrigin
herald Maybe TypedThing
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 -> HsWrapper
mkWpFun HsWrapper
idHsWrapper HsWrapper
wrap_res Scaled TcSigmaType
arg_ty1 TcSigmaType
res_ty
; (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) }
matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin
-> UserTypeCtxt
-> Arity
-> ExpRhoType
-> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys :: ExpectedFunTyOrigin
-> UserTypeCtxt
-> Arity
-> ExpRhoType
-> ([Scaled ExpRhoType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys ExpectedFunTyOrigin
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 })
= Bool -> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. HasCallStack => Bool -> a -> a
assert (AnonArgFlag
af AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
VisArg) (TcM (HsWrapper, a) -> TcM (HsWrapper, a))
-> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$
do { let arg_pos :: Arity
arg_pos = Arity
1 Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
+ [Scaled ExpRhoType] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Scaled ExpRhoType]
acc_arg_tys
; (TcCoercionN
arg_co, TcSigmaType
arg_ty) <- HasDebugCallStack =>
FixedRuntimeRepContext
-> TcSigmaType -> TcM (TcCoercionN, TcSigmaType)
FixedRuntimeRepContext
-> TcSigmaType -> TcM (TcCoercionN, TcSigmaType)
hasFixedRuntimeRep (ExpectedFunTyOrigin -> Arity -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Arity
arg_pos) TcSigmaType
arg_ty
; (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 wrap_arg :: HsWrapper
wrap_arg = TcCoercionN -> HsWrapper
mkWpCastN TcCoercionN
arg_co
fun_wrap :: HsWrapper
fun_wrap = HsWrapper
-> HsWrapper -> Scaled TcSigmaType -> TcSigmaType -> HsWrapper
mkWpFun HsWrapper
wrap_arg HsWrapper
wrap_res (TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
mult TcSigmaType
arg_ty) TcSigmaType
res_ty
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
fun_wrap, a
result) }
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 ExpSigmaTypeFRR] -> 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 { let last_acc_arg_pos :: Arity
last_acc_arg_pos = [Scaled ExpRhoType] -> Arity
forall (t :: * -> *) a. Foldable t => t a -> Arity
length [Scaled ExpRhoType]
acc_arg_tys
; [Scaled ExpRhoType]
more_arg_tys <- (Arity -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType))
-> [Arity] -> IOEnv (Env TcGblEnv TcLclEnv) [Scaled ExpRhoType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arity -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
new_exp_arg_ty [Arity
last_acc_arg_pos Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
+ Arity
1 .. Arity
last_acc_arg_pos Arity -> Arity -> Arity
forall a. Num a => a -> a -> a
+ Arity
n]
; ExpRhoType
res_ty <- TcM 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]
++ [Scaled ExpRhoType]
more_arg_tys) ExpRhoType
res_ty
; [Scaled TcSigmaType]
more_arg_tys <- (Scaled ExpRhoType
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcSigmaType))
-> [Scaled ExpRhoType]
-> IOEnv (Env TcGblEnv TcLclEnv) [Scaled TcSigmaType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(Scaled TcSigmaType
m ExpRhoType
t) -> TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
m (TcSigmaType -> Scaled TcSigmaType)
-> TcM TcSigmaType
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled TcSigmaType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpRhoType -> TcM TcSigmaType
readExpType ExpRhoType
t) [Scaled ExpRhoType]
more_arg_tys
; TcSigmaType
res_ty <- ExpRhoType -> TcM TcSigmaType
readExpType ExpRhoType
res_ty
; let unif_fun_ty :: TcSigmaType
unif_fun_ty = [Scaled TcSigmaType] -> TcSigmaType -> TcSigmaType
mkVisFunTys [Scaled TcSigmaType]
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) }
new_exp_arg_ty :: Int -> TcM (Scaled ExpSigmaTypeFRR)
new_exp_arg_ty :: Arity -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
new_exp_arg_ty Arity
arg_pos
= TcSigmaType -> ExpRhoType -> Scaled ExpRhoType
forall a. TcSigmaType -> a -> Scaled a
mkScaled (TcSigmaType -> ExpRhoType -> Scaled ExpRhoType)
-> TcM TcSigmaType
-> IOEnv (Env TcGblEnv TcLclEnv) (ExpRhoType -> Scaled ExpRhoType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcSigmaType -> TcM TcSigmaType
newFlexiTyVarTy TcSigmaType
multiplicityTy
IOEnv (Env TcGblEnv TcLclEnv) (ExpRhoType -> Scaled ExpRhoType)
-> TcM ExpRhoType
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FixedRuntimeRepContext -> TcM ExpRhoType
newInferExpTypeFRR (ExpectedFunTyOrigin -> Arity -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Arity
arg_pos)
mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt :: [Scaled ExpRhoType]
-> TcSigmaType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt [Scaled ExpRhoType]
arg_tys TcSigmaType
res_ty TidyEnv
env
= TidyEnv
-> ExpectedFunTyOrigin
-> [Scaled TcSigmaType]
-> TcSigmaType
-> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env ExpectedFunTyOrigin
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
-> ExpectedFunTyOrigin
-> [Scaled TcType] -> TcType -> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg :: TidyEnv
-> ExpectedFunTyOrigin
-> [Scaled TcSigmaType]
-> TcSigmaType
-> Arity
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env ExpectedFunTyOrigin
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 = ExpectedFunTyOrigin -> SDoc
pprExpectedFunTyHerald ExpectedFunTyOrigin
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
= Bool
-> TcM (TcCoercionN, ThetaType) -> TcM (TcCoercionN, ThetaType)
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyCon -> Bool
isFunTyCon TyCon
tc) (TcM (TcCoercionN, ThetaType) -> TcM (TcCoercionN, ThetaType))
-> TcM (TcCoercionN, ThetaType) -> TcM (TcCoercionN, ThetaType)
forall a b. (a -> b) -> a -> b
$ TcSigmaType -> TcM (TcCoercionN, ThetaType)
go TcSigmaType
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 -> TcM ()
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 TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
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 TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
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
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
fillInferResult :: TcSigmaType -> InferResult -> TcM TcCoercionN
fillInferResult TcSigmaType
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 TcSigmaType)
ir_ref = IORef (Maybe TcSigmaType)
ref })
= do { Maybe TcSigmaType
mb_exp_res_ty <- IORef (Maybe TcSigmaType)
-> TcRnIf TcGblEnv TcLclEnv (Maybe TcSigmaType)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe TcSigmaType)
ref
; case Maybe TcSigmaType
mb_exp_res_ty of
Just TcSigmaType
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
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
act_res_ty SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
exp_res_ty
; TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TcLevel
cur_lvl TcLevel -> TcLevel -> Bool
`sameDepthAs` TcLevel
res_lvl) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
TcSigmaType -> TcM ()
ensureMonoType TcSigmaType
act_res_ty
; Maybe TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
forall a. Maybe a
Nothing TcSigmaType
act_res_ty TcSigmaType
exp_res_ty }
Maybe TcSigmaType
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
<+> String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
act_res_ty
; (TcCoercionN
prom_co, TcSigmaType
act_res_ty) <- TcLevel -> TcSigmaType -> TcM (TcCoercionN, TcSigmaType)
promoteTcType TcLevel
res_lvl TcSigmaType
act_res_ty
; (TcCoercionN
frr_co, TcSigmaType
act_res_ty) <-
case Maybe FixedRuntimeRepContext
mb_frr of
Maybe FixedRuntimeRepContext
Nothing -> (TcCoercionN, TcSigmaType) -> TcM (TcCoercionN, TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType -> TcCoercionN
mkNomReflCo TcSigmaType
act_res_ty, TcSigmaType
act_res_ty)
Just FixedRuntimeRepContext
frr_orig -> HasDebugCallStack =>
FixedRuntimeRepContext
-> TcSigmaType -> TcM (TcCoercionN, TcSigmaType)
FixedRuntimeRepContext
-> TcSigmaType -> TcM (TcCoercionN, TcSigmaType)
hasFixedRuntimeRep FixedRuntimeRepContext
frr_orig TcSigmaType
act_res_ty
; let final_co :: TcCoercionN
final_co = TcCoercionN
prom_co TcCoercionN -> TcCoercionN -> TcCoercionN
`mkTcTransCo` TcCoercionN
frr_co
; IORef (Maybe TcSigmaType) -> Maybe TcSigmaType -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef IORef (Maybe TcSigmaType)
ref (TcSigmaType -> Maybe TcSigmaType
forall a. a -> Maybe a
Just TcSigmaType
act_res_ty)
; TcCoercionN -> TcM TcCoercionN
forall (m :: * -> *) a. Monad m => a -> m a
return TcCoercionN
final_co }
}
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 -> TcM ()
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 TypedThing
-> TcSigmaType
-> 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) 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
= Bool -> SDoc -> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcSigmaType -> Bool
isRhoTy TcSigmaType
act_ty) (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
act_ty SDoc -> SDoc -> SDoc
$$ 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 { TcCoercionN
co <- HsExpr GhcRn -> TcSigmaType -> ExpRhoType -> TcM TcCoercionN
unifyExpectedType HsExpr GhcRn
rn_expr TcSigmaType
act_ty ExpRhoType
res_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) }
unifyExpectedType :: HsExpr GhcRn
-> TcRhoType
-> ExpRhoType
-> TcM TcCoercionN
unifyExpectedType :: HsExpr GhcRn -> TcSigmaType -> ExpRhoType -> TcM TcCoercionN
unifyExpectedType HsExpr GhcRn
rn_expr TcSigmaType
act_ty ExpRhoType
exp_ty
= case ExpRhoType
exp_ty of
Infer InferResult
inf_res -> TcSigmaType -> InferResult -> TcM TcCoercionN
fillInferResult TcSigmaType
act_ty InferResult
inf_res
Check TcSigmaType
exp_ty -> Maybe TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
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) TcSigmaType
act_ty TcSigmaType
exp_ty
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 -> TcM ()
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 TypedThing
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
orig UserTypeCtxt
ctxt Maybe TypedThing
forall a. Maybe a
Nothing TcSigmaType
ty_actual ExpRhoType
ty_expected }
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
inst_orig UserTypeCtxt
ctxt Maybe TypedThing
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 TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
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 :: CtOrigin
-> UserTypeCtxt
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeSigma :: CtOrigin
-> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeSigma CtOrigin
orig UserTypeCtxt
ctxt TcSigmaType
ty_actual TcSigmaType
ty_expected
= (TcSigmaType -> TcSigmaType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type (Maybe TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
forall a. Maybe a
Nothing) CtOrigin
orig UserTypeCtxt
ctxt TcSigmaType
ty_actual TcSigmaType
ty_expected
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 -> TcM ()
traceTc String
"tc_sub_type (drop to equality)" (SDoc -> TcM ()) -> SDoc -> TcM ()
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 -> TcM ()
traceTc String
"tc_sub_type (general case)" (SDoc -> TcM ()) -> SDoc -> TcM ()
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
, Var -> TcSigmaType -> CheckTyEqResult
checkTyVarEq Var
tv TcSigmaType
tau CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
cteInsolubleOccurs
= 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 -> TcRnIf TcGblEnv TcLclEnv (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 {
; rec { (HsWrapper
wrap, [(Name, Var)]
tv_prs, [Var]
given, TcSigmaType
rho_ty) <- SkolemInfo
-> TcSigmaType
-> TcM (HsWrapper, [(Name, Var)], [Var], TcSigmaType)
topSkolemise SkolemInfo
skol_info 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
; SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (UserTypeCtxt -> TcSigmaType -> [(Name, Var)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt TcSigmaType
expected_ty [(Name, Var)]
tv_prs)
}
; (TcEvBinds
ev_binds, result
res)
<- SkolemInfoAnon
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfoAnon
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints (SkolemInfo -> SkolemInfoAnon
getSkolemInfo 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 {
; rec { (HsWrapper
wrap, [(Name, Var)]
tv_prs, [Var]
given, TcSigmaType
rho_ty) <- SkolemInfo
-> TcSigmaType
-> TcM (HsWrapper, [(Name, Var)], [Var], TcSigmaType)
topSkolemise SkolemInfo
skol_info 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
; SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (UserTypeCtxt -> TcSigmaType -> [(Name, Var)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt TcSigmaType
expected_ty [(Name, Var)]
tv_prs)
}
; (TcEvBinds
ev_binds, result
result)
<- SkolemInfoAnon
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfoAnon
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints (SkolemInfo -> SkolemInfoAnon
getSkolemInfo 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 :: SkolemInfoAnon
-> [TcTyVar]
-> [EvVar]
-> TcM result
-> TcM (TcEvBinds, result)
checkConstraints :: SkolemInfoAnon
-> [Var] -> [Var] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfoAnon
skol_info [Var]
skol_tvs [Var]
given TcM result
thing_inside
= do { Bool
implication_needed <- SkolemInfoAnon -> [Var] -> [Var] -> TcM Bool
implicationNeeded SkolemInfoAnon
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
-> SkolemInfoAnon
-> [Var]
-> [Var]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfoAnon
skol_info [Var]
skol_tvs [Var]
given WantedConstraints
wanted
; String -> SDoc -> TcM ()
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 -> TcM ()
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 -> TcM ()
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 -> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info [Var]
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 { Implication
implic <- SkolemInfoAnon
-> [Var] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfoAnon
skol_info_anon [Var]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; Implication -> TcM ()
emitImplication Implication
implic }
| Bool
otherwise
= () -> TcM ()
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
-> [Var] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfoAnon
skol_info [Var]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
= Bool -> SDoc -> TcM Implication -> TcM Implication
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Var -> Bool
isSkolemTyVar (Var -> Bool) -> (Var -> Bool) -> Var -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> Var -> Bool
isTyVarTyVar) [Var]
skol_tvs) ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
skol_tvs) (TcM Implication -> TcM Implication)
-> TcM Implication -> TcM Implication
forall a b. (a -> b) -> a -> b
$
do { EvBindsVar
ev_binds <- TcM EvBindsVar
newNoTcEvBinds
; 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_eqs :: HasGivenEqs
ic_given_eqs = HasGivenEqs
NoGivenEqs
, ic_wanted :: WantedConstraints
ic_wanted = WantedConstraints
wanted
, ic_binds :: EvBindsVar
ic_binds = EvBindsVar
ev_binds
, ic_info :: SkolemInfoAnon
ic_info = SkolemInfoAnon
skol_info }
; Implication -> TcM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Implication -> m ()
checkImplicationInvariants Implication
implic'
; Implication -> TcM Implication
forall (m :: * -> *) a. Monad m => a -> m a
return Implication
implic' }
implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
implicationNeeded :: SkolemInfoAnon -> [Var] -> [Var] -> TcM Bool
implicationNeeded SkolemInfoAnon
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 (SkolemInfoAnon -> Bool
alwaysBuildImplication SkolemInfoAnon
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 :: SkolemInfoAnon -> Bool
alwaysBuildImplication :: SkolemInfoAnon -> Bool
alwaysBuildImplication SkolemInfoAnon
_ = Bool
False
buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar]
-> [EvVar] -> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor :: TcLevel
-> SkolemInfoAnon
-> [Var]
-> [Var]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfoAnon
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
= Bool
-> SDoc
-> TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Var -> Bool
isSkolemTyVar (Var -> Bool) -> (Var -> Bool) -> Var -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> Var -> Bool
isTyVarTyVar) [Var]
skol_tvs) ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
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 { 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 :: SkolemInfoAnon
ic_info = SkolemInfoAnon
skol_info }
; Implication -> TcM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Implication -> m ()
checkImplicationInvariants Implication
implic'
; (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 TypedThing
-> TcTauType -> TcTauType
-> TcM TcCoercionN
unifyType :: Maybe TypedThing -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe TypedThing
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 TypedThing -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty1
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
ty2
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
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 TypedThing -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty2
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
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 -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyKind Maybe TypedThing
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 TypedThing -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
ty1
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
ty2
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
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 -> TcM () -> TcM ()
forall gbl lcl. DumpFlag -> TcRnIf gbl lcl () -> TcRnIf gbl lcl ()
whenDOptM DumpFlag
Opt_D_dump_tc_trace (TcM () -> TcM ()) -> TcM () -> TcM ()
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 -> TcM ()
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 -> TcM ()
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 -> TcM ()
traceTc String
"u_tys" (SDoc -> TcM ()) -> SDoc -> TcM ()
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 -> TcM ()
traceTc String
"u_tys yields no coercion" SDoc
Outputable.empty
else String -> SDoc -> TcM ()
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 { Maybe TcSigmaType
lookup_res <- Var -> TcRnIf TcGblEnv TcLclEnv (Maybe TcSigmaType)
isFilledMetaTyVar_maybe Var
tv1
; case Maybe TcSigmaType
lookup_res of
Just TcSigmaType
ty1 -> do { String -> SDoc -> TcM ()
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 }
Maybe TcSigmaType
Nothing -> 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 { Maybe TcSigmaType
lookup_res <- Var -> TcRnIf TcGblEnv TcLclEnv (Maybe TcSigmaType)
isFilledMetaTyVar_maybe Var
tv2
; case Maybe TcSigmaType
lookup_res of
Just TcSigmaType
ty2 -> do { String -> SDoc -> TcM ()
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 }
Maybe TcSigmaType
Nothing -> 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
= Bool -> SDoc -> TcM TcCoercionN -> TcM TcCoercionN
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc1 Role
Nominal) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc1) (TcM TcCoercionN -> TcM TcCoercionN)
-> TcM TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$
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
= Bool -> TcM TcCoercionN -> TcM TcCoercionN
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
mustBeSaturated TyCon
tc2)) (TcM TcCoercionN -> TcM TcCoercionN)
-> TcM TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$
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
= Bool -> TcM TcCoercionN -> TcM TcCoercionN
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
mustBeSaturated TyCon
tc1)) (TcM TcCoercionN -> TcM TcCoercionN)
-> TcM TcCoercionN -> TcM TcCoercionN
forall a b. (a -> b) -> a -> b
$
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
-> TcSigmaType -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin TcSigmaType
orig_ty1 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 { TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; TcLevel -> TcM TcCoercionN
go TcLevel
cur_lvl }
where
go :: TcLevel -> TcM TcCoercionN
go TcLevel
cur_lvl
| TcLevel -> Var -> Bool
isTouchableMetaTyVar TcLevel
cur_lvl Var
tv1
, CheckTyEqResult -> Bool
cterHasNoProblem (Var -> TcSigmaType -> CheckTyEqResult
checkTyVarEq Var
tv1 TcSigmaType
ty2)
= do { Bool
can_continue_solving <- MetaInfo -> TcSigmaType -> TcM Bool
startSolvingByUnification (Var -> MetaInfo
metaTyVarInfo Var
tv1) TcSigmaType
ty2
; if Bool -> Bool
not Bool
can_continue_solving
then TcM TcCoercionN
not_ok_so_defer
else
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 -> TcM ()
traceTc String
"uUnfilledVar2 ok" (SDoc -> TcM ()) -> SDoc -> TcM ()
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 -> TcM ()
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
= TcM TcCoercionN
not_ok_so_defer
ty1 :: TcSigmaType
ty1 = Var -> TcSigmaType
mkTyVarTy Var
tv1
kind_origin :: CtOrigin
kind_origin = TcSigmaType
-> TcSigmaType -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin TcSigmaType
ty1 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
not_ok_so_defer :: TcM TcCoercionN
not_ok_so_defer =
do { String -> SDoc -> TcM ()
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 }
startSolvingByUnification :: MetaInfo -> TcType
-> TcM Bool
startSolvingByUnification :: MetaInfo -> TcSigmaType -> TcM Bool
startSolvingByUnification MetaInfo
_ TcSigmaType
xi
| TcSigmaType -> Bool
hasCoercionHoleTy TcSigmaType
xi
= Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
startSolvingByUnification MetaInfo
info TcSigmaType
xi
= case MetaInfo
info of
MetaInfo
CycleBreakerTv -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
ConcreteTv ConcreteTvOrigin
conc_orig ->
do { (TcSigmaType
_, [NotConcreteReason]
not_conc_reasons) <- ConcreteTvOrigin
-> TcSigmaType -> TcM (TcSigmaType, [NotConcreteReason])
makeTypeConcrete ConcreteTvOrigin
conc_orig TcSigmaType
xi
; case [NotConcreteReason]
not_conc_reasons of
[] -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
[NotConcreteReason]
_ -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False }
MetaInfo
TyVarTv ->
case TcSigmaType -> Maybe Var
tcGetTyVar_maybe TcSigmaType
xi of
Maybe Var
Nothing -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Just Var
tv ->
case Var -> TcTyVarDetails
tcTyVarDetails Var
tv of
SkolemTv {} -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
TcTyVarDetails
RuntimeUnk -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } ->
case MetaInfo
info of
MetaInfo
TyVarTv -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
MetaInfo
_ -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
MetaInfo
_ -> Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
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
= Bool -> SDoc -> Arity -> Arity
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Var -> Bool
isTyVar Var
tv) (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv) (Arity -> Arity) -> Arity -> Arity
forall a b. (a -> b) -> a -> b
$
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
CycleBreakerTv -> Arity
0
MetaInfo
TyVarTv -> Arity
1
ConcreteTv {} -> Arity
2
MetaInfo
TauTv -> Arity
3
MetaInfo
RuntimeUnkTv -> Arity
4
matchExpectedFunKind
:: TypedThing
-> Arity
-> TcKind
-> TcM Coercion
matchExpectedFunKind :: TypedThing -> Arity -> TcSigmaType -> TcM TcCoercionN
matchExpectedFunKind TypedThing
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 -> TcM 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 TypedThing -> Bool -> CtOrigin
TypeEqOrigin { uo_actual :: TcSigmaType
uo_actual = TcSigmaType
k
, uo_expected :: TcSigmaType
uo_expected = TcSigmaType
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
}
; TypeOrKind
-> CtOrigin -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
uType TypeOrKind
KindLevel CtOrigin
origin TcSigmaType
k TcSigmaType
new_fun }
{-# NOINLINE checkTyVarEq #-}
checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult
checkTyVarEq :: Var -> TcSigmaType -> CheckTyEqResult
checkTyVarEq Var
tv TcSigmaType
ty
= (CanEqLHS -> TcSigmaType -> CheckTyEqResult)
-> CanEqLHS -> TcSigmaType -> CheckTyEqResult
forall a. a -> a
inline CanEqLHS -> TcSigmaType -> CheckTyEqResult
checkTypeEq (Var -> CanEqLHS
TyVarLHS Var
tv) TcSigmaType
ty
{-# NOINLINE checkTyFamEq #-}
checkTyFamEq :: TyCon
-> [TcType]
-> TcType
-> CheckTyEqResult
checkTyFamEq :: TyCon -> ThetaType -> TcSigmaType -> CheckTyEqResult
checkTyFamEq TyCon
fun_tc ThetaType
fun_args TcSigmaType
ty
= (CanEqLHS -> TcSigmaType -> CheckTyEqResult)
-> CanEqLHS -> TcSigmaType -> CheckTyEqResult
forall a. a -> a
inline CanEqLHS -> TcSigmaType -> CheckTyEqResult
checkTypeEq (TyCon -> ThetaType -> CanEqLHS
TyFamLHS TyCon
fun_tc ThetaType
fun_args) TcSigmaType
ty
CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
`cterRemoveProblem` CheckTyEqProblem
cteTypeFamily
checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult
checkTypeEq :: CanEqLHS -> TcSigmaType -> CheckTyEqResult
checkTypeEq CanEqLHS
lhs TcSigmaType
ty
= TcSigmaType -> CheckTyEqResult
go TcSigmaType
ty
where
impredicative :: CheckTyEqResult
impredicative = CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteImpredicative
type_family :: CheckTyEqResult
type_family = CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteTypeFamily
insoluble_occurs :: CheckTyEqResult
insoluble_occurs = CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteInsolubleOccurs
soluble_occurs :: CheckTyEqResult
soluble_occurs = CheckTyEqProblem -> CheckTyEqResult
cteProblem CheckTyEqProblem
cteSolubleOccurs
ghci_tv :: Bool
ghci_tv
| TyVarLHS Var
tv <- CanEqLHS
lhs
, MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
RuntimeUnkTv } <- Var -> TcTyVarDetails
tcTyVarDetails Var
tv
= Bool
True
| Bool
otherwise
= Bool
False
go :: TcType -> CheckTyEqResult
go :: TcSigmaType -> CheckTyEqResult
go (TyVarTy Var
tv') = Var -> CheckTyEqResult
go_tv Var
tv'
go (TyConApp TyCon
tc ThetaType
tys) = TyCon -> ThetaType -> CheckTyEqResult
go_tc TyCon
tc ThetaType
tys
go (LitTy {}) = CheckTyEqResult
cteOK
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
a, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
r})
= TcSigmaType -> CheckTyEqResult
go TcSigmaType
w CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TcSigmaType -> CheckTyEqResult
go TcSigmaType
a CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TcSigmaType -> CheckTyEqResult
go TcSigmaType
r CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
if Bool -> Bool
not Bool
ghci_tv Bool -> Bool -> Bool
&& AnonArgFlag
af AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
InvisArg
then CheckTyEqResult
impredicative
else CheckTyEqResult
cteOK
go (AppTy TcSigmaType
fun TcSigmaType
arg) = TcSigmaType -> CheckTyEqResult
go TcSigmaType
fun CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TcSigmaType -> CheckTyEqResult
go TcSigmaType
arg
go (CastTy TcSigmaType
ty TcCoercionN
co) = TcSigmaType -> CheckTyEqResult
go TcSigmaType
ty CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TcCoercionN -> CheckTyEqResult
go_co TcCoercionN
co
go (CoercionTy TcCoercionN
co) = TcCoercionN -> CheckTyEqResult
go_co TcCoercionN
co
go (ForAllTy (Bndr Var
tv' ArgFlag
_) TcSigmaType
ty) = (case CanEqLHS
lhs of
TyVarLHS Var
tv | Var
tv Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
tv' -> TcSigmaType -> CheckTyEqResult
go_occ (Var -> TcSigmaType
tyVarKind Var
tv') CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> CheckTyEqResult -> CheckTyEqResult
cterClearOccursCheck (TcSigmaType -> CheckTyEqResult
go TcSigmaType
ty)
| Bool
otherwise -> TcSigmaType -> CheckTyEqResult
go_occ (Var -> TcSigmaType
tyVarKind Var
tv') CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TcSigmaType -> CheckTyEqResult
go TcSigmaType
ty
CanEqLHS
_ -> TcSigmaType -> CheckTyEqResult
go TcSigmaType
ty)
CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
if Bool
ghci_tv then CheckTyEqResult
cteOK else CheckTyEqResult
impredicative
go_tv :: TcTyVar -> CheckTyEqResult
go_tv :: Var -> CheckTyEqResult
go_tv = case CanEqLHS
lhs of
TyVarLHS Var
tv -> \ Var
tv' -> TcSigmaType -> CheckTyEqResult
go_occ (Var -> TcSigmaType
tyVarKind Var
tv') CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
if Var
tv Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
tv' then CheckTyEqResult
insoluble_occurs else CheckTyEqResult
cteOK
TyFamLHS {} -> \ Var
_tv' -> CheckTyEqResult
cteOK
go_occ :: TcSigmaType -> CheckTyEqResult
go_occ TcSigmaType
k = CheckTyEqResult -> CheckTyEqResult
cterFromKind (CheckTyEqResult -> CheckTyEqResult)
-> CheckTyEqResult -> CheckTyEqResult
forall a b. (a -> b) -> a -> b
$ TcSigmaType -> CheckTyEqResult
go TcSigmaType
k
go_tc :: TyCon -> [TcType] -> CheckTyEqResult
go_tc :: TyCon -> ThetaType -> CheckTyEqResult
go_tc = case CanEqLHS
lhs of
TyVarLHS {} -> \ TyCon
tc ThetaType
tys -> TyCon -> CheckTyEqResult
check_tc TyCon
tc CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TyCon -> ThetaType -> CheckTyEqResult
go_tc_args TyCon
tc ThetaType
tys
TyFamLHS TyCon
fam_tc ThetaType
fam_args -> \ TyCon
tc ThetaType
tys ->
if TyCon -> ThetaType -> TyCon -> ThetaType -> Bool
tcEqTyConApps TyCon
fam_tc ThetaType
fam_args TyCon
tc ThetaType
tys
then CheckTyEqResult
insoluble_occurs
else TyCon -> CheckTyEqResult
check_tc TyCon
tc CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> TyCon -> ThetaType -> CheckTyEqResult
go_tc_args TyCon
tc ThetaType
tys
go_tc_args :: TyCon -> [TcType] -> CheckTyEqResult
go_tc_args :: TyCon -> ThetaType -> CheckTyEqResult
go_tc_args TyCon
tc ThetaType
tys | TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
Nominal = (TcSigmaType -> CheckTyEqResult) -> ThetaType -> CheckTyEqResult
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TcSigmaType -> CheckTyEqResult
go ThetaType
tys
| Bool
otherwise
= let (ThetaType
tf_args, ThetaType
non_tf_args) = Arity -> ThetaType -> (ThetaType, ThetaType)
forall a. Arity -> [a] -> ([a], [a])
splitAt (TyCon -> Arity
tyConArity TyCon
tc) ThetaType
tys in
CheckTyEqResult -> CheckTyEqResult
cterSetOccursCheckSoluble ((TcSigmaType -> CheckTyEqResult) -> ThetaType -> CheckTyEqResult
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TcSigmaType -> CheckTyEqResult
go ThetaType
tf_args) CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> (TcSigmaType -> CheckTyEqResult) -> ThetaType -> CheckTyEqResult
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap TcSigmaType -> CheckTyEqResult
go ThetaType
non_tf_args
go_co :: TcCoercionN -> CheckTyEqResult
go_co TcCoercionN
co | TyVarLHS Var
tv <- CanEqLHS
lhs
, Var
tv Var -> VarSet -> Bool
`elemVarSet` TcCoercionN -> VarSet
tyCoVarsOfCo TcCoercionN
co
= CheckTyEqResult
soluble_occurs
| Bool
otherwise
= CheckTyEqResult
cteOK
check_tc :: TyCon -> CheckTyEqResult
check_tc :: TyCon -> CheckTyEqResult
check_tc
| Bool
ghci_tv = \ TyCon
_tc -> CheckTyEqResult
cteOK
| Bool
otherwise = \ TyCon
tc -> (if TyCon -> Bool
isTauTyCon TyCon
tc then CheckTyEqResult
cteOK else CheckTyEqResult
impredicative) CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
(if TyCon -> Bool
isFamFreeTyCon TyCon
tc then CheckTyEqResult
cteOK else CheckTyEqResult
type_family)