{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RecursiveDo #-}
module GHC.Tc.Utils.Unify (
tcWrapResult, tcWrapResultO, tcWrapResultMono,
tcTopSkolemise, tcSkolemiseScoped, tcSkolemiseExpType,
tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS,
tcSubTypeAmbiguity, 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.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.TyCo.Rep
import GHC.Core.TyCo.Ppr( debugPprType )
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Multiplicity
import qualified GHC.LanguageExtensions as LangExt
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
import GHC.Tc.Types.Origin
import GHC.Types.Name( Name, isSystemName )
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.Data.FastString( fsLit )
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 qualified Data.Semigroup as S ( (<>) )
matchActualFunTySigma
:: ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Arity, [Scaled TcSigmaType])
-> TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
matchActualFunTySigma :: ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Int, [Scaled Type])
-> Type
-> TcM (HsWrapper, Scaled Type, Type)
matchActualFunTySigma ExpectedFunTyOrigin
herald Maybe TypedThing
mb_thing (Int, [Scaled Type])
err_info Type
fun_ty
= Bool
-> SDoc
-> TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
isRhoTy Type
fun_ty) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fun_ty) (TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type))
-> TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a b. (a -> b) -> a -> b
$
Type -> TcM (HsWrapper, Scaled Type, Type)
go Type
fun_ty
where
go :: TcRhoType
-> TcM (HsWrapper, Scaled TcSigmaTypeFRR, TcSigmaType)
go :: Type -> TcM (HsWrapper, Scaled Type, Type)
go Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> TcM (HsWrapper, Scaled Type, Type)
go Type
ty'
go (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg_ty, ft_res :: Type -> Type
ft_res = Type
res_ty })
= Bool
-> TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af) (TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type))
-> TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a b. (a -> b) -> a -> b
$
do { (() :: Constraint) => FixedRuntimeRepContext -> Type -> TcM ()
FixedRuntimeRepContext -> Type -> TcM ()
hasFixedRuntimeRep_syntactic (ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Int
1) Type
arg_ty
; (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
w Type
arg_ty, Type
res_ty) }
go ty :: Type
ty@(TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { MetaDetails
cts <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
tv
; case MetaDetails
cts of
Indirect Type
ty' -> Type -> TcM (HsWrapper, Scaled Type, Type)
go Type
ty'
MetaDetails
Flexi -> Type -> TcM (HsWrapper, Scaled Type, Type)
defer Type
ty }
go Type
ty = (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM (Type -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt Type
ty) (Type -> TcM (HsWrapper, Scaled Type, Type)
defer Type
ty)
defer :: Type -> TcM (HsWrapper, Scaled Type, Type)
defer Type
fun_ty
= do { Type
arg_ty <- TcM Type
newOpenFlexiTyVarTy
; Type
res_ty <- TcM Type
newOpenFlexiTyVarTy
; Type
mult <- Type -> TcM Type
newFlexiTyVarTy Type
multiplicityTy
; let unif_fun_ty :: Type
unif_fun_ty = Type -> Type -> Type -> Type
tcMkVisFunTy Type
mult Type
arg_ty Type
res_ty
; Coercion
co <- Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
mb_thing Type
fun_ty Type
unif_fun_ty
; (() :: Constraint) => FixedRuntimeRepContext -> Type -> TcM ()
FixedRuntimeRepContext -> Type -> TcM ()
hasFixedRuntimeRep_syntactic (ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Int
1) Type
arg_ty
; (HsWrapper, Scaled Type, Type)
-> TcM (HsWrapper, Scaled Type, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsWrapper
mkWpCastN Coercion
co, Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
mult Type
arg_ty, Type
res_ty) }
mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt :: Type -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt Type
res_ty TidyEnv
env = TidyEnv
-> ExpectedFunTyOrigin
-> [Scaled Type]
-> Type
-> Int
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env ExpectedFunTyOrigin
herald ([Scaled Type] -> [Scaled Type]
forall a. [a] -> [a]
reverse [Scaled Type]
arg_tys_so_far)
Type
res_ty Int
n_val_args_in_call
(Int
n_val_args_in_call, [Scaled Type]
arg_tys_so_far) = (Int, [Scaled Type])
err_info
matchActualFunTysRho :: ExpectedFunTyOrigin
-> CtOrigin
-> Maybe TypedThing
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
matchActualFunTysRho :: ExpectedFunTyOrigin
-> CtOrigin
-> Maybe TypedThing
-> Int
-> Type
-> TcM (HsWrapper, [Scaled Type], Type)
matchActualFunTysRho ExpectedFunTyOrigin
herald CtOrigin
ct_orig Maybe TypedThing
mb_thing Int
n_val_args_wanted Type
fun_ty
= Int
-> [Scaled Type] -> Type -> TcM (HsWrapper, [Scaled Type], Type)
go Int
n_val_args_wanted [] Type
fun_ty
where
go :: Int
-> [Scaled Type] -> Type -> TcM (HsWrapper, [Scaled Type], Type)
go Int
n [Scaled Type]
so_far Type
fun_ty
| Bool -> Bool
not (Type -> Bool
isRhoTy Type
fun_ty)
= do { (HsWrapper
wrap1, Type
rho) <- CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiate CtOrigin
ct_orig Type
fun_ty
; (HsWrapper
wrap2, [Scaled Type]
arg_tys, Type
res_ty) <- Int
-> [Scaled Type] -> Type -> TcM (HsWrapper, [Scaled Type], Type)
go Int
n [Scaled Type]
so_far Type
rho
; (HsWrapper, [Scaled Type], Type)
-> TcM (HsWrapper, [Scaled Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1, [Scaled Type]
arg_tys, Type
res_ty) }
go Int
0 [Scaled Type]
_ Type
fun_ty = (HsWrapper, [Scaled Type], Type)
-> TcM (HsWrapper, [Scaled Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, [], Type
fun_ty)
go Int
n [Scaled Type]
so_far Type
fun_ty
= do { (HsWrapper
wrap_fun1, Scaled Type
arg_ty1, Type
res_ty1) <- ExpectedFunTyOrigin
-> Maybe TypedThing
-> (Int, [Scaled Type])
-> Type
-> TcM (HsWrapper, Scaled Type, Type)
matchActualFunTySigma
ExpectedFunTyOrigin
herald Maybe TypedThing
mb_thing
(Int
n_val_args_wanted, [Scaled Type]
so_far)
Type
fun_ty
; (HsWrapper
wrap_res, [Scaled Type]
arg_tys, Type
res_ty) <- Int
-> [Scaled Type] -> Type -> TcM (HsWrapper, [Scaled Type], Type)
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Scaled Type
arg_ty1Scaled Type -> [Scaled Type] -> [Scaled Type]
forall a. a -> [a] -> [a]
:[Scaled Type]
so_far) Type
res_ty1
; let wrap_fun2 :: HsWrapper
wrap_fun2 = HsWrapper -> HsWrapper -> Scaled Type -> Type -> HsWrapper
mkWpFun HsWrapper
idHsWrapper HsWrapper
wrap_res Scaled Type
arg_ty1 Type
res_ty
; (HsWrapper, [Scaled Type], Type)
-> TcM (HsWrapper, [Scaled Type], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap_fun2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap_fun1, Scaled Type
arg_ty1Scaled Type -> [Scaled Type] -> [Scaled Type]
forall a. a -> [a] -> [a]
:[Scaled Type]
arg_tys, Type
res_ty) }
matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin
-> UserTypeCtxt
-> Arity
-> ExpRhoType
-> ([Scaled ExpSigmaTypeFRR] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin
-> UserTypeCtxt
-> Int
-> ExpRhoType
-> ([Scaled ExpRhoType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
matchExpectedFunTys ExpectedFunTyOrigin
herald UserTypeCtxt
ctx Int
arity ExpRhoType
orig_ty [Scaled ExpRhoType] -> ExpRhoType -> TcM a
thing_inside
= case ExpRhoType
orig_ty of
Check Type
ty -> [Scaled ExpRhoType] -> Int -> Type -> TcM (HsWrapper, a)
go [] Int
arity Type
ty
ExpRhoType
_ -> [Scaled ExpRhoType] -> Int -> ExpRhoType -> TcM (HsWrapper, a)
defer [] Int
arity ExpRhoType
orig_ty
where
go :: [Scaled ExpRhoType] -> Int -> Type -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Int
n Type
ty
| ([TcTyVar]
tvs, ThetaType
theta, Type
_) <- Type -> ([TcTyVar], ThetaType, Type)
tcSplitSigmaTy Type
ty
, Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= do { (HsWrapper
wrap_gen, (HsWrapper
wrap_res, a
result)) <- UserTypeCtxt
-> Type
-> (Type -> TcM (HsWrapper, a))
-> TcM (HsWrapper, (HsWrapper, a))
forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcTopSkolemise UserTypeCtxt
ctx Type
ty ((Type -> TcM (HsWrapper, a)) -> TcM (HsWrapper, (HsWrapper, a)))
-> (Type -> TcM (HsWrapper, a)) -> TcM (HsWrapper, (HsWrapper, a))
forall a b. (a -> b) -> a -> b
$ \Type
ty' ->
[Scaled ExpRhoType] -> Int -> Type -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Int
n Type
ty'
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) 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 Int
0 Type
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) (Type -> ExpRhoType
mkCheckExpType Type
rho_ty)
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, a
result) }
go [Scaled ExpRhoType]
acc_arg_tys Int
n Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = [Scaled ExpRhoType] -> Int -> Type -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Int
n Type
ty'
go [Scaled ExpRhoType]
acc_arg_tys Int
n (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
mult, ft_arg :: Type -> Type
ft_arg = Type
arg_ty, ft_res :: Type -> Type
ft_res = Type
res_ty })
= Bool -> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. HasCallStack => Bool -> a -> a
assert (FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af) (TcM (HsWrapper, a) -> TcM (HsWrapper, a))
-> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$
do { let arg_pos :: Int
arg_pos = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Scaled ExpRhoType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Scaled ExpRhoType]
acc_arg_tys
; (Coercion
arg_co, Type
arg_ty) <- (() :: Constraint) =>
FixedRuntimeRepContext -> Type -> TcM (Coercion, Type)
FixedRuntimeRepContext -> Type -> TcM (Coercion, Type)
hasFixedRuntimeRep (ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Int
arg_pos) Type
arg_ty
; (HsWrapper
wrap_res, a
result) <- [Scaled ExpRhoType] -> Int -> Type -> TcM (HsWrapper, a)
go ((Type -> ExpRhoType -> Scaled ExpRhoType
forall a. Type -> a -> Scaled a
Scaled Type
mult (ExpRhoType -> Scaled ExpRhoType)
-> ExpRhoType -> Scaled ExpRhoType
forall a b. (a -> b) -> a -> b
$ Type -> ExpRhoType
mkCheckExpType Type
arg_ty) Scaled ExpRhoType -> [Scaled ExpRhoType] -> [Scaled ExpRhoType]
forall a. a -> [a] -> [a]
: [Scaled ExpRhoType]
acc_arg_tys)
(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Type
res_ty
; let wrap_arg :: HsWrapper
wrap_arg = Coercion -> HsWrapper
mkWpCastN Coercion
arg_co
fun_wrap :: HsWrapper
fun_wrap = HsWrapper -> HsWrapper -> Scaled Type -> Type -> HsWrapper
mkWpFun HsWrapper
wrap_arg HsWrapper
wrap_res (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
mult Type
arg_ty) Type
res_ty
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
fun_wrap, a
result) }
go [Scaled ExpRhoType]
acc_arg_tys Int
n ty :: Type
ty@(TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { MetaDetails
cts <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
tv
; case MetaDetails
cts of
Indirect Type
ty' -> [Scaled ExpRhoType] -> Int -> Type -> TcM (HsWrapper, a)
go [Scaled ExpRhoType]
acc_arg_tys Int
n Type
ty'
MetaDetails
Flexi -> [Scaled ExpRhoType] -> Int -> ExpRhoType -> TcM (HsWrapper, a)
defer [Scaled ExpRhoType]
acc_arg_tys Int
n (Type -> ExpRhoType
mkCheckExpType Type
ty) }
go [Scaled ExpRhoType]
acc_arg_tys Int
n Type
ty = (TidyEnv -> TcM (TidyEnv, SDoc))
-> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. (TidyEnv -> TcM (TidyEnv, SDoc)) -> TcM a -> TcM a
addErrCtxtM ([Scaled ExpRhoType] -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt [Scaled ExpRhoType]
acc_arg_tys Type
ty) (TcM (HsWrapper, a) -> TcM (HsWrapper, a))
-> TcM (HsWrapper, a) -> TcM (HsWrapper, a)
forall a b. (a -> b) -> a -> b
$
[Scaled ExpRhoType] -> Int -> ExpRhoType -> TcM (HsWrapper, a)
defer [Scaled ExpRhoType]
acc_arg_tys Int
n (Type -> ExpRhoType
mkCheckExpType Type
ty)
defer :: [Scaled ExpSigmaTypeFRR] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
defer :: [Scaled ExpRhoType] -> Int -> ExpRhoType -> TcM (HsWrapper, a)
defer [Scaled ExpRhoType]
acc_arg_tys Int
n ExpRhoType
fun_ty
= do { let last_acc_arg_pos :: Int
last_acc_arg_pos = [Scaled ExpRhoType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Scaled ExpRhoType]
acc_arg_tys
; [Scaled ExpRhoType]
more_arg_tys <- (Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType))
-> [Int] -> IOEnv (Env TcGblEnv TcLclEnv) [Scaled ExpRhoType]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
new_exp_arg_ty [Int
last_acc_arg_pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 .. Int
last_acc_arg_pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 Type]
more_arg_tys <- (Scaled ExpRhoType -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled Type))
-> [Scaled ExpRhoType]
-> IOEnv (Env TcGblEnv TcLclEnv) [Scaled Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Scaled Type
m ExpRhoType
t) -> Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
m (Type -> Scaled Type)
-> TcM Type -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpRhoType -> TcM Type
readExpType ExpRhoType
t) [Scaled ExpRhoType]
more_arg_tys
; Type
res_ty <- ExpRhoType -> TcM Type
readExpType ExpRhoType
res_ty
; let unif_fun_ty :: Type
unif_fun_ty = [Scaled Type] -> Type -> Type
(() :: Constraint) => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
more_arg_tys Type
res_ty
; HsWrapper
wrap <- CtOrigin -> UserTypeCtxt -> Type -> ExpRhoType -> TcM HsWrapper
tcSubType CtOrigin
AppOrigin UserTypeCtxt
ctx Type
unif_fun_ty ExpRhoType
fun_ty
; (HsWrapper, a) -> TcM (HsWrapper, a)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) 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 :: Int -> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
new_exp_arg_ty Int
arg_pos
= Type -> ExpRhoType -> Scaled ExpRhoType
forall a. Type -> a -> Scaled a
mkScaled (Type -> ExpRhoType -> Scaled ExpRhoType)
-> TcM Type
-> IOEnv (Env TcGblEnv TcLclEnv) (ExpRhoType -> Scaled ExpRhoType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TcM Type
newFlexiTyVarTy Type
multiplicityTy
IOEnv (Env TcGblEnv TcLclEnv) (ExpRhoType -> Scaled ExpRhoType)
-> TcM ExpRhoType
-> IOEnv (Env TcGblEnv TcLclEnv) (Scaled ExpRhoType)
forall a b.
IOEnv (Env TcGblEnv TcLclEnv) (a -> b)
-> IOEnv (Env TcGblEnv TcLclEnv) a
-> IOEnv (Env TcGblEnv TcLclEnv) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FixedRuntimeRepContext -> TcM ExpRhoType
newInferExpTypeFRR (ExpectedFunTyOrigin -> Int -> FixedRuntimeRepContext
FRRExpectedFunTy ExpectedFunTyOrigin
herald Int
arg_pos)
mk_ctxt :: [Scaled ExpSigmaTypeFRR] -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt :: [Scaled ExpRhoType] -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
mk_ctxt [Scaled ExpRhoType]
arg_tys Type
res_ty TidyEnv
env
= TidyEnv
-> ExpectedFunTyOrigin
-> [Scaled Type]
-> Type
-> Int
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env ExpectedFunTyOrigin
herald [Scaled Type]
arg_tys' Type
res_ty Int
arity
where
arg_tys' :: [Scaled Type]
arg_tys' = (Scaled ExpRhoType -> Scaled Type)
-> [Scaled ExpRhoType] -> [Scaled Type]
forall a b. (a -> b) -> [a] -> [b]
map (\(Scaled Type
u ExpRhoType
v) -> Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
u (String -> ExpRhoType -> Type
checkingExpType String
"matchExpectedFunTys" ExpRhoType
v)) ([Scaled ExpRhoType] -> [Scaled Type])
-> [Scaled ExpRhoType] -> [Scaled Type]
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 Type]
-> Type
-> Int
-> TcM (TidyEnv, SDoc)
mkFunTysMsg TidyEnv
env ExpectedFunTyOrigin
herald [Scaled Type]
arg_tys Type
res_ty Int
n_val_args_in_call
= do { (TidyEnv
env', Type
fun_rho) <- TidyEnv -> Type -> TcM (TidyEnv, Type)
zonkTidyTcType TidyEnv
env (Type -> TcM (TidyEnv, Type)) -> Type -> TcM (TidyEnv, Type)
forall a b. (a -> b) -> a -> b
$
[Scaled Type] -> Type -> Type
(() :: Constraint) => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
arg_tys Type
res_ty
; let ([Scaled Type]
all_arg_tys, Type
_) = Type -> ([Scaled Type], Type)
splitFunTys Type
fun_rho
n_fun_args :: Int
n_fun_args = [Scaled Type] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Scaled Type]
all_arg_tys
msg :: SDoc
msg | Int
n_val_args_in_call Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
n_fun_args
= String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"In the result of a function call"
| Bool
otherwise
= SDoc -> Int -> SDoc -> SDoc
hang (SDoc
full_herald SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
comma)
Int
2 ([SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"but its type" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
quotes (Type -> SDoc
pprType Type
fun_rho)
, if Int
n_fun_args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has none"
else String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"has only" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
speakN Int
n_fun_args])
; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc -> SDoc
speakNOf Int
n_val_args_in_call (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"value argument")
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
matchExpectedListTy :: Type -> TcM (Coercion, Type)
matchExpectedListTy Type
exp_ty
= do { (Coercion
co, [Type
elt_ty]) <- TyCon -> Type -> TcM (Coercion, ThetaType)
matchExpectedTyConApp TyCon
listTyCon Type
exp_ty
; (Coercion, Type) -> TcM (Coercion, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
co, Type
elt_ty) }
matchExpectedTyConApp :: TyCon
-> TcRhoType
-> TcM (TcCoercionN,
[TcSigmaType])
matchExpectedTyConApp :: TyCon -> Type -> TcM (Coercion, ThetaType)
matchExpectedTyConApp TyCon
tc Type
orig_ty
= Bool
-> SDoc -> TcM (Coercion, ThetaType) -> TcM (Coercion, ThetaType)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TyCon -> Bool
isAlgTyCon TyCon
tc) (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc) (TcM (Coercion, ThetaType) -> TcM (Coercion, ThetaType))
-> TcM (Coercion, ThetaType) -> TcM (Coercion, ThetaType)
forall a b. (a -> b) -> a -> b
$
Type -> TcM (Coercion, ThetaType)
go Type
orig_ty
where
go :: Type -> TcM (Coercion, ThetaType)
go Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Type -> TcM (Coercion, ThetaType)
go Type
ty'
go ty :: Type
ty@(TyConApp TyCon
tycon ThetaType
args)
| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tycon
= (Coercion, ThetaType) -> TcM (Coercion, ThetaType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
ty, ThetaType
args)
go (TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { MetaDetails
cts <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
tv
; case MetaDetails
cts of
Indirect Type
ty -> Type -> TcM (Coercion, ThetaType)
go Type
ty
MetaDetails
Flexi -> TcM (Coercion, ThetaType)
defer }
go Type
_ = TcM (Coercion, ThetaType)
defer
defer :: TcM (Coercion, ThetaType)
defer
= do { (Subst
_, [TcTyVar]
arg_tvs) <- [TcTyVar] -> TcM (Subst, [TcTyVar])
newMetaTyVars (TyCon -> [TcTyVar]
tyConTyVars TyCon
tc)
; String -> SDoc -> TcM ()
traceTc String
"matchExpectedTyConApp" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon -> [TcTyVar]
tyConTyVars TyCon
tc) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
arg_tvs)
; let args :: ThetaType
args = [TcTyVar] -> ThetaType
mkTyVarTys [TcTyVar]
arg_tvs
tc_template :: Type
tc_template = TyCon -> ThetaType -> Type
mkTyConApp TyCon
tc ThetaType
args
; Coercion
co <- Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing Type
tc_template Type
orig_ty
; (Coercion, ThetaType) -> TcM (Coercion, ThetaType)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
co, ThetaType
args) }
matchExpectedAppTy :: TcRhoType
-> TcM (TcCoercion,
(TcSigmaType, TcSigmaType))
matchExpectedAppTy :: Type -> TcM (Coercion, (Type, Type))
matchExpectedAppTy Type
orig_ty
= Type -> TcM (Coercion, (Type, Type))
go Type
orig_ty
where
go :: Type -> TcM (Coercion, (Type, Type))
go Type
ty
| Just Type
ty' <- Type -> Maybe Type
coreView Type
ty = Type -> TcM (Coercion, (Type, Type))
go Type
ty'
| Just (Type
fun_ty, Type
arg_ty) <- Type -> Maybe (Type, Type)
tcSplitAppTy_maybe Type
ty
= (Coercion, (Type, Type)) -> TcM (Coercion, (Type, Type))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
orig_ty, (Type
fun_ty, Type
arg_ty))
go (TyVarTy TcTyVar
tv)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
tv
= do { MetaDetails
cts <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
tv
; case MetaDetails
cts of
Indirect Type
ty -> Type -> TcM (Coercion, (Type, Type))
go Type
ty
MetaDetails
Flexi -> TcM (Coercion, (Type, Type))
defer }
go Type
_ = TcM (Coercion, (Type, Type))
defer
defer :: TcM (Coercion, (Type, Type))
defer
= do { Type
ty1 <- Type -> TcM Type
newFlexiTyVarTy Type
kind1
; Type
ty2 <- Type -> TcM Type
newFlexiTyVarTy Type
kind2
; Coercion
co <- Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing (Type -> Type -> Type
mkAppTy Type
ty1 Type
ty2) Type
orig_ty
; (Coercion, (Type, Type)) -> TcM (Coercion, (Type, Type))
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion
co, (Type
ty1, Type
ty2)) }
orig_kind :: Type
orig_kind = (() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
orig_ty
kind1 :: Type
kind1 = (() :: Constraint) => Type -> Type -> Type
Type -> Type -> Type
mkVisFunTyMany Type
liftedTypeKind Type
orig_kind
kind2 :: Type
kind2 = Type
liftedTypeKind
fillInferResult :: TcType -> InferResult -> TcM TcCoercionN
fillInferResult :: Type -> InferResult -> TcM Coercion
fillInferResult Type
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 Type)
ir_ref = IORef (Maybe Type)
ref })
= do { Maybe Type
mb_exp_res_ty <- IORef (Maybe Type) -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a gbl lcl. TcRef a -> TcRnIf gbl lcl a
readTcRef IORef (Maybe Type)
ref
; case Maybe Type
mb_exp_res_ty of
Just Type
exp_res_ty
-> do { String -> SDoc -> TcM ()
traceTc String
"Joining inferred ExpType" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
colon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
act_res_ty SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
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
$
Type -> TcM ()
ensureMonoType Type
act_res_ty
; Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing Type
act_res_ty Type
exp_res_ty }
Maybe Type
Nothing
-> do { String -> SDoc -> TcM ()
traceTc String
"Filling inferred ExpType" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
Unique -> SDoc
forall a. Outputable a => a -> SDoc
ppr Unique
u SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
act_res_ty
; (Coercion
prom_co, Type
act_res_ty) <- TcLevel -> Type -> TcM (Coercion, Type)
promoteTcType TcLevel
res_lvl Type
act_res_ty
; (Coercion
frr_co, Type
act_res_ty) <-
case Maybe FixedRuntimeRepContext
mb_frr of
Maybe FixedRuntimeRepContext
Nothing -> (Coercion, Type) -> TcM (Coercion, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
act_res_ty, Type
act_res_ty)
Just FixedRuntimeRepContext
frr_orig -> (() :: Constraint) =>
FixedRuntimeRepContext -> Type -> TcM (Coercion, Type)
FixedRuntimeRepContext -> Type -> TcM (Coercion, Type)
hasFixedRuntimeRep FixedRuntimeRepContext
frr_orig Type
act_res_ty
; let final_co :: Coercion
final_co = Coercion
prom_co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
frr_co
; IORef (Maybe Type) -> Maybe Type -> TcM ()
forall a gbl lcl. TcRef a -> a -> TcRnIf gbl lcl ()
writeTcRef IORef (Maybe Type)
ref (Type -> Maybe Type
forall a. a -> Maybe a
Just Type
act_res_ty)
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
final_co }
}
tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResult :: HsExpr GhcRn
-> HsExpr GhcTc -> Type -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResult HsExpr GhcRn
rn_expr = CtOrigin
-> HsExpr GhcRn
-> HsExpr GhcTc
-> Type
-> 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
-> Type
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcWrapResultO CtOrigin
orig HsExpr GhcRn
rn_expr HsExpr GhcTc
expr Type
actual_ty ExpRhoType
res_ty
= do { String -> SDoc -> TcM ()
traceTc String
"tcWrapResult" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Actual: " SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
actual_ty
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"Expected:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
res_ty ])
; HsWrapper
wrap <- CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> Type
-> 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) Type
actual_ty ExpRhoType
res_ty
; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 -> Type -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
rn_expr HsExpr GhcTc
expr Type
act_ty ExpRhoType
res_ty
= Bool -> SDoc -> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (Type -> Bool
isRhoTy Type
act_ty) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
act_ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_expr) (TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc))
-> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
do { Coercion
co <- HsExpr GhcRn -> Type -> ExpRhoType -> TcM Coercion
unifyExpectedType HsExpr GhcRn
rn_expr Type
act_ty ExpRhoType
res_ty
; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrapCo Coercion
co HsExpr GhcTc
expr) }
unifyExpectedType :: HsExpr GhcRn
-> TcRhoType
-> ExpRhoType
-> TcM TcCoercionN
unifyExpectedType :: HsExpr GhcRn -> Type -> ExpRhoType -> TcM Coercion
unifyExpectedType HsExpr GhcRn
rn_expr Type
act_ty ExpRhoType
exp_ty
= case ExpRhoType
exp_ty of
Infer InferResult
inf_res -> Type -> InferResult -> TcM Coercion
fillInferResult Type
act_ty InferResult
inf_res
Check Type
exp_ty -> Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType (TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (TypedThing -> Maybe TypedThing) -> TypedThing -> Maybe TypedThing
forall a b. (a -> b) -> a -> b
$ HsExpr GhcRn -> TypedThing
HsExprRnThing HsExpr GhcRn
rn_expr) Type
act_ty Type
exp_ty
tcSubTypePat :: CtOrigin -> UserTypeCtxt
-> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypePat :: CtOrigin -> UserTypeCtxt -> ExpRhoType -> Type -> TcM HsWrapper
tcSubTypePat CtOrigin
inst_orig UserTypeCtxt
ctxt (Check Type
ty_actual) Type
ty_expected
= (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type Type -> Type -> TcM Coercion
unifyTypeET CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
tcSubTypePat CtOrigin
_ UserTypeCtxt
_ (Infer InferResult
inf_res) Type
ty_expected
= do { Coercion
co <- Type -> InferResult -> TcM Coercion
fillInferResult Type
ty_expected InferResult
inf_res
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsWrapper
mkWpCastN (Coercion -> Coercion
mkSymCo Coercion
co)) }
tcSubType :: CtOrigin -> UserTypeCtxt
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubType :: CtOrigin -> UserTypeCtxt -> Type -> ExpRhoType -> TcM HsWrapper
tcSubType CtOrigin
orig UserTypeCtxt
ctxt Type
ty_actual ExpRhoType
ty_expected
= Type -> ExpRhoType -> TcM HsWrapper -> TcM HsWrapper
forall a. Type -> ExpRhoType -> TcM a -> TcM a
addSubTypeCtxt Type
ty_actual ExpRhoType
ty_expected (TcM HsWrapper -> TcM HsWrapper) -> TcM HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"tcSubType" ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [UserTypeCtxt -> SDoc
pprUserTypeCtxt UserTypeCtxt
ctxt, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual, ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
ty_expected])
; CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> Type
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
orig UserTypeCtxt
ctxt Maybe TypedThing
forall a. Maybe a
Nothing Type
ty_actual ExpRhoType
ty_expected }
tcSubTypeDS :: HsExpr GhcRn
-> TcRhoType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeDS :: HsExpr GhcRn -> Type -> ExpRhoType -> TcM HsWrapper
tcSubTypeDS HsExpr GhcRn
rn_expr Type
act_rho ExpRhoType
res_ty
= case ExpRhoType
res_ty of
Check Type
exp_rho -> (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_deep (Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
m_thing) CtOrigin
orig
UserTypeCtxt
GenSigCtxt Type
act_rho Type
exp_rho
Infer InferResult
inf_res -> do { Coercion
co <- Type -> InferResult -> TcM Coercion
fillInferResult Type
act_rho InferResult
inf_res
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsWrapper
mkWpCastN Coercion
co) }
where
orig :: CtOrigin
orig = HsExpr GhcRn -> CtOrigin
exprCtOrigin HsExpr GhcRn
rn_expr
m_thing :: Maybe TypedThing
m_thing = TypedThing -> Maybe TypedThing
forall a. a -> Maybe a
Just (HsExpr GhcRn -> TypedThing
HsExprRnThing HsExpr GhcRn
rn_expr)
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> TcSigmaType
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC :: CtOrigin
-> UserTypeCtxt
-> Maybe TypedThing
-> Type
-> ExpRhoType
-> TcM HsWrapper
tcSubTypeNC CtOrigin
inst_orig UserTypeCtxt
ctxt Maybe TypedThing
m_thing Type
ty_actual ExpRhoType
res_ty
= case ExpRhoType
res_ty of
Check Type
ty_expected -> (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type (Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
m_thing) CtOrigin
inst_orig UserTypeCtxt
ctxt
Type
ty_actual Type
ty_expected
Infer InferResult
inf_res -> do { (HsWrapper
wrap, Type
rho) <- CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiate CtOrigin
inst_orig Type
ty_actual
; Coercion
co <- Type -> InferResult -> TcM Coercion
fillInferResult Type
rho InferResult
inf_res
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsWrapper
mkWpCastN Coercion
co HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap) }
tcSubTypeSigma :: CtOrigin
-> UserTypeCtxt
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeSigma :: CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tcSubTypeSigma CtOrigin
orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
= (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type (Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing) CtOrigin
orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
tcSubTypeAmbiguity :: UserTypeCtxt
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
tcSubTypeAmbiguity :: UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tcSubTypeAmbiguity UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
= (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_shallow (Maybe TypedThing -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
forall a. Maybe a
Nothing)
(UserTypeCtxt -> CtOrigin
AmbiguityCheckOrigin UserTypeCtxt
ctxt)
UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
addSubTypeCtxt :: forall a. Type -> ExpRhoType -> TcM a -> TcM a
addSubTypeCtxt Type
ty_actual ExpRhoType
ty_expected TcM a
thing_inside
| Type -> Bool
isRhoTy Type
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, Type
ty_actual) <- TidyEnv -> Type -> TcM (TidyEnv, Type)
zonkTidyTcType TidyEnv
tidy_env Type
ty_actual
; Type
ty_expected <- ExpRhoType -> TcM Type
readExpType ExpRhoType
ty_expected
; (TidyEnv
tidy_env, Type
ty_expected) <- TidyEnv -> Type -> TcM (TidyEnv, Type)
zonkTidyTcType TidyEnv
tidy_env Type
ty_expected
; let msg :: SDoc
msg = [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"When checking that:")
Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual)
, Int -> SDoc -> SDoc
nest Int
2 (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"is more polymorphic than:")
Int
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_expected)) ]
; (TidyEnv, SDoc) -> TcM (TidyEnv, SDoc)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TidyEnv
tidy_env, SDoc
msg) }
tc_sub_type, tc_sub_type_deep, tc_sub_type_shallow
:: (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcSigmaType
-> TcM HsWrapper
tc_sub_type :: (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
= do { Bool
deep_subsumption <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DeepSubsumption
; if Bool
deep_subsumption
then (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_deep Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
else (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_shallow Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
}
tc_sub_type_shallow :: (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_shallow Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
| Type -> Bool
definitely_poly Type
ty_expected
, Type -> Bool
definitely_mono_shallow Type
ty_actual
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type (drop to equality)" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_expected ]
; Coercion -> HsWrapper
mkWpCastN (Coercion -> HsWrapper) -> TcM Coercion -> TcM HsWrapper
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Type -> Type -> TcM Coercion
unify Type
ty_actual Type
ty_expected }
| Bool
otherwise
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type (general case)" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_expected ]
; (HsWrapper
sk_wrap, HsWrapper
inner_wrap)
<- UserTypeCtxt
-> Type -> (Type -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper)
forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcTopSkolemise UserTypeCtxt
ctxt Type
ty_expected ((Type -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper))
-> (Type -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper)
forall a b. (a -> b) -> a -> b
$ \ Type
sk_rho ->
do { (HsWrapper
wrap, Type
rho_a) <- CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiate CtOrigin
inst_orig Type
ty_actual
; Coercion
cow <- Type -> Type -> TcM Coercion
unify Type
rho_a Type
sk_rho
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsWrapper
mkWpCastN Coercion
cow HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap) }
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
sk_wrap HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
inner_wrap) }
tc_sub_type_deep :: (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_deep Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
| Type -> Bool
definitely_poly Type
ty_expected
, Type -> Bool
definitely_mono_deep Type
ty_actual
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type_deep (drop to equality)" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_expected ]
; Coercion -> HsWrapper
mkWpCastN (Coercion -> HsWrapper) -> TcM Coercion -> TcM HsWrapper
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
Type -> Type -> TcM Coercion
unify Type
ty_actual Type
ty_expected }
| Bool
otherwise
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type_deep (general case)" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_expected ]
; (HsWrapper
sk_wrap, HsWrapper
inner_wrap)
<- UserTypeCtxt
-> Type -> (Type -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper)
forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcDeeplySkolemise UserTypeCtxt
ctxt Type
ty_expected ((Type -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper))
-> (Type -> TcM HsWrapper) -> TcM (HsWrapper, HsWrapper)
forall a b. (a -> b) -> a -> b
$ \ Type
sk_rho ->
(Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_ds Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
sk_rho
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
sk_wrap HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
inner_wrap) }
definitely_mono_shallow :: TcType -> Bool
definitely_mono_shallow :: Type -> Bool
definitely_mono_shallow Type
ty = Type -> Bool
isRhoTy Type
ty
definitely_mono_deep :: TcType -> Bool
definitely_mono_deep :: Type -> Bool
definitely_mono_deep Type
ty
| Bool -> Bool
not (Type -> Bool
definitely_mono_shallow Type
ty) = Bool
False
| Just (Scaled Type
_, Type
res) <- Type -> Maybe (Scaled Type, Type)
tcSplitFunTy_maybe Type
ty = Type -> Bool
definitely_mono_deep Type
res
| Bool
otherwise = Bool
True
definitely_poly :: TcType -> Bool
definitely_poly :: Type -> Bool
definitely_poly Type
ty
| ([TcTyVar]
tvs, ThetaType
theta, Type
tau) <- Type -> ([TcTyVar], ThetaType, Type)
tcSplitSigmaTy Type
ty
, (TcTyVar
tv:[TcTyVar]
_) <- [TcTyVar]
tvs
, ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta
, TcTyVar -> Type -> CheckTyEqResult
checkTyVarEq TcTyVar
tv Type
tau CheckTyEqResult -> CheckTyEqProblem -> Bool
`cterHasProblem` CheckTyEqProblem
cteInsolubleOccurs
= Bool
True
| Bool
otherwise
= Bool
False
tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
tcSubMult :: CtOrigin -> Type -> Type -> TcM HsWrapper
tcSubMult CtOrigin
origin Type
w_actual Type
w_expected
| Just (Type
w1, Type
w2) <- Type -> Maybe (Type, Type)
isMultMul Type
w_actual =
do { HsWrapper
w1 <- CtOrigin -> Type -> Type -> TcM HsWrapper
tcSubMult CtOrigin
origin Type
w1 Type
w_expected
; HsWrapper
w2 <- CtOrigin -> Type -> Type -> TcM HsWrapper
tcSubMult CtOrigin
origin Type
w2 Type
w_expected
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
w1 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
w2) }
tcSubMult CtOrigin
origin Type
w_actual Type
w_expected =
case Type -> Type -> IsSubmult
submult Type
w_actual Type
w_expected of
IsSubmult
Submult -> HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return HsWrapper
WpHole
IsSubmult
Unknown -> CtOrigin -> Type -> Type -> TcM HsWrapper
tcEqMult CtOrigin
origin Type
w_actual Type
w_expected
tcEqMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper
tcEqMult :: CtOrigin -> Type -> Type -> TcM HsWrapper
tcEqMult CtOrigin
origin Type
w_actual Type
w_expected = do
{
; Coercion
coercion <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
TypeLevel CtOrigin
origin Type
w_actual Type
w_expected
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> TcM HsWrapper) -> HsWrapper -> TcM HsWrapper
forall a b. (a -> b) -> a -> b
$ if Coercion -> Bool
isReflCo Coercion
coercion then HsWrapper
WpHole else Coercion -> HsWrapper
WpMultCoercion Coercion
coercion }
tc_sub_type_ds :: (TcType -> TcType -> TcM TcCoercionN)
-> CtOrigin
-> UserTypeCtxt
-> TcSigmaType
-> TcRhoType
-> TcM HsWrapper
tc_sub_type_ds :: (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_ds Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_actual Type
ty_expected
= do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type_ds" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_actual =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_actual
, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"ty_expected =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_expected ]
; Type -> Type -> TcM HsWrapper
go Type
ty_actual Type
ty_expected }
where
go :: Type -> Type -> TcM HsWrapper
go Type
ty_a Type
ty_e | Just Type
ty_a' <- Type -> Maybe Type
coreView Type
ty_a = Type -> Type -> TcM HsWrapper
go Type
ty_a' Type
ty_e
| Just Type
ty_e' <- Type -> Maybe Type
coreView Type
ty_e = Type -> Type -> TcM HsWrapper
go Type
ty_a Type
ty_e'
go (TyVarTy TcTyVar
tv_a) Type
ty_e
= do { Maybe Type
lookup_res <- TcTyVar -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv_a
; case Maybe Type
lookup_res of
Just Type
ty_a' ->
do { String -> SDoc -> TcM ()
traceTc String
"tc_sub_type_ds following filled meta-tyvar:"
(TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv_a SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"-->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_a')
; (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_ds Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
ty_a' Type
ty_e }
Maybe Type
Nothing -> Type -> Type -> TcM HsWrapper
just_unify Type
ty_actual Type
ty_expected }
go ty_a :: Type
ty_a@(FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af1, ft_mult :: Type -> Type
ft_mult = Type
act_mult, ft_arg :: Type -> Type
ft_arg = Type
act_arg, ft_res :: Type -> Type
ft_res = Type
act_res })
ty_e :: Type
ty_e@(FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af2, ft_mult :: Type -> Type
ft_mult = Type
exp_mult, ft_arg :: Type -> Type
ft_arg = Type
exp_arg, ft_res :: Type -> Type
ft_res = Type
exp_res })
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af1, FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af2
= if (Type -> Bool
isTauTy Type
ty_a Bool -> Bool -> Bool
&& Type -> Bool
isTauTy Type
ty_e)
then Type -> Type -> TcM HsWrapper
just_unify Type
ty_actual Type
ty_expected
else
do { HsWrapper
arg_wrap <- (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_deep Type -> Type -> TcM Coercion
unify CtOrigin
given_orig UserTypeCtxt
GenSigCtxt Type
exp_arg Type
act_arg
; HsWrapper
res_wrap <- (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_ds Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
act_res Type
exp_res
; HsWrapper
mult_wrap <- CtOrigin -> Type -> Type -> TcM HsWrapper
tcEqMult CtOrigin
inst_orig Type
act_mult Type
exp_mult
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
mult_wrap HsWrapper -> HsWrapper -> HsWrapper
<.>
HsWrapper -> HsWrapper -> Scaled Type -> Type -> HsWrapper
mkWpFun HsWrapper
arg_wrap HsWrapper
res_wrap (Type -> Type -> Scaled Type
forall a. Type -> a -> Scaled a
Scaled Type
exp_mult Type
exp_arg) Type
exp_res) }
where
given_orig :: CtOrigin
given_orig = SkolemInfoAnon -> CtOrigin
GivenOrigin (UserTypeCtxt -> Type -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
GenSigCtxt Type
exp_arg [])
go Type
ty_a Type
ty_e
| let ([TcTyVar]
tvs, ThetaType
theta, Type
_) = Type -> ([TcTyVar], ThetaType, Type)
tcSplitSigmaTy Type
ty_a
, Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= do { (HsWrapper
in_wrap, Type
in_rho) <- CtOrigin -> Type -> TcM (HsWrapper, Type)
topInstantiate CtOrigin
inst_orig Type
ty_a
; HsWrapper
body_wrap <- (Type -> Type -> TcM Coercion)
-> CtOrigin -> UserTypeCtxt -> Type -> Type -> TcM HsWrapper
tc_sub_type_ds Type -> Type -> TcM Coercion
unify CtOrigin
inst_orig UserTypeCtxt
ctxt Type
in_rho Type
ty_e
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
body_wrap HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
in_wrap) }
| Bool
otherwise
= do {
(HsWrapper
inst_wrap, Type
rho_a) <- CtOrigin -> Type -> TcM (HsWrapper, Type)
deeplyInstantiate CtOrigin
inst_orig Type
ty_actual
; HsWrapper
unify_wrap <- Type -> Type -> TcM HsWrapper
just_unify Type
rho_a Type
ty_expected
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
unify_wrap HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
inst_wrap) }
just_unify :: Type -> Type -> TcM HsWrapper
just_unify Type
ty_a Type
ty_e = do { Coercion
cow <- Type -> Type -> TcM Coercion
unify Type
ty_a Type
ty_e
; HsWrapper -> TcM HsWrapper
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> HsWrapper
mkWpCastN Coercion
cow) }
tcDeeplySkolemise
:: UserTypeCtxt -> TcSigmaType
-> (TcType -> TcM result)
-> TcM (HsWrapper, result)
tcDeeplySkolemise :: forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcDeeplySkolemise UserTypeCtxt
ctxt Type
expected_ty Type -> TcM result
thing_inside
| Type -> Bool
isTauTy Type
expected_ty
= do { result
res <- Type -> TcM result
thing_inside Type
expected_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, result
res) }
| Bool
otherwise
= do {
rec { (HsWrapper
wrap, [(Name, TcTyVar)]
tv_prs, [TcTyVar]
given, Type
rho_ty) <- SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
deeplySkolemise SkolemInfo
skol_info Type
expected_ty
; SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (UserTypeCtxt -> Type -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt Type
expected_ty [(Name, TcTyVar)]
tv_prs) }
; String -> SDoc -> TcM ()
traceTc String
"tcDeeplySkolemise" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
expected_ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rho_ty SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [(Name, TcTyVar)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Name, TcTyVar)]
tv_prs)
; let skol_tvs :: [TcTyVar]
skol_tvs = ((Name, TcTyVar) -> TcTyVar) -> [(Name, TcTyVar)] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TcTyVar) -> TcTyVar
forall a b. (a, b) -> b
snd [(Name, TcTyVar)]
tv_prs
; (TcEvBinds
ev_binds, result
result)
<- SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
skol_tvs [TcTyVar]
given (TcM result -> TcM (TcEvBinds, result))
-> TcM result -> TcM (TcEvBinds, result)
forall a b. (a -> b) -> a -> b
$
Type -> TcM result
thing_inside Type
rho_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> TcEvBinds -> HsWrapper
mkWpLet TcEvBinds
ev_binds, result
result) }
deeplySkolemise :: SkolemInfo -> TcSigmaType
-> TcM ( HsWrapper
, [(Name,TyVar)]
, [EvVar]
, TcRhoType )
deeplySkolemise :: SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
deeplySkolemise SkolemInfo
skol_info Type
ty
= Subst
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
go Subst
init_subst Type
ty
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty))
go :: Subst
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
go Subst
subst Type
ty
| Just ([Scaled Type]
arg_tys, [TcTyVar]
tvs, ThetaType
theta, Type
ty') <- Type -> Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
tcDeepSplitSigmaTy_maybe Type
ty
= do { let arg_tys' :: [Scaled Type]
arg_tys' = (() :: Constraint) => Subst -> [Scaled Type] -> [Scaled Type]
Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys Subst
subst [Scaled Type]
arg_tys
; [TcTyVar]
ids1 <- FastString -> [Scaled Type] -> TcRnIf TcGblEnv TcLclEnv [TcTyVar]
forall gbl lcl.
FastString -> [Scaled Type] -> TcRnIf gbl lcl [TcTyVar]
newSysLocalIds (String -> FastString
fsLit String
"dk") [Scaled Type]
arg_tys'
; (Subst
subst', [TcTyVar]
tvs1) <- SkolemInfo -> Subst -> [TcTyVar] -> TcM (Subst, [TcTyVar])
tcInstSkolTyVarsX SkolemInfo
skol_info Subst
subst [TcTyVar]
tvs
; [TcTyVar]
ev_vars1 <- ThetaType -> TcRnIf TcGblEnv TcLclEnv [TcTyVar]
newEvVars ((() :: Constraint) => Subst -> ThetaType -> ThetaType
Subst -> ThetaType -> ThetaType
substTheta Subst
subst' ThetaType
theta)
; (HsWrapper
wrap, [(Name, TcTyVar)]
tvs_prs2, [TcTyVar]
ev_vars2, Type
rho) <- Subst
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
go Subst
subst' Type
ty'
; let tv_prs1 :: [(Name, TcTyVar)]
tv_prs1 = (TcTyVar -> Name) -> [TcTyVar] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map TcTyVar -> Name
tyVarName [TcTyVar]
tvs [Name] -> [TcTyVar] -> [(Name, TcTyVar)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [TcTyVar]
tvs1
; (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
-> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [TcTyVar] -> HsWrapper -> HsWrapper
mkWpEta [TcTyVar]
ids1 ([TcTyVar] -> HsWrapper
mkWpTyLams [TcTyVar]
tvs1
HsWrapper -> HsWrapper -> HsWrapper
<.> [TcTyVar] -> HsWrapper
mkWpEvLams [TcTyVar]
ev_vars1
HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap)
, [(Name, TcTyVar)]
tv_prs1 [(Name, TcTyVar)] -> [(Name, TcTyVar)] -> [(Name, TcTyVar)]
forall a. [a] -> [a] -> [a]
++ [(Name, TcTyVar)]
tvs_prs2
, [TcTyVar]
ev_vars1 [TcTyVar] -> [TcTyVar] -> [TcTyVar]
forall a. [a] -> [a] -> [a]
++ [TcTyVar]
ev_vars2
, [Scaled Type] -> Type -> Type
(() :: Constraint) => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
arg_tys' Type
rho ) }
| Bool
otherwise
= (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
-> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, [], [], (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty)
deeplyInstantiate :: CtOrigin -> TcType -> TcM (HsWrapper, Type)
deeplyInstantiate :: CtOrigin -> Type -> TcM (HsWrapper, Type)
deeplyInstantiate CtOrigin
orig Type
ty
= Subst -> Type -> TcM (HsWrapper, Type)
go Subst
init_subst Type
ty
where
init_subst :: Subst
init_subst = InScopeSet -> Subst
mkEmptySubst (VarSet -> InScopeSet
mkInScopeSet (Type -> VarSet
tyCoVarsOfType Type
ty))
go :: Subst -> Type -> TcM (HsWrapper, Type)
go Subst
subst Type
ty
| Just ([Scaled Type]
arg_tys, [TcTyVar]
tvs, ThetaType
theta, Type
rho) <- Type -> Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
tcDeepSplitSigmaTy_maybe Type
ty
= do { (Subst
subst', [TcTyVar]
tvs') <- Subst -> [TcTyVar] -> TcM (Subst, [TcTyVar])
newMetaTyVarsX Subst
subst [TcTyVar]
tvs
; let arg_tys' :: [Scaled Type]
arg_tys' = (() :: Constraint) => Subst -> [Scaled Type] -> [Scaled Type]
Subst -> [Scaled Type] -> [Scaled Type]
substScaledTys Subst
subst' [Scaled Type]
arg_tys
theta' :: ThetaType
theta' = (() :: Constraint) => Subst -> ThetaType -> ThetaType
Subst -> ThetaType -> ThetaType
substTheta Subst
subst' ThetaType
theta
; [TcTyVar]
ids1 <- FastString -> [Scaled Type] -> TcRnIf TcGblEnv TcLclEnv [TcTyVar]
forall gbl lcl.
FastString -> [Scaled Type] -> TcRnIf gbl lcl [TcTyVar]
newSysLocalIds (String -> FastString
fsLit String
"di") [Scaled Type]
arg_tys'
; HsWrapper
wrap1 <- CtOrigin -> ThetaType -> ThetaType -> TcM HsWrapper
instCall CtOrigin
orig ([TcTyVar] -> ThetaType
mkTyVarTys [TcTyVar]
tvs') ThetaType
theta'
; (HsWrapper
wrap2, Type
rho2) <- Subst -> Type -> TcM (HsWrapper, Type)
go Subst
subst' Type
rho
; (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TcTyVar] -> HsWrapper -> HsWrapper
mkWpEta [TcTyVar]
ids1 (HsWrapper
wrap2 HsWrapper -> HsWrapper -> HsWrapper
<.> HsWrapper
wrap1),
[Scaled Type] -> Type -> Type
(() :: Constraint) => [Scaled Type] -> Type -> Type
mkScaledFunTys [Scaled Type]
arg_tys' Type
rho2) }
| Bool
otherwise
= do { let ty' :: Type
ty' = (() :: Constraint) => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst Type
ty
; (HsWrapper, Type) -> TcM (HsWrapper, Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, Type
ty') }
tcDeepSplitSigmaTy_maybe
:: TcSigmaType -> Maybe ([Scaled TcType], [TyVar], ThetaType, TcSigmaType)
tcDeepSplitSigmaTy_maybe :: Type -> Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
tcDeepSplitSigmaTy_maybe Type
ty
| Just (Scaled Type
arg_ty, Type
res_ty) <- Type -> Maybe (Scaled Type, Type)
tcSplitFunTy_maybe Type
ty
, Just ([Scaled Type]
arg_tys, [TcTyVar]
tvs, ThetaType
theta, Type
rho) <- Type -> Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
tcDeepSplitSigmaTy_maybe Type
res_ty
= ([Scaled Type], [TcTyVar], ThetaType, Type)
-> Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
forall a. a -> Maybe a
Just (Scaled Type
arg_tyScaled Type -> [Scaled Type] -> [Scaled Type]
forall a. a -> [a] -> [a]
:[Scaled Type]
arg_tys, [TcTyVar]
tvs, ThetaType
theta, Type
rho)
| ([TcTyVar]
tvs, ThetaType
theta, Type
rho) <- Type -> ([TcTyVar], ThetaType, Type)
tcSplitSigmaTy Type
ty
, Bool -> Bool
not ([TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= ([Scaled Type], [TcTyVar], ThetaType, Type)
-> Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
forall a. a -> Maybe a
Just ([], [TcTyVar]
tvs, ThetaType
theta, Type
rho)
| Bool
otherwise = Maybe ([Scaled Type], [TcTyVar], ThetaType, Type)
forall a. Maybe a
Nothing
tcTopSkolemise, tcSkolemiseScoped
:: UserTypeCtxt -> TcSigmaType
-> (TcType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseScoped :: forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcSkolemiseScoped UserTypeCtxt
ctxt Type
expected_ty Type -> TcM result
thing_inside
= do { Bool
deep_subsumption <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DeepSubsumption
; let skolemise :: SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
skolemise | Bool
deep_subsumption = SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
deeplySkolemise
| Bool
otherwise = SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
topSkolemise
;
rec { (HsWrapper
wrap, [(Name, TcTyVar)]
tv_prs, [TcTyVar]
given, Type
rho_ty) <- SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
skolemise SkolemInfo
skol_info Type
expected_ty
; SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (UserTypeCtxt -> Type -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt Type
expected_ty [(Name, TcTyVar)]
tv_prs) }
; let skol_tvs :: [TcTyVar]
skol_tvs = ((Name, TcTyVar) -> TcTyVar) -> [(Name, TcTyVar)] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TcTyVar) -> TcTyVar
forall a b. (a, b) -> b
snd [(Name, TcTyVar)]
tv_prs
; (TcEvBinds
ev_binds, result
res)
<- SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
skol_tvs [TcTyVar]
given (TcM result -> TcM (TcEvBinds, result))
-> TcM result -> TcM (TcEvBinds, result)
forall a b. (a -> b) -> a -> b
$
[(Name, TcTyVar)] -> TcM result -> TcM result
forall r. [(Name, TcTyVar)] -> TcM r -> TcM r
tcExtendNameTyVarEnv [(Name, TcTyVar)]
tv_prs (TcM result -> TcM result) -> TcM result -> TcM result
forall a b. (a -> b) -> a -> b
$
Type -> TcM result
thing_inside Type
rho_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> TcEvBinds -> HsWrapper
mkWpLet TcEvBinds
ev_binds, result
res) }
tcTopSkolemise :: forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcTopSkolemise UserTypeCtxt
ctxt Type
expected_ty Type -> TcM result
thing_inside
| Type -> Bool
isRhoTy Type
expected_ty
= do { result
res <- Type -> TcM result
thing_inside Type
expected_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
idHsWrapper, result
res) }
| Bool
otherwise
= do {
rec { (HsWrapper
wrap, [(Name, TcTyVar)]
tv_prs, [TcTyVar]
given, Type
rho_ty) <- SkolemInfo
-> Type -> TcM (HsWrapper, [(Name, TcTyVar)], [TcTyVar], Type)
topSkolemise SkolemInfo
skol_info Type
expected_ty
; SkolemInfo
skol_info <- SkolemInfoAnon -> IOEnv (Env TcGblEnv TcLclEnv) SkolemInfo
forall (m :: * -> *). MonadIO m => SkolemInfoAnon -> m SkolemInfo
mkSkolemInfo (UserTypeCtxt -> Type -> [(Name, TcTyVar)] -> SkolemInfoAnon
SigSkol UserTypeCtxt
ctxt Type
expected_ty [(Name, TcTyVar)]
tv_prs) }
; let skol_tvs :: [TcTyVar]
skol_tvs = ((Name, TcTyVar) -> TcTyVar) -> [(Name, TcTyVar)] -> [TcTyVar]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TcTyVar) -> TcTyVar
forall a b. (a, b) -> b
snd [(Name, TcTyVar)]
tv_prs
; (TcEvBinds
ev_binds, result
result)
<- SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
forall result.
SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints (SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info) [TcTyVar]
skol_tvs [TcTyVar]
given (TcM result -> TcM (TcEvBinds, result))
-> TcM result -> TcM (TcEvBinds, result)
forall a b. (a -> b) -> a -> b
$
Type -> TcM result
thing_inside Type
rho_ty
; (HsWrapper, result) -> TcM (HsWrapper, result)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper
wrap HsWrapper -> HsWrapper -> HsWrapper
<.> TcEvBinds -> HsWrapper
mkWpLet TcEvBinds
ev_binds, result
result) }
tcSkolemiseExpType :: UserTypeCtxt -> ExpSigmaType
-> (ExpRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseExpType :: forall result.
UserTypeCtxt
-> ExpRhoType
-> (ExpRhoType -> TcM result)
-> TcM (HsWrapper, result)
tcSkolemiseExpType UserTypeCtxt
_ et :: ExpRhoType
et@(Infer {}) ExpRhoType -> TcM result
thing_inside
= (HsWrapper
idHsWrapper, ) (result -> (HsWrapper, result))
-> TcM result -> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExpRhoType -> TcM result
thing_inside ExpRhoType
et
tcSkolemiseExpType UserTypeCtxt
ctxt (Check Type
ty) ExpRhoType -> TcM result
thing_inside
= do { Bool
deep_subsumption <- Extension -> TcRnIf TcGblEnv TcLclEnv Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.DeepSubsumption
; let skolemise :: UserTypeCtxt
-> Type
-> (Type -> TcM result)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result)
skolemise | Bool
deep_subsumption = UserTypeCtxt
-> Type
-> (Type -> TcM result)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result)
forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcDeeplySkolemise
| Bool
otherwise = UserTypeCtxt
-> Type
-> (Type -> TcM result)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result)
forall result.
UserTypeCtxt
-> Type -> (Type -> TcM result) -> TcM (HsWrapper, result)
tcTopSkolemise
; UserTypeCtxt
-> Type
-> (Type -> TcM result)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result)
skolemise UserTypeCtxt
ctxt Type
ty ((Type -> TcM result)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result))
-> (Type -> TcM result)
-> IOEnv (Env TcGblEnv TcLclEnv) (HsWrapper, result)
forall a b. (a -> b) -> a -> b
$ \Type
rho_ty ->
ExpRhoType -> TcM result
thing_inside (Type -> ExpRhoType
mkCheckExpType Type
rho_ty) }
checkConstraints :: SkolemInfoAnon
-> [TcTyVar]
-> [EvVar]
-> TcM result
-> TcM (TcEvBinds, result)
checkConstraints :: forall result.
SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcM result -> TcM (TcEvBinds, result)
checkConstraints SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given TcM result
thing_inside
= do { Bool
implication_needed <- SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcRnIf TcGblEnv TcLclEnv Bool
implicationNeeded SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
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
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given WantedConstraints
wanted
; String -> SDoc -> TcM ()
traceTc String
"checkConstraints" (TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ [TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs)
; Bag Implication -> TcM ()
emitImplications Bag Implication
implics
; (TcEvBinds, result) -> TcM (TcEvBinds, result)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcEvBinds
emptyTcEvBinds, result
res) } }
checkTvConstraints :: SkolemInfo
-> [TcTyVar]
-> TcM result
-> TcM result
checkTvConstraints :: forall result. SkolemInfo -> [TcTyVar] -> TcM result -> TcM result
checkTvConstraints SkolemInfo
skol_info [TcTyVar]
skol_tvs TcM result
thing_inside
= do { (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 -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; result -> TcM result
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return result
result }
emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM ()
emitResidualTvConstraint SkolemInfo
skol_info [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
| Bool -> Bool
not (WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted) Bool -> Bool -> Bool
||
SkolemInfoAnon -> Bool
checkTelescopeSkol SkolemInfoAnon
skol_info_anon
=
do { Implication
implic <- SkolemInfoAnon
-> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfoAnon
skol_info_anon [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
; Implication -> TcM ()
emitImplication Implication
implic }
| Bool
otherwise
= () -> TcM ()
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
skol_info_anon :: SkolemInfoAnon
skol_info_anon = SkolemInfo -> SkolemInfoAnon
getSkolemInfo SkolemInfo
skol_info
buildTvImplication :: SkolemInfoAnon -> [TcTyVar]
-> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication :: SkolemInfoAnon
-> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication
buildTvImplication SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs TcLevel
tclvl WantedConstraints
wanted
= Bool -> SDoc -> TcM Implication -> TcM Implication
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((TcTyVar -> Bool) -> [TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Bool
isSkolemTyVar (TcTyVar -> Bool) -> (TcTyVar -> Bool) -> TcTyVar -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> TcTyVar -> Bool
isTyVarTyVar) [TcTyVar]
skol_tvs) ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs) (TcM Implication -> TcM Implication)
-> TcM Implication -> TcM Implication
forall a b. (a -> b) -> a -> b
$
do { EvBindsVar
ev_binds <- TcM EvBindsVar
newNoTcEvBinds
; Implication
implic <- TcM Implication
newImplication
; let implic' :: Implication
implic' = Implication
implic { ic_tclvl = tclvl
, ic_skols = skol_tvs
, ic_given_eqs = NoGivenEqs
, ic_wanted = wanted
, ic_binds = ev_binds
, ic_info = skol_info }
; Implication -> TcM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Implication -> m ()
checkImplicationInvariants Implication
implic'
; Implication -> TcM Implication
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Implication
implic' }
implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
implicationNeeded :: SkolemInfoAnon
-> [TcTyVar] -> [TcTyVar] -> TcRnIf TcGblEnv TcLclEnv Bool
implicationNeeded SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given
| [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
skol_tvs
, [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
given
, Bool -> Bool
not (SkolemInfoAnon -> Bool
alwaysBuildImplication SkolemInfoAnon
skol_info)
=
do { TcLevel
tc_lvl <- TcM TcLevel
getTcLevel
; if Bool -> Bool
not (TcLevel -> Bool
isTopTcLevel TcLevel
tc_lvl)
then Bool -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 -> TcRnIf TcGblEnv TcLclEnv Bool
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
alwaysBuildImplication :: SkolemInfoAnon -> Bool
alwaysBuildImplication :: SkolemInfoAnon -> Bool
alwaysBuildImplication SkolemInfoAnon
_ = Bool
False
buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar]
-> [EvVar] -> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor :: TcLevel
-> SkolemInfoAnon
-> [TcTyVar]
-> [TcTyVar]
-> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
buildImplicationFor TcLevel
tclvl SkolemInfoAnon
skol_info [TcTyVar]
skol_tvs [TcTyVar]
given WantedConstraints
wanted
| WantedConstraints -> Bool
isEmptyWC WantedConstraints
wanted Bool -> Bool -> Bool
&& [TcTyVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TcTyVar]
given
= (Bag Implication, TcEvBinds) -> TcM (Bag Implication, TcEvBinds)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag Implication
forall a. Bag a
emptyBag, TcEvBinds
emptyTcEvBinds)
| Bool
otherwise
= Bool
-> SDoc
-> TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds)
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr ((TcTyVar -> Bool) -> [TcTyVar] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TcTyVar -> Bool
isSkolemTyVar (TcTyVar -> Bool) -> (TcTyVar -> Bool) -> TcTyVar -> Bool
forall (f :: * -> *). Applicative f => f Bool -> f Bool -> f Bool
<||> TcTyVar -> Bool
isTyVarTyVar) [TcTyVar]
skol_tvs) ([TcTyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TcTyVar]
skol_tvs) (TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds))
-> TcM (Bag Implication, TcEvBinds)
-> TcM (Bag Implication, TcEvBinds)
forall a b. (a -> b) -> a -> b
$
do { EvBindsVar
ev_binds_var <- TcM EvBindsVar
newTcEvBinds
; Implication
implic <- TcM Implication
newImplication
; let implic' :: Implication
implic' = Implication
implic { ic_tclvl = tclvl
, ic_skols = skol_tvs
, ic_given = given
, ic_wanted = wanted
, ic_binds = ev_binds_var
, ic_info = skol_info }
; Implication -> TcM ()
forall (m :: * -> *).
(HasCallStack, Applicative m) =>
Implication -> m ()
checkImplicationInvariants Implication
implic'
; (Bag Implication, TcEvBinds) -> TcM (Bag Implication, TcEvBinds)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
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 -> Type -> Type -> TcM Coercion
unifyType Maybe TypedThing
thing Type
ty1 Type
ty2
= TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
TypeLevel CtOrigin
origin Type
ty1 Type
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: Type
uo_actual = Type
ty1
, uo_expected :: Type
uo_expected = Type
ty2
, uo_thing :: Maybe TypedThing
uo_thing = Maybe TypedThing
thing
, uo_visible :: Bool
uo_visible = Bool
True }
unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN
unifyTypeET :: Type -> Type -> TcM Coercion
unifyTypeET Type
ty1 Type
ty2
= TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
TypeLevel CtOrigin
origin Type
ty1 Type
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: Type
uo_actual = Type
ty2
, uo_expected :: Type
uo_expected = Type
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 -> Type -> Type -> TcM Coercion
unifyKind Maybe TypedThing
mb_thing Type
ty1 Type
ty2
= TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
KindLevel CtOrigin
origin Type
ty1 Type
ty2
where
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: Type
uo_actual = Type
ty1
, uo_expected :: Type
uo_expected = Type
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 -> Type -> Type -> TcM Coercion
uType_defer TypeOrKind
t_or_k CtOrigin
origin Type
ty1 Type
ty2
= do { Coercion
co <- CtOrigin -> TypeOrKind -> Role -> Type -> Type -> TcM Coercion
emitWantedEq CtOrigin
origin TypeOrKind
t_or_k Role
Nominal Type
ty1 Type
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
forall doc. IsDoc doc => [doc] -> doc
vcat [ Type -> SDoc
debugPprType Type
ty1
, Type -> SDoc
debugPprType Type
ty2
, CtOrigin -> SDoc
pprCtOrigin CtOrigin
origin
, SDoc
doc])
; String -> SDoc -> TcM ()
traceTc String
"utype_defer2" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
}
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co }
uType :: TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
orig_ty1 Type
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
forall doc. IsDoc doc => [doc] -> doc
vcat
[ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"tclvl" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> TcLevel -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcLevel
tclvl
, [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_ty1, String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"~", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_ty2]
, CtOrigin -> SDoc
pprCtOrigin CtOrigin
origin]
; Coercion
co <- Type -> Type -> TcM Coercion
go Type
orig_ty1 Type
orig_ty2
; if Coercion -> Bool
isReflCo Coercion
co
then String -> SDoc -> TcM ()
traceTc String
"u_tys yields no coercion" SDoc
forall doc. IsOutput doc => doc
Outputable.empty
else String -> SDoc -> TcM ()
traceTc String
"u_tys yields coercion:" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Coercion
co }
where
go :: TcType -> TcType -> TcM CoercionN
go :: Type -> Type -> TcM Coercion
go (CastTy Type
t1 Coercion
co1) Type
t2
= do { Coercion
co_tys <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
t1 Type
t2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
Nominal Type
t1 Coercion
co1 Coercion
co_tys) }
go Type
t1 (CastTy Type
t2 Coercion
co2)
= do { Coercion
co_tys <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
t1 Type
t2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
Nominal Type
t2 Coercion
co2 Coercion
co_tys) }
go (TyVarTy TcTyVar
tv1) Type
ty2
= do { Maybe Type
lookup_res <- TcTyVar -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv1
; case Maybe Type
lookup_res of
Just Type
ty1 -> do { String -> SDoc -> TcM ()
traceTc String
"found filled tyvar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1)
; Type -> Type -> TcM Coercion
go Type
ty1 Type
ty2 }
Maybe Type
Nothing -> CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar CtOrigin
origin TypeOrKind
t_or_k SwapFlag
NotSwapped TcTyVar
tv1 Type
ty2 }
go Type
ty1 (TyVarTy TcTyVar
tv2)
= do { Maybe Type
lookup_res <- TcTyVar -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
isFilledMetaTyVar_maybe TcTyVar
tv2
; case Maybe Type
lookup_res of
Just Type
ty2 -> do { String -> SDoc -> TcM ()
traceTc String
"found filled tyvar" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv2 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
":->" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
; Type -> Type -> TcM Coercion
go Type
ty1 Type
ty2 }
Maybe Type
Nothing -> CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar CtOrigin
origin TypeOrKind
t_or_k SwapFlag
IsSwapped TcTyVar
tv2 Type
ty1 }
go ty1 :: Type
ty1@(TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Type -> Coercion
mkNomReflCo Type
ty1
go Type
ty1 Type
ty2
| Just Type
ty1' <- Type -> Maybe Type
coreView Type
ty1 = Type -> Type -> TcM Coercion
go Type
ty1' Type
ty2
| Just Type
ty2' <- Type -> Maybe Type
coreView Type
ty2 = Type -> Type -> TcM Coercion
go Type
ty1 Type
ty2'
go (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af1, ft_mult :: Type -> Type
ft_mult = Type
w1, ft_arg :: Type -> Type
ft_arg = Type
arg1, ft_res :: Type -> Type
ft_res = Type
res1 })
(FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af2, ft_mult :: Type -> Type
ft_mult = Type
w2, ft_arg :: Type -> Type
ft_arg = Type
arg2, ft_res :: Type -> Type
ft_res = Type
res2 })
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af1, FunTyFlag
af1 FunTyFlag -> FunTyFlag -> Bool
forall a. Eq a => a -> a -> Bool
== FunTyFlag
af2
= do { Coercion
co_l <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
arg1 Type
arg2
; Coercion
co_r <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
res1 Type
res2
; Coercion
co_w <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
w1 Type
w2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkNakedFunCo1 Role
Nominal FunTyFlag
af1 Coercion
co_w Coercion
co_l Coercion
co_r }
go ty1 :: Type
ty1@(TyConApp TyCon
tc1 ThetaType
_) Type
ty2
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1 = Type -> Type -> TcM Coercion
defer Type
ty1 Type
ty2
go Type
ty1 ty2 :: Type
ty2@(TyConApp TyCon
tc2 ThetaType
_)
| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc2 = Type -> Type -> TcM Coercion
defer Type
ty1 Type
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 Coercion -> TcM Coercion
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 Coercion -> TcM Coercion) -> TcM Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$
do { [Coercion]
cos <- (CtOrigin -> Type -> Type -> TcM Coercion)
-> [CtOrigin]
-> ThetaType
-> ThetaType
-> IOEnv (Env TcGblEnv TcLclEnv) [Coercion]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M (TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k) [CtOrigin]
origins' ThetaType
tys1 ThetaType
tys2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ (() :: Constraint) => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc1 [Coercion]
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 :: Type
ty@(LitTy TyLit
n)
| TyLit
m TyLit -> TyLit -> Bool
forall a. Eq a => a -> a -> Bool
== TyLit
n
= Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Type -> Coercion
mkNomReflCo Type
ty
go (AppTy Type
s1 Type
t1) (AppTy Type
s2 Type
t2)
= Bool -> Type -> Type -> Type -> Type -> TcM Coercion
go_app (Type -> Bool
isNextArgVisible Type
s1) Type
s1 Type
t1 Type
s2 Type
t2
go (AppTy Type
s1 Type
t1) (TyConApp TyCon
tc2 ThetaType
ts2)
| Just (ThetaType
ts2', Type
t2') <- ThetaType -> Maybe (ThetaType, Type)
forall a. [a] -> Maybe ([a], a)
snocView ThetaType
ts2
= Bool -> TcM Coercion -> TcM Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc2)) (TcM Coercion -> TcM Coercion) -> TcM Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$
Bool -> Type -> Type -> Type -> Type -> TcM Coercion
go_app (TyCon -> ThetaType -> Bool
isNextTyConArgVisible TyCon
tc2 ThetaType
ts2') Type
s1 Type
t1 (TyCon -> ThetaType -> Type
TyConApp TyCon
tc2 ThetaType
ts2') Type
t2'
go (TyConApp TyCon
tc1 ThetaType
ts1) (AppTy Type
s2 Type
t2)
| Just (ThetaType
ts1', Type
t1') <- ThetaType -> Maybe (ThetaType, Type)
forall a. [a] -> Maybe ([a], a)
snocView ThetaType
ts1
= Bool -> TcM Coercion -> TcM Coercion
forall a. HasCallStack => Bool -> a -> a
assert (Bool -> Bool
not (TyCon -> Bool
tyConMustBeSaturated TyCon
tc1)) (TcM Coercion -> TcM Coercion) -> TcM Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$
Bool -> Type -> Type -> Type -> Type -> TcM Coercion
go_app (TyCon -> ThetaType -> Bool
isNextTyConArgVisible TyCon
tc1 ThetaType
ts1') (TyCon -> ThetaType -> Type
TyConApp TyCon
tc1 ThetaType
ts1') Type
t1' Type
s2 Type
t2
go (CoercionTy Coercion
co1) (CoercionTy Coercion
co2)
= do { let ty1 :: Type
ty1 = Coercion -> Type
coercionType Coercion
co1
ty2 :: Type
ty2 = Coercion -> Type
coercionType Coercion
co2
; Coercion
kco <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
KindLevel
(Type -> Type -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin Type
orig_ty1 Type
orig_ty2 CtOrigin
origin
(TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
t_or_k))
Type
ty1 Type
ty2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kco Coercion
co1 Coercion
co2 }
go Type
ty1 Type
ty2 = Type -> Type -> TcM Coercion
defer Type
ty1 Type
ty2
defer :: Type -> Type -> TcM Coercion
defer Type
ty1 Type
ty2
| Type
ty1 (() :: Constraint) => Type -> Type -> Bool
Type -> Type -> Bool
`tcEqType` Type
ty2 = Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
ty1)
| Bool
otherwise = TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType_defer TypeOrKind
t_or_k CtOrigin
origin Type
ty1 Type
ty2
go_app :: Bool -> Type -> Type -> Type -> Type -> TcM Coercion
go_app Bool
vis Type
s1 Type
t1 Type
s2 Type
t2
= do { Coercion
co_s <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
origin Type
s1 Type
s2
; let arg_origin :: CtOrigin
arg_origin
| Bool
vis = CtOrigin
origin
| Bool
otherwise = CtOrigin -> CtOrigin
toInvisibleOrigin CtOrigin
origin
; Coercion
co_t <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
t_or_k CtOrigin
arg_origin Type
t1 Type
t2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> TcM Coercion) -> Coercion -> TcM Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion -> Coercion
mkAppCo Coercion
co_s Coercion
co_t }
uUnfilledVar :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM Coercion
uUnfilledVar :: CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped TcTyVar
tv1 Type
ty2
= do { Type
ty2 <- Type -> TcM Type
zonkTcType Type
ty2
; CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar1 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped TcTyVar
tv1 Type
ty2 }
uUnfilledVar1 :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM Coercion
uUnfilledVar1 :: CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar1 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped TcTyVar
tv1 Type
ty2
| Just TcTyVar
tv2 <- Type -> Maybe TcTyVar
getTyVar_maybe Type
ty2
= TcTyVar -> TcM Coercion
go TcTyVar
tv2
| Bool
otherwise
= CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped TcTyVar
tv1 Type
ty2
where
go :: TcTyVar -> TcM Coercion
go TcTyVar
tv2 | TcTyVar
tv1 TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv2
= Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo (TcTyVar -> Type
mkTyVarTy TcTyVar
tv1))
| Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars Bool
False TcTyVar
tv1 TcTyVar
tv2
= do { TcTyVar
tv1 <- TcTyVar -> TcM TcTyVar
zonkTyCoVarKind TcTyVar
tv1
; CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k (SwapFlag -> SwapFlag
flipSwap SwapFlag
swapped)
TcTyVar
tv2 (TcTyVar -> Type
mkTyVarTy TcTyVar
tv1) }
| Bool
otherwise
= CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped TcTyVar
tv1 Type
ty2
uUnfilledVar2 :: CtOrigin
-> TypeOrKind
-> SwapFlag
-> TcTyVar
-> TcTauType
-> TcM Coercion
uUnfilledVar2 :: CtOrigin
-> TypeOrKind -> SwapFlag -> TcTyVar -> Type -> TcM Coercion
uUnfilledVar2 CtOrigin
origin TypeOrKind
t_or_k SwapFlag
swapped TcTyVar
tv1 Type
ty2
= do { TcLevel
cur_lvl <- TcM TcLevel
getTcLevel
; TcLevel -> TcM Coercion
go TcLevel
cur_lvl }
where
go :: TcLevel -> TcM Coercion
go TcLevel
cur_lvl
| TcLevel -> TcTyVar -> Bool
isTouchableMetaTyVar TcLevel
cur_lvl TcTyVar
tv1
, CheckTyEqResult -> Bool
cterHasNoProblem (TcTyVar -> Type -> CheckTyEqResult
checkTyVarEq TcTyVar
tv1 Type
ty2)
= do { Maybe Type
mb_continue_solving <- MetaInfo -> Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
startSolvingByUnification (TcTyVar -> MetaInfo
metaTyVarInfo TcTyVar
tv1) Type
ty2
; case Maybe Type
mb_continue_solving of
{ Maybe Type
Nothing -> TcM Coercion
not_ok_so_defer
; Just Type
ty2 ->
do { Coercion
co_k <- TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType TypeOrKind
KindLevel CtOrigin
kind_origin ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty2) (TcTyVar -> Type
tyVarKind TcTyVar
tv1)
; String -> SDoc -> TcM ()
traceTc String
"uUnfilledVar2 ok" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcTyVar -> Type
tyVarKind TcTyVar
tv1)
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2 SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((() :: Constraint) => Type -> Type
Type -> Type
typeKind Type
ty2)
, Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Coercion -> Bool
isReflCo Coercion
co_k), Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co_k ]
; if Coercion -> Bool
isReflCo Coercion
co_k
then do { (() :: Constraint) => TcTyVar -> Type -> TcM ()
TcTyVar -> Type -> TcM ()
writeMetaTyVar TcTyVar
tv1 Type
ty2
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
ty2) }
else TcM Coercion
defer }}}
| Bool
otherwise
= TcM Coercion
not_ok_so_defer
ty1 :: Type
ty1 = TcTyVar -> Type
mkTyVarTy TcTyVar
tv1
kind_origin :: CtOrigin
kind_origin = Type -> Type -> CtOrigin -> Maybe TypeOrKind -> CtOrigin
KindEqOrigin Type
ty1 Type
ty2 CtOrigin
origin (TypeOrKind -> Maybe TypeOrKind
forall a. a -> Maybe a
Just TypeOrKind
t_or_k)
defer :: TcM Coercion
defer = SwapFlag
-> (Type -> Type -> TcM Coercion) -> Type -> Type -> TcM Coercion
forall a b. SwapFlag -> (a -> a -> b) -> a -> a -> b
unSwap SwapFlag
swapped (TypeOrKind -> CtOrigin -> Type -> Type -> TcM Coercion
uType_defer TypeOrKind
t_or_k CtOrigin
origin) Type
ty1 Type
ty2
not_ok_so_defer :: TcM Coercion
not_ok_so_defer =
do { String -> SDoc -> TcM ()
traceTc String
"uUnfilledVar2 not ok" (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv1 SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2)
; TcM Coercion
defer }
startSolvingByUnification :: MetaInfo -> TcType
-> TcM (Maybe TcType)
startSolvingByUnification :: MetaInfo -> Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
startSolvingByUnification MetaInfo
_ Type
xi
| Type -> Bool
hasCoercionHoleTy Type
xi
= Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
startSolvingByUnification MetaInfo
info Type
xi
= case MetaInfo
info of
MetaInfo
CycleBreakerTv -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
ConcreteTv ConcreteTvOrigin
conc_orig ->
do { (Type
xi, [NotConcreteReason]
not_conc_reasons) <- ConcreteTvOrigin -> Type -> TcM (Type, [NotConcreteReason])
makeTypeConcrete ConcreteTvOrigin
conc_orig Type
xi
; case [NotConcreteReason]
not_conc_reasons of
[] -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type))
-> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
xi
[NotConcreteReason]
_ -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing }
MetaInfo
TyVarTv ->
case Type -> Maybe TcTyVar
getTyVar_maybe Type
xi of
Maybe TcTyVar
Nothing -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
Just TcTyVar
tv ->
case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
SkolemTv {} -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type))
-> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
xi
TcTyVarDetails
RuntimeUnk -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type))
-> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
xi
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } ->
case MetaInfo
info of
MetaInfo
TyVarTv -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type))
-> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
xi
MetaInfo
_ -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Type
forall a. Maybe a
Nothing
MetaInfo
_ -> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type))
-> Maybe Type -> TcRnIf TcGblEnv TcLclEnv (Maybe Type)
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Type
forall a. a -> Maybe a
Just Type
xi
swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars Bool
is_given TcTyVar
tv1 TcTyVar
tv2
| Bool -> Bool
not Bool
is_given, Int
pri1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0, Int
pri2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Bool
True
| Bool -> Bool
not Bool
is_given, Int
pri2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0, Int
pri1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Bool
False
| TcLevel
lvl1 TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl2 = Bool
False
| TcLevel
lvl2 TcLevel -> TcLevel -> Bool
`strictlyDeeperThan` TcLevel
lvl1 = Bool
True
| Int
pri1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pri2 = Bool
False
| Int
pri2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pri1 = Bool
True
| Name -> Bool
isSystemName Name
tv2_name, Bool -> Bool
not (Name -> Bool
isSystemName Name
tv1_name) = Bool
True
| Bool
otherwise = Bool
False
where
lvl1 :: TcLevel
lvl1 = TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv1
lvl2 :: TcLevel
lvl2 = TcTyVar -> TcLevel
tcTyVarLevel TcTyVar
tv2
pri1 :: Int
pri1 = TcTyVar -> Int
lhsPriority TcTyVar
tv1
pri2 :: Int
pri2 = TcTyVar -> Int
lhsPriority TcTyVar
tv2
tv1_name :: Name
tv1_name = TcTyVar -> Name
Var.varName TcTyVar
tv1
tv2_name :: Name
tv2_name = TcTyVar -> Name
Var.varName TcTyVar
tv2
lhsPriority :: TcTyVar -> Int
lhsPriority :: TcTyVar -> Int
lhsPriority TcTyVar
tv
= Bool -> SDoc -> Int -> Int
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (TcTyVar -> Bool
isTyVar TcTyVar
tv) (TcTyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcTyVar
tv) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$
case TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv of
TcTyVarDetails
RuntimeUnk -> Int
0
SkolemTv {} -> Int
0
MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
info } -> case MetaInfo
info of
MetaInfo
CycleBreakerTv -> Int
0
MetaInfo
TyVarTv -> Int
1
ConcreteTv {} -> Int
2
MetaInfo
TauTv -> Int
3
MetaInfo
RuntimeUnkTv -> Int
4
matchExpectedFunKind
:: TypedThing
-> Arity
-> TcKind
-> TcM Coercion
matchExpectedFunKind :: TypedThing -> Int -> Type -> TcM Coercion
matchExpectedFunKind TypedThing
hs_ty Int
n Type
k = Int -> Type -> TcM Coercion
go Int
n Type
k
where
go :: Int -> Type -> TcM Coercion
go Int
0 Type
k = Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Coercion
mkNomReflCo Type
k)
go Int
n Type
k | Just Type
k' <- Type -> Maybe Type
coreView Type
k = Int -> Type -> TcM Coercion
go Int
n Type
k'
go Int
n k :: Type
k@(TyVarTy TcTyVar
kvar)
| TcTyVar -> Bool
isMetaTyVar TcTyVar
kvar
= do { MetaDetails
maybe_kind <- TcTyVar -> TcM MetaDetails
readMetaTyVar TcTyVar
kvar
; case MetaDetails
maybe_kind of
Indirect Type
fun_kind -> Int -> Type -> TcM Coercion
go Int
n Type
fun_kind
MetaDetails
Flexi -> Int -> Type -> TcM Coercion
defer Int
n Type
k }
go Int
n (FunTy { ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
arg, ft_res :: Type -> Type
ft_res = Type
res })
| FunTyFlag -> Bool
isVisibleFunArg FunTyFlag
af
= do { Coercion
co <- Int -> Type -> TcM Coercion
go (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Type
res
; Coercion -> TcM Coercion
forall a. a -> IOEnv (Env TcGblEnv TcLclEnv) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> FunTyFlag -> Coercion -> Coercion -> Coercion -> Coercion
mkNakedFunCo1 Role
Nominal FunTyFlag
af (Type -> Coercion
mkNomReflCo Type
w) (Type -> Coercion
mkNomReflCo Type
arg) Coercion
co) }
go Int
n Type
other
= Int -> Type -> TcM Coercion
defer Int
n Type
other
defer :: Int -> Type -> TcM Coercion
defer Int
n Type
k
= do { ThetaType
arg_kinds <- Int -> TcM ThetaType
newMetaKindVars Int
n
; Type
res_kind <- TcM Type
newMetaKindVar
; let new_fun :: Type
new_fun = ThetaType -> Type -> Type
mkVisFunTysMany ThetaType
arg_kinds Type
res_kind
origin :: CtOrigin
origin = TypeEqOrigin { uo_actual :: Type
uo_actual = Type
k
, uo_expected :: Type
uo_expected = Type
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 -> Type -> Type -> TcM Coercion
uType TypeOrKind
KindLevel CtOrigin
origin Type
k Type
new_fun }
{-# NOINLINE checkTyVarEq #-}
checkTyVarEq :: TcTyVar -> TcType -> CheckTyEqResult
checkTyVarEq :: TcTyVar -> Type -> CheckTyEqResult
checkTyVarEq TcTyVar
tv Type
ty
= (CanEqLHS -> Type -> CheckTyEqResult)
-> CanEqLHS -> Type -> CheckTyEqResult
forall a. a -> a
inline CanEqLHS -> Type -> CheckTyEqResult
checkTypeEq (TcTyVar -> CanEqLHS
TyVarLHS TcTyVar
tv) Type
ty
{-# NOINLINE checkTyFamEq #-}
checkTyFamEq :: TyCon
-> [TcType]
-> TcType
-> CheckTyEqResult
checkTyFamEq :: TyCon -> ThetaType -> Type -> CheckTyEqResult
checkTyFamEq TyCon
fun_tc ThetaType
fun_args Type
ty
= (CanEqLHS -> Type -> CheckTyEqResult)
-> CanEqLHS -> Type -> CheckTyEqResult
forall a. a -> a
inline CanEqLHS -> Type -> CheckTyEqResult
checkTypeEq (TyCon -> ThetaType -> CanEqLHS
TyFamLHS TyCon
fun_tc ThetaType
fun_args) Type
ty
CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
`cterRemoveProblem` CheckTyEqProblem
cteTypeFamily
checkTypeEq :: CanEqLHS -> TcType -> CheckTyEqResult
checkTypeEq :: CanEqLHS -> Type -> CheckTyEqResult
checkTypeEq CanEqLHS
lhs Type
ty
= Type -> CheckTyEqResult
go Type
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 TcTyVar
tv <- CanEqLHS
lhs
, MetaTv { mtv_info :: TcTyVarDetails -> MetaInfo
mtv_info = MetaInfo
RuntimeUnkTv } <- TcTyVar -> TcTyVarDetails
tcTyVarDetails TcTyVar
tv
= Bool
True
| Bool
otherwise
= Bool
False
go :: TcType -> CheckTyEqResult
go :: Type -> CheckTyEqResult
go (TyVarTy TcTyVar
tv') = TcTyVar -> CheckTyEqResult
go_tv TcTyVar
tv'
go (TyConApp TyCon
tc ThetaType
tys) = TyCon -> ThetaType -> CheckTyEqResult
go_tc TyCon
tc ThetaType
tys
go (LitTy {}) = CheckTyEqResult
cteOK
go (FunTy {ft_af :: Type -> FunTyFlag
ft_af = FunTyFlag
af, ft_mult :: Type -> Type
ft_mult = Type
w, ft_arg :: Type -> Type
ft_arg = Type
a, ft_res :: Type -> Type
ft_res = Type
r})
= Type -> CheckTyEqResult
go Type
w CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> Type -> CheckTyEqResult
go Type
a CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> Type -> CheckTyEqResult
go Type
r CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
if Bool -> Bool
not Bool
ghci_tv Bool -> Bool -> Bool
&& FunTyFlag -> Bool
isInvisibleFunArg FunTyFlag
af
then CheckTyEqResult
impredicative
else CheckTyEqResult
cteOK
go (AppTy Type
fun Type
arg) = Type -> CheckTyEqResult
go Type
fun CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> Type -> CheckTyEqResult
go Type
arg
go (CastTy Type
ty Coercion
co) = Type -> CheckTyEqResult
go Type
ty CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> Coercion -> CheckTyEqResult
go_co Coercion
co
go (CoercionTy Coercion
co) = Coercion -> CheckTyEqResult
go_co Coercion
co
go (ForAllTy (Bndr TcTyVar
tv' ForAllTyFlag
_) Type
ty) = (case CanEqLHS
lhs of
TyVarLHS TcTyVar
tv | TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv' -> Type -> CheckTyEqResult
go_occ (TcTyVar -> Type
tyVarKind TcTyVar
tv') CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> CheckTyEqResult -> CheckTyEqResult
cterClearOccursCheck (Type -> CheckTyEqResult
go Type
ty)
| Bool
otherwise -> Type -> CheckTyEqResult
go_occ (TcTyVar -> Type
tyVarKind TcTyVar
tv') CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> Type -> CheckTyEqResult
go Type
ty
CanEqLHS
_ -> Type -> CheckTyEqResult
go Type
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 :: TcTyVar -> CheckTyEqResult
go_tv = case CanEqLHS
lhs of
TyVarLHS TcTyVar
tv -> \ TcTyVar
tv' -> Type -> CheckTyEqResult
go_occ (TcTyVar -> Type
tyVarKind TcTyVar
tv') CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<>
if TcTyVar
tv TcTyVar -> TcTyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TcTyVar
tv' then CheckTyEqResult
insoluble_occurs else CheckTyEqResult
cteOK
TyFamLHS {} -> \ TcTyVar
_tv' -> CheckTyEqResult
cteOK
go_occ :: Type -> CheckTyEqResult
go_occ Type
k = CheckTyEqResult -> CheckTyEqResult
cterFromKind (CheckTyEqResult -> CheckTyEqResult)
-> CheckTyEqResult -> CheckTyEqResult
forall a b. (a -> b) -> a -> b
$ Type -> CheckTyEqResult
go Type
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 = (Type -> CheckTyEqResult) -> ThetaType -> CheckTyEqResult
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> CheckTyEqResult
go ThetaType
tys
| Bool
otherwise
= let (ThetaType
tf_args, ThetaType
non_tf_args) = Int -> ThetaType -> (ThetaType, ThetaType)
forall a. Int -> [a] -> ([a], [a])
splitAt (TyCon -> Int
tyConArity TyCon
tc) ThetaType
tys in
CheckTyEqResult -> CheckTyEqResult
cterSetOccursCheckSoluble ((Type -> CheckTyEqResult) -> ThetaType -> CheckTyEqResult
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> CheckTyEqResult
go ThetaType
tf_args) CheckTyEqResult -> CheckTyEqResult -> CheckTyEqResult
forall a. Semigroup a => a -> a -> a
S.<> (Type -> CheckTyEqResult) -> ThetaType -> CheckTyEqResult
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Type -> CheckTyEqResult
go ThetaType
non_tf_args
go_co :: Coercion -> CheckTyEqResult
go_co Coercion
co | TyVarLHS TcTyVar
tv <- CanEqLHS
lhs
, TcTyVar
tv TcTyVar -> VarSet -> Bool
`elemVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
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)