{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module GHC.Tc.Gen.App
( tcApp
, tcInferSigma
, tcValArg
, tcExprPrag ) where
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExprNC )
import GHC.Builtin.Types (multiplicityTy)
import GHC.Tc.Gen.Head
import GHC.Hs
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe )
import GHC.Tc.Gen.HsType
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType as TcType
import GHC.Core.TyCon
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst (substTyWithInScope)
import GHC.Core.TyCo.FVs( shallowTyCoVarsOfType )
import GHC.Core.Type
import GHC.Tc.Types.Evidence
import GHC.Types.Var.Set
import GHC.Builtin.PrimOps( tagToEnumKey )
import GHC.Builtin.Names
import GHC.Driver.Session
import GHC.Types.SrcLoc
import GHC.Types.Var.Env ( emptyTidyEnv, mkInScopeSet )
import GHC.Data.Maybe
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
import GHC.Utils.Panic
import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Data.Function
#include "GhclibHsVersions.h"
import GHC.Prelude
tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
tcInferSigma :: Bool -> LHsExpr GhcRn -> TcM TcSigmaType
tcInferSigma Bool
inst (L loc rn_expr)
| (HsExpr GhcRn
rn_fun, [HsExprArg 'TcpRn]
rn_args, Rebuilder
_) <- HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder)
splitHsApps HsExpr GhcRn
rn_expr
= HsExpr GhcRn -> TcM TcSigmaType -> TcM TcSigmaType
forall a. HsExpr GhcRn -> TcRn a -> TcRn a
addExprCtxt HsExpr GhcRn
rn_expr (TcM TcSigmaType -> TcM TcSigmaType)
-> TcM TcSigmaType -> TcM TcSigmaType
forall a b. (a -> b) -> a -> b
$
SrcSpan -> TcM TcSigmaType -> TcM TcSigmaType
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM TcSigmaType -> TcM TcSigmaType)
-> TcM TcSigmaType -> TcM TcSigmaType
forall a b. (a -> b) -> a -> b
$
do { Bool
do_ql <- HsExpr GhcRn -> TcM Bool
wantQuickLook HsExpr GhcRn
rn_fun
; (HsExpr GhcTc
tc_fun, TcSigmaType
fun_sigma) <- HsExpr GhcRn
-> [HsExprArg 'TcpRn]
-> Maybe TcSigmaType
-> TcM (HsExpr GhcTc, TcSigmaType)
tcInferAppHead HsExpr GhcRn
rn_fun [HsExprArg 'TcpRn]
rn_args Maybe TcSigmaType
forall a. Maybe a
Nothing
; (Delta
_delta, [HsExprArg 'TcpInst]
inst_args, TcSigmaType
app_res_sigma) <- Bool
-> Bool
-> HsExpr GhcRn
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
inst HsExpr GhcRn
rn_fun TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
; [HsExprArg 'TcpTc]
_tc_args <- Bool
-> HsExpr GhcTc -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql HsExpr GhcTc
tc_fun [HsExprArg 'TcpInst]
inst_args
; TcSigmaType -> TcM TcSigmaType
forall (m :: * -> *) a. Monad m => a -> m a
return TcSigmaType
app_res_sigma }
tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
tcApp HsExpr GhcRn
rn_expr ExpRhoType
exp_res_ty
| (HsExpr GhcRn
rn_fun, [HsExprArg 'TcpRn]
rn_args, Rebuilder
rebuild) <- HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder)
splitHsApps HsExpr GhcRn
rn_expr
= do { (HsExpr GhcTc
tc_fun, TcSigmaType
fun_sigma) <- HsExpr GhcRn
-> [HsExprArg 'TcpRn]
-> Maybe TcSigmaType
-> TcM (HsExpr GhcTc, TcSigmaType)
tcInferAppHead HsExpr GhcRn
rn_fun [HsExprArg 'TcpRn]
rn_args
(ExpRhoType -> Maybe TcSigmaType
checkingExpType_maybe ExpRhoType
exp_res_ty)
; Bool
do_ql <- HsExpr GhcRn -> TcM Bool
wantQuickLook HsExpr GhcRn
rn_fun
; (Delta
delta, [HsExprArg 'TcpInst]
inst_args, TcSigmaType
app_res_rho) <- Bool
-> Bool
-> HsExpr GhcRn
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
True HsExpr GhcRn
rn_fun TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
; Bool -> Delta -> TcSigmaType -> ExpRhoType -> TcM ()
quickLookResultType Bool
do_ql Delta
delta TcSigmaType
app_res_rho ExpRhoType
exp_res_ty
; 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 { [HsExprArg 'TcpInst]
inst_args <- (HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst))
-> [HsExprArg 'TcpInst]
-> IOEnv (Env TcGblEnv TcLclEnv) [HsExprArg 'TcpInst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst)
zonkArg [HsExprArg 'TcpInst]
inst_args
; String -> SDoc -> TcM ()
traceTc String
"tcApp" ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"rn_fun" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun
, String -> SDoc
text String
"inst_args" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
brackets ((HsExprArg 'TcpInst -> SDoc) -> [HsExprArg 'TcpInst] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas HsExprArg 'TcpInst -> SDoc
pprHsExprArgTc [HsExprArg 'TcpInst]
inst_args)
, String -> SDoc
text String
"do_ql: " SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
do_ql
, String -> SDoc
text String
"fun_sigma: " SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_sigma
, String -> SDoc
text String
"delta: " SDoc -> SDoc -> SDoc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
, String -> SDoc
text String
"app_res_rho:" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
app_res_rho
, String -> SDoc
text String
"exp_res_ty:" SDoc -> SDoc -> SDoc
<+> ExpRhoType -> SDoc
forall a. Outputable a => a -> SDoc
ppr ExpRhoType
exp_res_ty
, String -> SDoc
text String
"rn_expr:" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_expr ]) }
; [HsExprArg 'TcpTc]
tc_args <- Bool
-> HsExpr GhcTc -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql HsExpr GhcTc
tc_fun [HsExprArg 'TcpInst]
inst_args
; TcSigmaType
app_res_rho <- Bool -> TcSigmaType -> TcM TcSigmaType
zonkQuickLook Bool
do_ql TcSigmaType
app_res_rho
; if HsExpr GhcRn -> Bool
isTagToEnum HsExpr GhcRn
rn_fun
then HsExpr GhcRn
-> HsExpr GhcTc
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcRn
rn_expr HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args TcSigmaType
app_res_rho ExpRhoType
exp_res_ty
else
do {
; let tc_expr :: HsExpr GhcTc
tc_expr = Rebuilder
rebuild HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args
; HsExpr GhcTc
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
-> TcM (HsExpr GhcTc)
forall a.
HsExpr GhcTc
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM a
-> TcM a
addFunResCtxt HsExpr GhcTc
tc_fun [HsExprArg 'TcpTc]
tc_args TcSigmaType
app_res_rho ExpRhoType
exp_res_ty (TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc))
-> TcM (HsExpr GhcTc) -> TcM (HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
HsExpr GhcRn
-> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
rn_expr HsExpr GhcTc
tc_expr TcSigmaType
app_res_rho ExpRhoType
exp_res_ty } }
wantQuickLook :: HsExpr GhcRn -> TcM Bool
wantQuickLook :: HsExpr GhcRn -> TcM Bool
wantQuickLook (HsVar XVar GhcRn
_ LIdP GhcRn
f) | GenLocated SrcSpan Name -> Name
forall l e. GenLocated l e -> e
unLoc GenLocated SrcSpan Name
LIdP GhcRn
f Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
dollarIdKey = Bool -> TcM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
wantQuickLook HsExpr GhcRn
_ = Extension -> TcM Bool
forall gbl lcl. Extension -> TcRnIf gbl lcl Bool
xoptM Extension
LangExt.ImpredicativeTypes
zonkQuickLook :: Bool -> TcType -> TcM TcType
zonkQuickLook :: Bool -> TcSigmaType -> TcM TcSigmaType
zonkQuickLook Bool
do_ql TcSigmaType
ty
| Bool
do_ql = TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
ty
| Bool
otherwise = TcSigmaType -> TcM TcSigmaType
forall (m :: * -> *) a. Monad m => a -> m a
return TcSigmaType
ty
zonkArg :: HsExprArg 'TcpInst -> TcM (HsExprArg 'TcpInst)
zonkArg :: HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst)
zonkArg eva :: HsExprArg 'TcpInst
eva@(EValArg { eva_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
eva_arg_ty = Scaled m ty })
= do { TcSigmaType
ty' <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
ty
; HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExprArg 'TcpInst
eva { eva_arg_ty :: XEVAType 'TcpInst
eva_arg_ty = TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
m TcSigmaType
ty' }) }
zonkArg HsExprArg 'TcpInst
arg = HsExprArg 'TcpInst
-> IOEnv (Env TcGblEnv TcLclEnv) (HsExprArg 'TcpInst)
forall (m :: * -> *) a. Monad m => a -> m a
return HsExprArg 'TcpInst
arg
tcValArgs :: Bool
-> HsExpr GhcTc
-> [HsExprArg 'TcpInst]
-> TcM [HsExprArg 'TcpTc]
tcValArgs :: Bool
-> HsExpr GhcTc -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
do_ql HsExpr GhcTc
fun [HsExprArg 'TcpInst]
args
= Int -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
go Int
1 [HsExprArg 'TcpInst]
args
where
go :: Int -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
go Int
_ [] = [HsExprArg 'TcpTc] -> TcM [HsExprArg 'TcpTc]
forall (m :: * -> *) a. Monad m => a -> m a
return []
go Int
n (HsExprArg 'TcpInst
arg:[HsExprArg 'TcpInst]
args) = do { (Int
n',HsExprArg 'TcpTc
arg') <- Int -> HsExprArg 'TcpInst -> TcM (Int, HsExprArg 'TcpTc)
tc_arg Int
n HsExprArg 'TcpInst
arg
; [HsExprArg 'TcpTc]
args' <- Int -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
go Int
n' [HsExprArg 'TcpInst]
args
; [HsExprArg 'TcpTc] -> TcM [HsExprArg 'TcpTc]
forall (m :: * -> *) a. Monad m => a -> m a
return (HsExprArg 'TcpTc
arg' HsExprArg 'TcpTc -> [HsExprArg 'TcpTc] -> [HsExprArg 'TcpTc]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpTc]
args') }
tc_arg :: Int -> HsExprArg 'TcpInst -> TcM (Int, HsExprArg 'TcpTc)
tc_arg :: Int -> HsExprArg 'TcpInst -> TcM (Int, HsExprArg 'TcpTc)
tc_arg Int
n (EPar SrcSpan
l) = (Int, HsExprArg 'TcpTc) -> TcM (Int, HsExprArg 'TcpTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, SrcSpan -> HsExprArg 'TcpTc
forall (p :: TcPass). SrcSpan -> HsExprArg p
EPar SrcSpan
l)
tc_arg Int
n (EPrag SrcSpan
l HsPragE (GhcPass (XPass 'TcpInst))
p) = (Int, HsExprArg 'TcpTc) -> TcM (Int, HsExprArg 'TcpTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, SrcSpan -> HsPragE (GhcPass (XPass 'TcpTc)) -> HsExprArg 'TcpTc
forall (p :: TcPass).
SrcSpan -> HsPragE (GhcPass (XPass p)) -> HsExprArg p
EPrag SrcSpan
l (HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag HsPragE GhcRn
HsPragE (GhcPass (XPass 'TcpInst))
p))
tc_arg Int
n (EWrap XEWrap 'TcpInst
wrap) = (Int, HsExprArg 'TcpTc) -> TcM (Int, HsExprArg 'TcpTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
n, XEWrap 'TcpTc -> HsExprArg 'TcpTc
forall (p :: TcPass). XEWrap p -> HsExprArg p
EWrap XEWrap 'TcpInst
XEWrap 'TcpTc
wrap)
tc_arg Int
n (ETypeArg SrcSpan
l LHsWcType GhcRn
hs_ty XETAType 'TcpInst
ty) = (Int, HsExprArg 'TcpTc) -> TcM (Int, HsExprArg 'TcpTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, SrcSpan -> LHsWcType GhcRn -> XETAType 'TcpTc -> HsExprArg 'TcpTc
forall (p :: TcPass).
SrcSpan -> LHsWcType GhcRn -> XETAType p -> HsExprArg p
ETypeArg SrcSpan
l LHsWcType GhcRn
hs_ty XETAType 'TcpInst
XETAType 'TcpTc
ty)
tc_arg Int
n eva :: HsExprArg 'TcpInst
eva@(EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = EValArg 'TcpInst
arg, eva_arg_ty :: forall (p :: TcPass). HsExprArg p -> XEVAType p
eva_arg_ty = Scaled mult arg_ty })
= do {
TcSigmaType
arg_ty <- Bool -> TcSigmaType -> TcM TcSigmaType
zonkQuickLook Bool
do_ql TcSigmaType
arg_ty
; Located (HsExpr GhcTc)
arg' <- SDoc
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (HsExpr GhcTc -> Located (HsExpr GhcRn) -> Int -> SDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> SDoc
funAppCtxt HsExpr GhcTc
fun (EValArg 'TcpInst -> LHsExpr GhcRn
eValArgExpr EValArg 'TcpInst
arg) Int
n) (TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc)))
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
TcSigmaType
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a. TcSigmaType -> TcM a -> TcM a
tcScalingUsage TcSigmaType
mult (TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc)))
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"tcEValArg" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"of" SDoc -> SDoc -> SDoc
<+> HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
fun
, String -> SDoc
text String
"arg type:" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
arg_ty
, String -> SDoc
text String
"arg:" SDoc -> SDoc -> SDoc
<+> EValArg 'TcpInst -> SDoc
forall a. Outputable a => a -> SDoc
ppr EValArg 'TcpInst
arg ]
; EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
tcEValArg EValArg 'TcpInst
arg TcSigmaType
arg_ty }
; (Int, HsExprArg 'TcpTc) -> TcM (Int, HsExprArg 'TcpTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, HsExprArg 'TcpInst
eva { eva_arg :: EValArg 'TcpTc
eva_arg = LHsExpr (GhcPass (XPass 'TcpTc)) -> EValArg 'TcpTc
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg Located (HsExpr GhcTc)
LHsExpr (GhcPass (XPass 'TcpTc))
arg'
, eva_arg_ty :: XEVAType 'TcpTc
eva_arg_ty = TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
Scaled TcSigmaType
mult TcSigmaType
arg_ty }) }
tcEValArg :: EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
tcEValArg :: EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc)
tcEValArg (ValArg LHsExpr (GhcPass (XPass 'TcpInst))
arg) TcSigmaType
exp_arg_sigma
= LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTc)
tcCheckPolyExprNC LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpInst))
arg TcSigmaType
exp_arg_sigma
tcEValArg (ValArgQL { va_expr :: EValArg 'TcpInst -> LHsExpr GhcRn
va_expr = L loc _, va_fun :: EValArg 'TcpInst -> HsExpr GhcTc
va_fun = HsExpr GhcTc
fun, va_args :: EValArg 'TcpInst -> [HsExprArg 'TcpInst]
va_args = [HsExprArg 'TcpInst]
args
, va_ty :: EValArg 'TcpInst -> TcSigmaType
va_ty = TcSigmaType
app_res_rho, va_rebuild :: EValArg 'TcpInst -> Rebuilder
va_rebuild = Rebuilder
rebuild }) TcSigmaType
exp_arg_sigma
= SrcSpan
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc)))
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"tcEValArg {" ([SDoc] -> SDoc
vcat [ HsExpr GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcTc
fun SDoc -> SDoc -> SDoc
<+> [HsExprArg 'TcpInst] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpInst]
args ])
; [HsExprArg 'TcpTc]
tc_args <- Bool
-> HsExpr GhcTc -> [HsExprArg 'TcpInst] -> TcM [HsExprArg 'TcpTc]
tcValArgs Bool
True HsExpr GhcTc
fun [HsExprArg 'TcpInst]
args
; TcCoercionN
co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyType Maybe SDoc
forall a. Maybe a
Nothing TcSigmaType
app_res_rho TcSigmaType
exp_arg_sigma
; String -> SDoc -> TcM ()
traceTc String
"tcEValArg }" SDoc
empty
; Located (HsExpr GhcTc) -> TcM (Located (HsExpr GhcTc))
forall (m :: * -> *) a. Monad m => a -> m a
return (SrcSpan -> HsExpr GhcTc -> Located (HsExpr GhcTc)
forall l e. l -> e -> GenLocated l e
L SrcSpan
loc (HsExpr GhcTc -> Located (HsExpr GhcTc))
-> HsExpr GhcTc -> Located (HsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$ TcCoercionN -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrapCo TcCoercionN
co (HsExpr GhcTc -> HsExpr GhcTc) -> HsExpr GhcTc -> HsExpr GhcTc
forall a b. (a -> b) -> a -> b
$ Rebuilder
rebuild HsExpr GhcTc
fun [HsExprArg 'TcpTc]
tc_args) }
tcValArg :: HsExpr GhcRn
-> LHsExpr GhcRn
-> Scaled TcSigmaType
-> Int
-> TcM (LHsExpr GhcTc)
tcValArg :: HsExpr GhcRn
-> LHsExpr GhcRn
-> Scaled TcSigmaType
-> Int
-> TcM (LHsExpr GhcTc)
tcValArg HsExpr GhcRn
fun LHsExpr GhcRn
arg (Scaled TcSigmaType
mult TcSigmaType
arg_ty) Int
arg_no
= SDoc
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (HsExpr GhcRn -> Located (HsExpr GhcRn) -> Int -> SDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> SDoc
funAppCtxt HsExpr GhcRn
fun Located (HsExpr GhcRn)
LHsExpr GhcRn
arg Int
arg_no) (TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc)))
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
TcSigmaType
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a. TcSigmaType -> TcM a -> TcM a
tcScalingUsage TcSigmaType
mult (TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc)))
-> TcM (Located (HsExpr GhcTc)) -> TcM (Located (HsExpr GhcTc))
forall a b. (a -> b) -> a -> b
$
do { String -> SDoc -> TcM ()
traceTc String
"tcValArg" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
arg_no SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"of" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
fun
, String -> SDoc
text String
"arg type:" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
arg_ty
, String -> SDoc
text String
"arg:" SDoc -> SDoc -> SDoc
<+> Located (HsExpr GhcRn) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Located (HsExpr GhcRn)
LHsExpr GhcRn
arg ]
; LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTc)
tcCheckPolyExprNC LHsExpr GhcRn
arg TcSigmaType
arg_ty }
type Delta = TcTyVarSet
tcInstFun :: Bool
-> Bool
-> HsExpr GhcRn -> TcSigmaType -> [HsExprArg 'TcpRn]
-> TcM ( Delta
, [HsExprArg 'TcpInst]
, TcSigmaType )
tcInstFun :: Bool
-> Bool
-> HsExpr GhcRn
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
inst_final HsExpr GhcRn
rn_fun TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
= do { String -> SDoc -> TcM ()
traceTc String
"tcInstFun" (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun SDoc -> SDoc -> SDoc
$$ [HsExprArg 'TcpRn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpRn]
rn_args SDoc -> SDoc -> SDoc
$$ String -> SDoc
text String
"do_ql" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
do_ql)
; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
emptyVarSet [] [] TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args }
where
fun_orig :: CtOrigin
fun_orig = HsExpr GhcRn -> CtOrigin
exprCtOrigin HsExpr GhcRn
rn_fun
herald :: SDoc
herald = [SDoc] -> SDoc
sep [ String -> SDoc
text String
"The function" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun)
, String -> SDoc
text String
"is applied to"]
n_val_args :: Int
n_val_args = (HsExprArg 'TcpRn -> Bool) -> [HsExprArg 'TcpRn] -> Int
forall a. (a -> Bool) -> [a] -> Int
count HsExprArg 'TcpRn -> Bool
forall (id :: TcPass). HsExprArg id -> Bool
isHsValArg [HsExprArg 'TcpRn]
rn_args
fun_is_out_of_scope :: Bool
fun_is_out_of_scope
= case HsExpr GhcRn
rn_fun of
HsUnboundVar {} -> Bool
True
HsExpr GhcRn
_ -> Bool
False
inst_all :: ArgFlag -> Bool
inst_all :: ArgFlag -> Bool
inst_all (Invisible {}) = Bool
True
inst_all ArgFlag
Required = Bool
False
inst_inferred :: ArgFlag -> Bool
inst_inferred :: ArgFlag -> Bool
inst_inferred (Invisible Specificity
InferredSpec) = Bool
True
inst_inferred (Invisible Specificity
SpecifiedSpec) = Bool
False
inst_inferred ArgFlag
Required = Bool
False
inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
inst_fun [] | Bool
inst_final = ArgFlag -> Bool
inst_all
| Bool
otherwise = ArgFlag -> Bool
inst_inferred
inst_fun (EValArg {} : [HsExprArg 'TcpRn]
_) = ArgFlag -> Bool
inst_all
inst_fun [HsExprArg 'TcpRn]
_ = ArgFlag -> Bool
inst_inferred
go, go1 :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType -> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
| Just TyVar
kappa <- TcSigmaType -> Maybe TyVar
tcGetTyVar_maybe TcSigmaType
fun_ty
, TyVar
kappa TyVar -> Delta -> Bool
`elemVarSet` Delta
delta
= do { MetaDetails
cts <- TyVar -> TcM MetaDetails
readMetaTyVar TyVar
kappa
; case MetaDetails
cts of
Indirect TcSigmaType
fun_ty' -> Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty' [HsExprArg 'TcpRn]
args
MetaDetails
Flexi -> Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args }
| Bool
otherwise
= Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
go1 :: Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
| ([TyVar]
tvs, TcSigmaType
body1) <- (ArgFlag -> Bool) -> TcSigmaType -> ([TyVar], TcSigmaType)
tcSplitSomeForAllTyVars ([HsExprArg 'TcpRn] -> ArgFlag -> Bool
inst_fun [HsExprArg 'TcpRn]
args) TcSigmaType
fun_ty
, (ThetaType
theta, TcSigmaType
body2) <- TcSigmaType -> (ThetaType, TcSigmaType)
tcSplitPhiTy TcSigmaType
body1
, Bool -> Bool
not ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= do { ([TyVar]
inst_tvs, HsWrapper
wrap, TcSigmaType
fun_rho) <- [HsExprArg 'TcpRn]
-> TcM ([TyVar], HsWrapper, TcSigmaType)
-> TcM ([TyVar], HsWrapper, TcSigmaType)
forall a. [HsExprArg 'TcpRn] -> TcM a -> TcM a
setSrcSpanFromArgs [HsExprArg 'TcpRn]
rn_args (TcM ([TyVar], HsWrapper, TcSigmaType)
-> TcM ([TyVar], HsWrapper, TcSigmaType))
-> TcM ([TyVar], HsWrapper, TcSigmaType)
-> TcM ([TyVar], HsWrapper, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
CtOrigin
-> [TyVar]
-> ThetaType
-> TcSigmaType
-> TcM ([TyVar], HsWrapper, TcSigmaType)
instantiateSigma CtOrigin
fun_orig [TyVar]
tvs ThetaType
theta TcSigmaType
body2
; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go (Delta
delta Delta -> [TyVar] -> Delta
`extendVarSetList` [TyVar]
inst_tvs)
(HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
fun_rho [HsExprArg 'TcpRn]
args }
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
_ TcSigmaType
fun_ty []
= do { String -> SDoc -> TcM ()
traceTc String
"tcInstFun:ret" (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_ty)
; (Delta, [HsExprArg 'TcpInst], TcSigmaType)
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. [a] -> [a]
reverse [HsExprArg 'TcpInst]
acc, TcSigmaType
fun_ty) }
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty (EPar SrcSpan
sp : [HsExprArg 'TcpRn]
args)
= Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta (SrcSpan -> HsExprArg 'TcpInst
forall (p :: TcPass). SrcSpan -> HsExprArg p
EPar SrcSpan
sp HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty (EPrag SrcSpan
sp HsPragE (GhcPass (XPass 'TcpRn))
prag : [HsExprArg 'TcpRn]
args)
= Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go1 Delta
delta (SrcSpan -> HsPragE (GhcPass (XPass 'TcpInst)) -> HsExprArg 'TcpInst
forall (p :: TcPass).
SrcSpan -> HsPragE (GhcPass (XPass p)) -> HsExprArg p
EPrag SrcSpan
sp HsPragE (GhcPass (XPass 'TcpRn))
HsPragE (GhcPass (XPass 'TcpInst))
prag HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty ( ETypeArg { eva_loc :: forall (p :: TcPass). HsExprArg p -> SrcSpan
eva_loc = SrcSpan
loc, eva_hs_ty :: forall (p :: TcPass). HsExprArg p -> LHsWcType GhcRn
eva_hs_ty = LHsWcType GhcRn
hs_ty }
: [HsExprArg 'TcpRn]
rest_args )
| Bool
fun_is_out_of_scope
= Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty [HsExprArg 'TcpRn]
rest_args
| Bool
otherwise
= do { (TcSigmaType
ty_arg, TcSigmaType
inst_ty) <- TcSigmaType -> LHsWcType GhcRn -> TcM (TcSigmaType, TcSigmaType)
tcVTA TcSigmaType
fun_ty LHsWcType GhcRn
hs_ty
; let arg' :: HsExprArg 'TcpInst
arg' = ETypeArg :: forall (p :: TcPass).
SrcSpan -> LHsWcType GhcRn -> XETAType p -> HsExprArg p
ETypeArg { eva_loc :: SrcSpan
eva_loc = SrcSpan
loc, eva_hs_ty :: LHsWcType GhcRn
eva_hs_ty = LHsWcType GhcRn
hs_ty, eva_ty :: XETAType 'TcpInst
eva_ty = TcSigmaType
XETAType 'TcpInst
ty_arg }
; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta (HsExprArg 'TcpInst
arg' HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: [HsExprArg 'TcpInst]
acc) [Scaled TcSigmaType]
so_far TcSigmaType
inst_ty [HsExprArg 'TcpRn]
rest_args }
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty args :: [HsExprArg 'TcpRn]
args@(EValArg {} : [HsExprArg 'TcpRn]
_)
| Just TyVar
kappa <- TcSigmaType -> Maybe TyVar
tcGetTyVar_maybe TcSigmaType
fun_ty
, TyVar
kappa TyVar -> Delta -> Bool
`elemVarSet` Delta
delta
=
do { let valArgsCount :: Int
valArgsCount = [HsExprArg 'TcpRn] -> Int
forall (id :: TcPass). [HsExprArg id] -> Int
countLeadingValArgs [HsExprArg 'TcpRn]
args
; [TyVar]
arg_nus <- Int
-> IOEnv (Env TcGblEnv TcLclEnv) TyVar
-> IOEnv (Env TcGblEnv TcLclEnv) [TyVar]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
valArgsCount IOEnv (Env TcGblEnv TcLclEnv) TyVar
newOpenFlexiTyVar
; ThetaType
mults <- Int -> TcM TcSigmaType -> IOEnv (Env TcGblEnv TcLclEnv) ThetaType
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
valArgsCount (TcSigmaType -> TcM TcSigmaType
newFlexiTyVarTy TcSigmaType
multiplicityTy)
; TyVar
res_nu <- IOEnv (Env TcGblEnv TcLclEnv) TyVar
newOpenFlexiTyVar
; TcCoercionN
kind_co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyKind Maybe SDoc
forall a. Maybe a
Nothing TcSigmaType
liftedTypeKind (TyVar -> TcSigmaType
tyVarKind TyVar
kappa)
; let delta' :: Delta
delta' = Delta
delta Delta -> [TyVar] -> Delta
`extendVarSetList` (TyVar
res_nuTyVar -> [TyVar] -> [TyVar]
forall a. a -> [a] -> [a]
:[TyVar]
arg_nus)
arg_tys :: ThetaType
arg_tys = [TyVar] -> ThetaType
mkTyVarTys [TyVar]
arg_nus
res_ty :: TcSigmaType
res_ty = TyVar -> TcSigmaType
mkTyVarTy TyVar
res_nu
fun_ty' :: TcSigmaType
fun_ty' = [Scaled TcSigmaType] -> TcSigmaType -> TcSigmaType
mkVisFunTys (String
-> (TcSigmaType -> TcSigmaType -> Scaled TcSigmaType)
-> ThetaType
-> ThetaType
-> [Scaled TcSigmaType]
forall a b c. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"tcInstFun" TcSigmaType -> TcSigmaType -> Scaled TcSigmaType
forall a. TcSigmaType -> a -> Scaled a
mkScaled ThetaType
mults ThetaType
arg_tys) TcSigmaType
res_ty
co_wrap :: HsWrapper
co_wrap = TcCoercionN -> HsWrapper
mkWpCastN (Role -> TcSigmaType -> TcCoercionN -> TcCoercionN
mkTcGReflLeftCo Role
Nominal TcSigmaType
fun_ty' TcCoercionN
kind_co)
acc' :: [HsExprArg 'TcpInst]
acc' = HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
addArgWrap HsWrapper
co_wrap [HsExprArg 'TcpInst]
acc
; TyVar -> TcSigmaType -> TcM ()
writeMetaTyVar TyVar
kappa (TcSigmaType -> TcCoercionN -> TcSigmaType
mkCastTy TcSigmaType
fun_ty' TcCoercionN
kind_co)
; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta' [HsExprArg 'TcpInst]
acc' [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty' [HsExprArg 'TcpRn]
args }
go1 Delta
delta [HsExprArg 'TcpInst]
acc [Scaled TcSigmaType]
so_far TcSigmaType
fun_ty
(eva :: HsExprArg 'TcpRn
eva@(EValArg { eva_arg :: forall (p :: TcPass). HsExprArg p -> EValArg p
eva_arg = ValArg LHsExpr (GhcPass (XPass 'TcpRn))
arg }) : [HsExprArg 'TcpRn]
rest_args)
= do { (HsWrapper
wrap, Scaled TcSigmaType
arg_ty, TcSigmaType
res_ty) <- SDoc
-> Maybe SDoc
-> (Int, [Scaled TcSigmaType])
-> TcSigmaType
-> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType)
matchActualFunTySigma SDoc
herald
(SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun))
(Int
n_val_args, [Scaled TcSigmaType]
so_far) TcSigmaType
fun_ty
; let arg_no :: Int
arg_no = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (HsExprArg 'TcpInst -> Bool) -> [HsExprArg 'TcpInst] -> Int
forall a. (a -> Bool) -> [a] -> Int
count HsExprArg 'TcpInst -> Bool
forall (id :: TcPass). HsExprArg id -> Bool
isVisibleArg [HsExprArg 'TcpInst]
acc
; (Delta
delta', EValArg 'TcpInst
arg') <- if Bool
do_ql
then SDoc
-> TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a. SDoc -> TcM a -> TcM a
addErrCtxt (HsExpr GhcRn -> Located (HsExpr GhcRn) -> Int -> SDoc
forall fun arg.
(Outputable fun, Outputable arg) =>
fun -> arg -> Int -> SDoc
funAppCtxt HsExpr GhcRn
rn_fun Located (HsExpr GhcRn)
LHsExpr (GhcPass (XPass 'TcpRn))
arg Int
arg_no) (TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst))
-> TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a b. (a -> b) -> a -> b
$
Delta
-> LHsExpr GhcRn
-> Scaled TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg Delta
delta LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpRn))
arg Scaled TcSigmaType
arg_ty
else (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, LHsExpr (GhcPass (XPass 'TcpInst)) -> EValArg 'TcpInst
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg LHsExpr (GhcPass (XPass 'TcpRn))
LHsExpr (GhcPass (XPass 'TcpInst))
arg)
; let acc' :: [HsExprArg 'TcpInst]
acc' = HsExprArg 'TcpRn
eva { eva_arg :: EValArg 'TcpInst
eva_arg = EValArg 'TcpInst
arg', eva_arg_ty :: XEVAType 'TcpInst
eva_arg_ty = Scaled TcSigmaType
XEVAType 'TcpInst
arg_ty }
HsExprArg 'TcpInst -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
forall a. a -> [a] -> [a]
: HsWrapper -> [HsExprArg 'TcpInst] -> [HsExprArg 'TcpInst]
addArgWrap HsWrapper
wrap [HsExprArg 'TcpInst]
acc
; Delta
-> [HsExprArg 'TcpInst]
-> [Scaled TcSigmaType]
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
go Delta
delta' [HsExprArg 'TcpInst]
acc' (Scaled TcSigmaType
arg_tyScaled TcSigmaType -> [Scaled TcSigmaType] -> [Scaled TcSigmaType]
forall a. a -> [a] -> [a]
:[Scaled TcSigmaType]
so_far) TcSigmaType
res_ty [HsExprArg 'TcpRn]
rest_args }
tcVTA :: TcType
-> LHsWcType GhcRn
-> TcM (TcType, TcType)
tcVTA :: TcSigmaType -> LHsWcType GhcRn -> TcM (TcSigmaType, TcSigmaType)
tcVTA TcSigmaType
fun_ty LHsWcType GhcRn
hs_ty
| Just (TyVarBinder
tvb, TcSigmaType
inner_ty) <- TcSigmaType -> Maybe (TyVarBinder, TcSigmaType)
tcSplitForAllTyVarBinder_maybe TcSigmaType
fun_ty
, TyVarBinder -> ArgFlag
forall tv argf. VarBndr tv argf -> argf
binderArgFlag TyVarBinder
tvb ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Specified
= do { let tv :: TyVar
tv = TyVarBinder -> TyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
tvb
kind :: TcSigmaType
kind = TyVar -> TcSigmaType
tyVarKind TyVar
tv
; TcSigmaType
ty_arg <- LHsWcType GhcRn -> TcSigmaType -> TcM TcSigmaType
tcHsTypeApp LHsWcType GhcRn
hs_ty TcSigmaType
kind
; TcSigmaType
inner_ty <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
inner_ty
; let in_scope :: InScopeSet
in_scope = Delta -> InScopeSet
mkInScopeSet (ThetaType -> Delta
tyCoVarsOfTypes [TcSigmaType
fun_ty, TcSigmaType
ty_arg])
insted_ty :: TcSigmaType
insted_ty = InScopeSet -> [TyVar] -> ThetaType -> TcSigmaType -> TcSigmaType
substTyWithInScope InScopeSet
in_scope [TyVar
tv] [TcSigmaType
ty_arg] TcSigmaType
inner_ty
; String -> SDoc -> TcM ()
traceTc String
"VTA" ([SDoc] -> SDoc
vcat [TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
tv, TcSigmaType -> SDoc
debugPprType TcSigmaType
kind
, TcSigmaType -> SDoc
debugPprType TcSigmaType
ty_arg
, TcSigmaType -> SDoc
debugPprType (HasDebugCallStack => TcSigmaType -> TcSigmaType
TcSigmaType -> TcSigmaType
tcTypeKind TcSigmaType
ty_arg)
, TcSigmaType -> SDoc
debugPprType TcSigmaType
inner_ty
, TcSigmaType -> SDoc
debugPprType TcSigmaType
insted_ty ])
; (TcSigmaType, TcSigmaType) -> TcM (TcSigmaType, TcSigmaType)
forall (m :: * -> *) a. Monad m => a -> m a
return (TcSigmaType
ty_arg, TcSigmaType
insted_ty) }
| Bool
otherwise
= do { (TidyEnv
_, TcSigmaType
fun_ty) <- TidyEnv -> TcSigmaType -> TcM (TidyEnv, TcSigmaType)
zonkTidyTcType TidyEnv
emptyTidyEnv TcSigmaType
fun_ty
; SDoc -> TcM (TcSigmaType, TcSigmaType)
forall a. SDoc -> TcRn a
failWith (SDoc -> TcM (TcSigmaType, TcSigmaType))
-> SDoc -> TcM (TcSigmaType, TcSigmaType)
forall a b. (a -> b) -> a -> b
$
String -> SDoc
text String
"Cannot apply expression of type" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
fun_ty) SDoc -> SDoc -> SDoc
$$
String -> SDoc
text String
"to a visible type argument" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (HsWildCardBndrs GhcRn (Located (HsType GhcRn)) -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsWildCardBndrs GhcRn (Located (HsType GhcRn))
LHsWcType GhcRn
hs_ty) }
quickLookArg :: Delta
-> LHsExpr GhcRn
-> Scaled TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg :: Delta
-> LHsExpr GhcRn
-> Scaled TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg Delta
delta LHsExpr GhcRn
larg (Scaled TcSigmaType
_ TcSigmaType
arg_ty)
| Delta -> Bool
isEmptyVarSet Delta
delta = Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr GhcRn
larg
| Bool
otherwise = TcSigmaType -> TcM (Delta, EValArg 'TcpInst)
go TcSigmaType
arg_ty
where
guarded :: Bool
guarded = TcSigmaType -> Bool
isGuardedTy TcSigmaType
arg_ty
go :: TcSigmaType -> TcM (Delta, EValArg 'TcpInst)
go TcSigmaType
arg_ty | Bool -> Bool
not (TcSigmaType -> Bool
isRhoTy TcSigmaType
arg_ty)
= Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr GhcRn
larg
| Just TyVar
kappa <- TcSigmaType -> Maybe TyVar
tcGetTyVar_maybe TcSigmaType
arg_ty
, TyVar
kappa TyVar -> Delta -> Bool
`elemVarSet` Delta
delta
= do { MetaDetails
info <- TyVar -> TcM MetaDetails
readMetaTyVar TyVar
kappa
; case MetaDetails
info of
Indirect TcSigmaType
arg_ty' -> TcSigmaType -> TcM (Delta, EValArg 'TcpInst)
go TcSigmaType
arg_ty'
MetaDetails
Flexi -> Bool
-> Delta
-> LHsExpr GhcRn
-> TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta LHsExpr GhcRn
larg TcSigmaType
arg_ty }
| Bool
otherwise
= Bool
-> Delta
-> LHsExpr GhcRn
-> TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta LHsExpr GhcRn
larg TcSigmaType
arg_ty
isGuardedTy :: TcType -> Bool
isGuardedTy :: TcSigmaType -> Bool
isGuardedTy TcSigmaType
ty
| Just (TyCon
tc,ThetaType
_) <- HasCallStack => TcSigmaType -> Maybe (TyCon, ThetaType)
TcSigmaType -> Maybe (TyCon, ThetaType)
tcSplitTyConApp_maybe TcSigmaType
ty = TyCon -> Role -> Bool
isGenerativeTyCon TyCon
tc Role
Nominal
| Just {} <- TcSigmaType -> Maybe (TcSigmaType, TcSigmaType)
tcSplitAppTy_maybe TcSigmaType
ty = Bool
True
| Bool
otherwise = Bool
False
quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 :: Bool
-> Delta
-> LHsExpr GhcRn
-> TcSigmaType
-> TcM (Delta, EValArg 'TcpInst)
quickLookArg1 Bool
guarded Delta
delta larg :: LHsExpr GhcRn
larg@(L loc arg) TcSigmaType
arg_ty
= SrcSpan
-> TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a. SrcSpan -> TcRn a -> TcRn a
setSrcSpan SrcSpan
loc (TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst))
-> TcM (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall a b. (a -> b) -> a -> b
$
do { let (HsExpr GhcRn
rn_fun,[HsExprArg 'TcpRn]
rn_args,Rebuilder
rebuild) = HsExpr GhcRn -> (HsExpr GhcRn, [HsExprArg 'TcpRn], Rebuilder)
splitHsApps HsExpr GhcRn
arg
; Maybe (HsExpr GhcTc, TcSigmaType)
mb_fun_ty <- HsExpr GhcRn
-> [HsExprArg 'TcpRn]
-> Maybe TcSigmaType
-> TcM (Maybe (HsExpr GhcTc, TcSigmaType))
tcInferAppHead_maybe HsExpr GhcRn
rn_fun [HsExprArg 'TcpRn]
rn_args (TcSigmaType -> Maybe TcSigmaType
forall a. a -> Maybe a
Just TcSigmaType
arg_ty)
; String -> SDoc -> TcM ()
traceTc String
"quickLookArg 1" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"arg:" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
arg
, String -> SDoc
text String
"head:" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
rn_fun SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Maybe (HsExpr GhcTc, TcSigmaType) -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe (HsExpr GhcTc, TcSigmaType)
mb_fun_ty
, String -> SDoc
text String
"args:" SDoc -> SDoc -> SDoc
<+> [HsExprArg 'TcpRn] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [HsExprArg 'TcpRn]
rn_args ]
; case Maybe (HsExpr GhcTc, TcSigmaType)
mb_fun_ty of {
Maybe (HsExpr GhcTc, TcSigmaType)
Nothing ->
Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr GhcRn
larg ;
Just (HsExpr GhcTc
fun', TcSigmaType
fun_sigma) ->
do { let no_free_kappas :: Bool
no_free_kappas = TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
findNoQuantVars TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
; String -> SDoc -> TcM ()
traceTc String
"quickLookArg 2" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"no_free_kappas:" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
no_free_kappas
, String -> SDoc
text String
"guarded:" SDoc -> SDoc -> SDoc
<+> Bool -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bool
guarded ]
; if Bool -> Bool
not (Bool
guarded Bool -> Bool -> Bool
|| Bool
no_free_kappas)
then Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr GhcRn
larg
else
do { Bool
do_ql <- HsExpr GhcRn -> TcM Bool
wantQuickLook HsExpr GhcRn
rn_fun
; (Delta
delta_app, [HsExprArg 'TcpInst]
inst_args, TcSigmaType
app_res_rho)
<- Bool
-> Bool
-> HsExpr GhcRn
-> TcSigmaType
-> [HsExprArg 'TcpRn]
-> TcM (Delta, [HsExprArg 'TcpInst], TcSigmaType)
tcInstFun Bool
do_ql Bool
True HsExpr GhcRn
rn_fun TcSigmaType
fun_sigma [HsExprArg 'TcpRn]
rn_args
; String -> SDoc -> TcM ()
traceTc String
"quickLookArg" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ String -> SDoc
text String
"arg:" SDoc -> SDoc -> SDoc
<+> HsExpr GhcRn -> SDoc
forall a. Outputable a => a -> SDoc
ppr HsExpr GhcRn
arg
, String -> SDoc
text String
"delta:" SDoc -> SDoc -> SDoc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
, String -> SDoc
text String
"delta_app:" SDoc -> SDoc -> SDoc
<+> Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta_app
, String -> SDoc
text String
"arg_ty:" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
arg_ty
, String -> SDoc
text String
"app_res_rho:" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
app_res_rho ]
; let delta' :: Delta
delta' = Delta
delta Delta -> Delta -> Delta
`unionVarSet` Delta
delta_app
; Delta -> TcSigmaType -> TcSigmaType -> TcM ()
qlUnify Delta
delta' TcSigmaType
arg_ty TcSigmaType
app_res_rho
; let ql_arg :: EValArg 'TcpInst
ql_arg = ValArgQL :: LHsExpr GhcRn
-> HsExpr GhcTc
-> [HsExprArg 'TcpInst]
-> TcSigmaType
-> Rebuilder
-> EValArg 'TcpInst
ValArgQL { va_expr :: LHsExpr GhcRn
va_expr = LHsExpr GhcRn
larg, va_fun :: HsExpr GhcTc
va_fun = HsExpr GhcTc
fun'
, va_args :: [HsExprArg 'TcpInst]
va_args = [HsExprArg 'TcpInst]
inst_args
, va_ty :: TcSigmaType
va_ty = TcSigmaType
app_res_rho
, va_rebuild :: Rebuilder
va_rebuild = Rebuilder
rebuild }
; (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta', EValArg 'TcpInst
ql_arg) } } } }
skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook Delta
delta LHsExpr GhcRn
larg = (Delta, EValArg 'TcpInst) -> TcM (Delta, EValArg 'TcpInst)
forall (m :: * -> *) a. Monad m => a -> m a
return (Delta
delta, LHsExpr (GhcPass (XPass 'TcpInst)) -> EValArg 'TcpInst
forall (p :: TcPass). LHsExpr (GhcPass (XPass p)) -> EValArg p
ValArg LHsExpr GhcRn
LHsExpr (GhcPass (XPass 'TcpInst))
larg)
quickLookResultType :: Bool -> Delta -> TcRhoType -> ExpRhoType -> TcM ()
quickLookResultType :: Bool -> Delta -> TcSigmaType -> ExpRhoType -> TcM ()
quickLookResultType Bool
do_ql Delta
delta TcSigmaType
app_res_rho ExpRhoType
exp_res_ty
| Bool
do_ql
, Bool -> Bool
not (Delta -> Bool
isEmptyVarSet Delta
delta)
, Just TcSigmaType
exp_rho <- ExpRhoType -> Maybe TcSigmaType
checkingExpType_maybe ExpRhoType
exp_res_ty
= Delta -> TcSigmaType -> TcSigmaType -> TcM ()
qlUnify Delta
delta TcSigmaType
app_res_rho TcSigmaType
exp_rho
| Bool
otherwise
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
qlUnify :: Delta -> TcType -> TcType -> TcM ()
qlUnify :: Delta -> TcSigmaType -> TcSigmaType -> TcM ()
qlUnify Delta
delta TcSigmaType
ty1 TcSigmaType
ty2
= do { String -> SDoc -> TcM ()
traceTc String
"qlUnify" (Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta SDoc -> SDoc -> SDoc
$$ TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty1 SDoc -> SDoc -> SDoc
$$ TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2)
; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta
emptyVarSet,Delta
emptyVarSet) TcSigmaType
ty1 TcSigmaType
ty2 }
where
go :: (TyVarSet, TcTyVarSet)
-> TcType -> TcType
-> TcM ()
go :: (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs (TyVarTy TyVar
tv) TcSigmaType
ty2
| TyVar
tv TyVar -> Delta -> Bool
`elemVarSet` Delta
delta = (Delta, Delta) -> TyVar -> TcSigmaType -> TcM ()
go_kappa (Delta, Delta)
bvs TyVar
tv TcSigmaType
ty2
go (Delta
bvs1, Delta
bvs2) TcSigmaType
ty1 (TyVarTy TyVar
tv)
| TyVar
tv TyVar -> Delta -> Bool
`elemVarSet` Delta
delta = (Delta, Delta) -> TyVar -> TcSigmaType -> TcM ()
go_kappa (Delta
bvs2,Delta
bvs1) TyVar
tv TcSigmaType
ty1
go (Delta, Delta)
bvs (CastTy TcSigmaType
ty1 TcCoercionN
_) TcSigmaType
ty2 = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
ty1 TcSigmaType
ty2
go (Delta, Delta)
bvs TcSigmaType
ty1 (CastTy TcSigmaType
ty2 TcCoercionN
_) = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
ty1 TcSigmaType
ty2
go (Delta, Delta)
_ (TyConApp TyCon
tc1 []) (TyConApp TyCon
tc2 [])
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go (Delta, Delta)
bvs TcSigmaType
rho1 TcSigmaType
rho2
| Just TcSigmaType
rho1 <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
rho1 = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
rho1 TcSigmaType
rho2
| Just TcSigmaType
rho2 <- TcSigmaType -> Maybe TcSigmaType
tcView TcSigmaType
rho2 = (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
rho1 TcSigmaType
rho2
go (Delta, Delta)
bvs (TyConApp TyCon
tc1 ThetaType
tys1) (TyConApp TyCon
tc2 ThetaType
tys2)
| TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
, Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc1)
, ThetaType
tys1 ThetaType -> ThetaType -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` ThetaType
tys2
= (TcSigmaType -> TcSigmaType -> TcM ())
-> ThetaType -> ThetaType -> TcM ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ ((Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs) ThetaType
tys1 ThetaType
tys2
go (Delta, Delta)
bvs (FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af1, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg1, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res1, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
mult1 })
(FunTy { ft_af :: TcSigmaType -> AnonArgFlag
ft_af = AnonArgFlag
af2, ft_arg :: TcSigmaType -> TcSigmaType
ft_arg = TcSigmaType
arg2, ft_res :: TcSigmaType -> TcSigmaType
ft_res = TcSigmaType
res2, ft_mult :: TcSigmaType -> TcSigmaType
ft_mult = TcSigmaType
mult2 })
| AnonArgFlag
af1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
af2
= do { Bool -> TcM () -> TcM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (AnonArgFlag
af1 AnonArgFlag -> AnonArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== AnonArgFlag
VisArg) (TcM () -> TcM ()) -> TcM () -> TcM ()
forall a b. (a -> b) -> a -> b
$
do { (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
arg1 TcSigmaType
arg2; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
mult1 TcSigmaType
mult2 }
; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
res1 TcSigmaType
res2 }
go (Delta, Delta)
bvs (AppTy TcSigmaType
t1a TcSigmaType
t1b) TcSigmaType
ty2
| Just (TcSigmaType
t2a, TcSigmaType
t2b) <- TcSigmaType -> Maybe (TcSigmaType, TcSigmaType)
tcRepSplitAppTy_maybe TcSigmaType
ty2
= do { (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
t1a TcSigmaType
t2a; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
t1b TcSigmaType
t2b }
go (Delta, Delta)
bvs TcSigmaType
ty1 (AppTy TcSigmaType
t2a TcSigmaType
t2b)
| Just (TcSigmaType
t1a, TcSigmaType
t1b) <- TcSigmaType -> Maybe (TcSigmaType, TcSigmaType)
tcRepSplitAppTy_maybe TcSigmaType
ty1
= do { (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
t1a TcSigmaType
t2a; (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
t1b TcSigmaType
t2b }
go (Delta
bvs1, Delta
bvs2) (ForAllTy TyVarBinder
bv1 TcSigmaType
ty1) (ForAllTy TyVarBinder
bv2 TcSigmaType
ty2)
= (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta
bvs1',Delta
bvs2') TcSigmaType
ty1 TcSigmaType
ty2
where
bvs1' :: Delta
bvs1' = Delta
bvs1 Delta -> TyVar -> Delta
`extendVarSet` TyVarBinder -> TyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
bv1
bvs2' :: Delta
bvs2' = Delta
bvs2 Delta -> TyVar -> Delta
`extendVarSet` TyVarBinder -> TyVar
forall tv argf. VarBndr tv argf -> tv
binderVar TyVarBinder
bv2
go (Delta, Delta)
_ TcSigmaType
_ TcSigmaType
_ = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
go_kappa :: (Delta, Delta) -> TyVar -> TcSigmaType -> TcM ()
go_kappa (Delta, Delta)
bvs TyVar
kappa TcSigmaType
ty2
= ASSERT2( isMetaTyVar kappa, ppr kappa )
do { MetaDetails
info <- TyVar -> TcM MetaDetails
readMetaTyVar TyVar
kappa
; case MetaDetails
info of
Indirect TcSigmaType
ty1 -> (Delta, Delta) -> TcSigmaType -> TcSigmaType -> TcM ()
go (Delta, Delta)
bvs TcSigmaType
ty1 TcSigmaType
ty2
MetaDetails
Flexi -> do { TcSigmaType
ty2 <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
ty2
; (Delta, Delta) -> TyVar -> TcSigmaType -> TcM ()
forall a. (a, Delta) -> TyVar -> TcSigmaType -> TcM ()
go_flexi (Delta, Delta)
bvs TyVar
kappa TcSigmaType
ty2 } }
go_flexi :: (a, Delta) -> TyVar -> TcSigmaType -> TcM ()
go_flexi (a
_,Delta
bvs2) TyVar
kappa TcSigmaType
ty2
|
let ty2_tvs :: Delta
ty2_tvs = TcSigmaType -> Delta
shallowTyCoVarsOfType TcSigmaType
ty2
, Bool -> Bool
not (Delta
ty2_tvs Delta -> Delta -> Bool
`intersectsVarSet` Delta
bvs2)
, Just TcSigmaType
ty2 <- [TyVar] -> TcSigmaType -> Maybe TcSigmaType
occCheckExpand [TyVar
kappa] TcSigmaType
ty2
= do { let ty2_kind :: TcSigmaType
ty2_kind = HasDebugCallStack => TcSigmaType -> TcSigmaType
TcSigmaType -> TcSigmaType
typeKind TcSigmaType
ty2
kappa_kind :: TcSigmaType
kappa_kind = TyVar -> TcSigmaType
tyVarKind TyVar
kappa
; TcCoercionN
co <- Maybe SDoc -> TcSigmaType -> TcSigmaType -> TcM TcCoercionN
unifyKind (SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2)) TcSigmaType
ty2_kind TcSigmaType
kappa_kind
; String -> SDoc -> TcM ()
traceTc String
"qlUnify:update" (SDoc -> TcM ()) -> SDoc -> TcM ()
forall a b. (a -> b) -> a -> b
$
[SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
kappa SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
kappa_kind)
Int
2 (String -> SDoc
text String
":=" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty2_kind)
, String -> SDoc
text String
"co:" SDoc -> SDoc -> SDoc
<+> TcCoercionN -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcCoercionN
co ]
; TyVar -> TcSigmaType -> TcM ()
writeMetaTyVar TyVar
kappa (TcSigmaType -> TcCoercionN -> TcSigmaType
mkCastTy TcSigmaType
ty2 TcCoercionN
co) }
| Bool
otherwise
= () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
findNoQuantVars :: TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
findNoQuantVars TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
= Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go Delta
emptyVarSet TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
where
need_instantiation :: [HsExprArg p] -> Bool
need_instantiation [] = Bool
True
need_instantiation (EValArg {} : [HsExprArg p]
_) = Bool
True
need_instantiation [HsExprArg p]
_ = Bool
False
go :: TyVarSet -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go :: Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
| [HsExprArg 'TcpRn] -> Bool
forall (p :: TcPass). [HsExprArg p] -> Bool
need_instantiation [HsExprArg 'TcpRn]
args
, ([TyVar]
tvs, ThetaType
theta, TcSigmaType
rho) <- TcSigmaType -> ([TyVar], ThetaType, TcSigmaType)
tcSplitSigmaTy TcSigmaType
fun_ty
, Bool -> Bool
not ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go (Delta
bvs Delta -> [TyVar] -> Delta
`extendVarSetList` [TyVar]
tvs) TcSigmaType
rho [HsExprArg 'TcpRn]
args
go Delta
bvs TcSigmaType
fun_ty [] = TcSigmaType -> Delta
tyCoVarsOfType TcSigmaType
fun_ty Delta -> Delta -> Bool
`disjointVarSet` Delta
bvs
go Delta
bvs TcSigmaType
fun_ty (EPar {} : [HsExprArg 'TcpRn]
args) = Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
go Delta
bvs TcSigmaType
fun_ty (EPrag {} : [HsExprArg 'TcpRn]
args) = Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcSigmaType
fun_ty [HsExprArg 'TcpRn]
args
go Delta
bvs TcSigmaType
fun_ty args :: [HsExprArg 'TcpRn]
args@(ETypeArg {} : [HsExprArg 'TcpRn]
rest_args)
| ([TyVar]
tvs, TcSigmaType
body1) <- (ArgFlag -> Bool) -> TcSigmaType -> ([TyVar], TcSigmaType)
tcSplitSomeForAllTyVars (ArgFlag -> ArgFlag -> Bool
forall a. Eq a => a -> a -> Bool
== ArgFlag
Inferred) TcSigmaType
fun_ty
, (ThetaType
theta, TcSigmaType
body2) <- TcSigmaType -> (ThetaType, TcSigmaType)
tcSplitPhiTy TcSigmaType
body1
, Bool -> Bool
not ([TyVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TyVar]
tvs Bool -> Bool -> Bool
&& ThetaType -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ThetaType
theta)
= Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go (Delta
bvs Delta -> [TyVar] -> Delta
`extendVarSetList` [TyVar]
tvs) TcSigmaType
body2 [HsExprArg 'TcpRn]
args
| Just (TyVarBinder
_tv, TcSigmaType
res_ty) <- TcSigmaType -> Maybe (TyVarBinder, TcSigmaType)
tcSplitForAllTyVarBinder_maybe TcSigmaType
fun_ty
= Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcSigmaType
res_ty [HsExprArg 'TcpRn]
rest_args
| Bool
otherwise
= Bool
False
go Delta
bvs TcSigmaType
fun_ty (EValArg {} : [HsExprArg 'TcpRn]
rest_args)
| Just (Scaled TcSigmaType
_, TcSigmaType
res_ty) <- TcSigmaType -> Maybe (Scaled TcSigmaType, TcSigmaType)
tcSplitFunTy_maybe TcSigmaType
fun_ty
= Delta -> TcSigmaType -> [HsExprArg 'TcpRn] -> Bool
go Delta
bvs TcSigmaType
res_ty [HsExprArg 'TcpRn]
rest_args
| Bool
otherwise
= Bool
False
isTagToEnum :: HsExpr GhcRn -> Bool
isTagToEnum :: HsExpr GhcRn -> Bool
isTagToEnum (HsVar XVar GhcRn
_ (L _ fun_id)) = Name
fun_id Name -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
tagToEnumKey
isTagToEnum HsExpr GhcRn
_ = Bool
False
tcTagToEnum :: HsExpr GhcRn -> HsExpr GhcTc -> [HsExprArg 'TcpTc]
-> TcRhoType -> ExpRhoType
-> TcM (HsExpr GhcTc)
tcTagToEnum :: HsExpr GhcRn
-> HsExpr GhcTc
-> [HsExprArg 'TcpTc]
-> TcSigmaType
-> ExpRhoType
-> TcM (HsExpr GhcTc)
tcTagToEnum HsExpr GhcRn
expr HsExpr GhcTc
fun [HsExprArg 'TcpTc]
args TcSigmaType
app_res_ty ExpRhoType
res_ty
| [HsExprArg 'TcpTc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [HsExprArg 'TcpTc]
val_args
= SDoc -> TcM (HsExpr GhcTc)
forall a. SDoc -> TcRn a
failWithTc (String -> SDoc
text String
"tagToEnum# must appear applied to one argument")
| Bool
otherwise
= do { TcSigmaType
res_ty <- ExpRhoType -> TcM TcSigmaType
readExpType ExpRhoType
res_ty
; TcSigmaType
ty' <- TcSigmaType -> TcM TcSigmaType
zonkTcType TcSigmaType
res_ty
; case HasCallStack => TcSigmaType -> Maybe (TyCon, ThetaType)
TcSigmaType -> Maybe (TyCon, ThetaType)
tcSplitTyConApp_maybe TcSigmaType
ty' of {
Maybe (TyCon, ThetaType)
Nothing -> do { SDoc -> TcM ()
addErrTc (TcSigmaType -> SDoc -> SDoc
mk_error TcSigmaType
ty' SDoc
doc1)
; TcM (HsExpr GhcTc)
vanilla_result } ;
Just (TyCon
tc, ThetaType
tc_args) ->
do {
; FamInstEnvs
fam_envs <- TcM FamInstEnvs
tcGetFamInstEnvs
; case FamInstEnvs
-> TyCon -> ThetaType -> Maybe (TyCon, ThetaType, TcCoercionN)
tcLookupDataFamInst_maybe FamInstEnvs
fam_envs TyCon
tc ThetaType
tc_args of {
Maybe (TyCon, ThetaType, TcCoercionN)
Nothing -> do { TcSigmaType -> TyCon -> TcM ()
check_enumeration TcSigmaType
ty' TyCon
tc
; TcM (HsExpr GhcTc)
vanilla_result } ;
Just (TyCon
rep_tc, ThetaType
rep_args, TcCoercionN
coi) ->
do {
TcSigmaType -> TyCon -> TcM ()
check_enumeration TcSigmaType
ty' TyCon
rep_tc
; let rep_ty :: TcSigmaType
rep_ty = TyCon -> ThetaType -> TcSigmaType
mkTyConApp TyCon
rep_tc ThetaType
rep_args
fun' :: HsExpr GhcTc
fun' = HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap (TcSigmaType -> HsWrapper
WpTyApp TcSigmaType
rep_ty) HsExpr GhcTc
fun
expr' :: HsExpr GhcTc
expr' = Rebuilder
rebuildPrefixApps HsExpr GhcTc
fun' [HsExprArg 'TcpTc]
val_args
df_wrap :: HsWrapper
df_wrap = TcCoercionN -> HsWrapper
mkWpCastR (TcCoercionN -> TcCoercionN
mkTcSymCo TcCoercionN
coi)
; HsExpr GhcTc -> TcM (HsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
mkHsWrap HsWrapper
df_wrap HsExpr GhcTc
expr') }}}}}
where
val_args :: [HsExprArg 'TcpTc]
val_args = (HsExprArg 'TcpTc -> Bool)
-> [HsExprArg 'TcpTc] -> [HsExprArg 'TcpTc]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not (Bool -> Bool)
-> (HsExprArg 'TcpTc -> Bool) -> HsExprArg 'TcpTc -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsExprArg 'TcpTc -> Bool
forall (id :: TcPass). HsExprArg id -> Bool
isHsValArg) [HsExprArg 'TcpTc]
args
vanilla_result :: TcM (HsExpr GhcTc)
vanilla_result
= do { let expr' :: HsExpr GhcTc
expr' = Rebuilder
rebuildPrefixApps HsExpr GhcTc
fun [HsExprArg 'TcpTc]
args
; HsExpr GhcRn
-> HsExpr GhcTc -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTc)
tcWrapResultMono HsExpr GhcRn
expr HsExpr GhcTc
expr' TcSigmaType
app_res_ty ExpRhoType
res_ty }
check_enumeration :: TcSigmaType -> TyCon -> TcM ()
check_enumeration TcSigmaType
ty' TyCon
tc
| TyCon -> Bool
isEnumerationTyCon TyCon
tc = () -> TcM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
otherwise = SDoc -> TcM ()
addErrTc (TcSigmaType -> SDoc -> SDoc
mk_error TcSigmaType
ty' SDoc
doc2)
doc1 :: SDoc
doc1 = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Specify the type by giving a type signature"
, String -> SDoc
text String
"e.g. (tagToEnum# x) :: Bool" ]
doc2 :: SDoc
doc2 = String -> SDoc
text String
"Result type must be an enumeration type"
mk_error :: TcType -> SDoc -> SDoc
mk_error :: TcSigmaType -> SDoc -> SDoc
mk_error TcSigmaType
ty SDoc
what
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Bad call to tagToEnum#"
SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"at type" SDoc -> SDoc -> SDoc
<+> TcSigmaType -> SDoc
forall a. Outputable a => a -> SDoc
ppr TcSigmaType
ty)
Int
2 SDoc
what
tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag (HsPragSCC XSCC GhcRn
x1 SourceText
src StringLiteral
ann) = XSCC GhcTc -> SourceText -> StringLiteral -> HsPragE GhcTc
forall p. XSCC p -> SourceText -> StringLiteral -> HsPragE p
HsPragSCC XSCC GhcRn
XSCC GhcTc
x1 SourceText
src StringLiteral
ann