summaryrefslogtreecommitdiff
path: root/compiler/GHC/Tc/Gen
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/GHC/Tc/Gen')
-rw-r--r--compiler/GHC/Tc/Gen/Arrow.hs15
-rw-r--r--compiler/GHC/Tc/Gen/Bind.hs148
-rw-r--r--compiler/GHC/Tc/Gen/Default.hs4
-rw-r--r--compiler/GHC/Tc/Gen/Expr.hs288
-rw-r--r--compiler/GHC/Tc/Gen/Expr.hs-boot30
-rw-r--r--compiler/GHC/Tc/Gen/Foreign.hs2
-rw-r--r--compiler/GHC/Tc/Gen/HsType.hs831
-rw-r--r--compiler/GHC/Tc/Gen/Match.hs75
-rw-r--r--compiler/GHC/Tc/Gen/Pat.hs52
-rw-r--r--compiler/GHC/Tc/Gen/Rule.hs2
-rw-r--r--compiler/GHC/Tc/Gen/Sig.hs16
-rw-r--r--compiler/GHC/Tc/Gen/Splice.hs12
12 files changed, 862 insertions, 613 deletions
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index ef60b3cea7..c21a885970 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -14,7 +14,8 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where
import GHC.Prelude
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcLExpr, tcInferRho, tcSyntaxOp, tcCheckId, tcCheckExpr )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp
+ , tcCheckId, tcCheckPolyExpr )
import GHC.Hs
import GHC.Tc.Gen.Match
@@ -161,7 +162,7 @@ tc_cmd env in_cmd@(HsCmdLamCase x matches) (stk, res_ty)
return (mkHsCmdWrap (mkWpCastN co) (HsCmdLamCase x matches'))
tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if'
- = do { pred' <- tcLExpr pred (mkCheckExpType boolTy)
+ = do { pred' <- tcCheckMonoExpr pred boolTy
; b1' <- tcCmd env b1 res_ty
; b2' <- tcCmd env b2 res_ty
; return (HsCmdIf x NoSyntaxExprTc pred' b1' b2')
@@ -179,7 +180,7 @@ tc_cmd env (HsCmdIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty -- Rebindable syn
; (pred', fun')
<- tcSyntaxOp IfOrigin fun (map synKnownType [pred_ty, r_ty, r_ty])
(mkCheckExpType r_ty) $ \ _ ->
- tcLExpr pred (mkCheckExpType pred_ty)
+ tcCheckMonoExpr pred pred_ty
; b1' <- tcCmd env b1 res_ty
; b2' <- tcCmd env b2 res_ty
@@ -206,9 +207,9 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty)
= addErrCtxt (cmdCtxt cmd) $
do { arg_ty <- newOpenFlexiTyVarTy
; let fun_ty = mkCmdArrTy env arg_ty res_ty
- ; fun' <- select_arrow_scope (tcLExpr fun (mkCheckExpType fun_ty))
+ ; fun' <- select_arrow_scope (tcCheckMonoExpr fun fun_ty)
- ; arg' <- tcLExpr arg (mkCheckExpType arg_ty)
+ ; arg' <- tcCheckMonoExpr arg arg_ty
; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) }
where
@@ -233,7 +234,7 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty)
= addErrCtxt (cmdCtxt cmd) $
do { arg_ty <- newOpenFlexiTyVarTy
; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty)
- ; arg' <- tcLExpr arg (mkCheckExpType arg_ty)
+ ; arg' <- tcCheckMonoExpr arg arg_ty
; return (HsCmdApp x fun' arg') }
-------------------------------------------
@@ -310,7 +311,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty)
; let e_ty = mkInfForAllTy alphaTyVar $
mkVisFunTys cmd_tys $
mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty
- ; expr' <- tcCheckExpr expr e_ty
+ ; expr' <- tcCheckPolyExpr expr e_ty
; return (HsCmdArrForm x expr' f fixity cmd_args') }
where
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index 1870531f60..bd9d14e2d4 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -23,8 +23,9 @@ where
import GHC.Prelude
import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun )
-import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcLExpr )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckMonoExpr )
import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind )
+
import GHC.Core (Tickish (..))
import GHC.Types.CostCentre (mkUserCC, CCFlavour(DeclCC))
import GHC.Driver.Session
@@ -354,7 +355,7 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
= do { ty <- newOpenFlexiTyVarTy
; let p = mkStrLitTy $ hsIPNameFS ip
; ip_id <- newDict ipClass [ p, ty ]
- ; expr' <- tcLExpr expr (mkCheckExpType ty)
+ ; expr' <- tcCheckMonoExpr expr ty
; let d = toDict ipClass p ty `fmap` expr'
; return (ip_id, (IPBind noExtField (Right ip_id) d)) }
tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind"
@@ -389,22 +390,25 @@ tcValBinds top_lvl binds sigs thing_inside
-- It's easier to do so now, once for all the SCCs together
-- because a single signature f,g :: <type>
-- might relate to more than one SCC
- ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
+ (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
tcTySigs sigs
- -- Extend the envt right away with all the Ids
- -- declared with complete type signatures
- -- Do not extend the TcBinderStack; instead
- -- we extend it on a per-rhs basis in tcExtendForRhs
- ; tcExtendSigIds top_lvl poly_ids $ do
- { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
- { thing <- thing_inside
- -- See Note [Pattern synonym builders don't yield dependencies]
- -- in GHC.Rename.Bind
- ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns
- ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ]
- ; return (extra_binds, thing) }
- ; return (binds' ++ extra_binds', thing) }}
+ -- Extend the envt right away with all the Ids
+ -- declared with complete type signatures
+ -- Do not extend the TcBinderStack; instead
+ -- we extend it on a per-rhs basis in tcExtendForRhs
+ -- See Note [Relevant bindings and the binder stack]
+ ; tcExtendSigIds top_lvl poly_ids $
+ do { (binds', (extra_binds', thing))
+ <- tcBindGroups top_lvl sig_fn prag_fn binds $
+ do { thing <- thing_inside
+ -- See Note [Pattern synonym builders don't yield dependencies]
+ -- in GHC.Rename.Bind
+ ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns
+ ; let extra_binds = [ (NonRecursive, builder)
+ | builder <- patsyn_builders ]
+ ; return (extra_binds, thing) }
+ ; return (binds' ++ extra_binds', thing) }}
where
patsyns = getPatSynBinds binds
prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
@@ -686,50 +690,60 @@ tcPolyCheck prag_fn
(CompleteSig { sig_bndr = poly_id
, sig_ctxt = ctxt
, sig_loc = sig_loc })
- (L loc (FunBind { fun_id = (L nm_loc name)
- , fun_matches = matches }))
- = setSrcSpan sig_loc $
- do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
- ; (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id
- -- See Note [Instantiate sig with fresh variables]
+ (L bind_loc (FunBind { fun_id = L nm_loc name
+ , fun_matches = matches }))
+ = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
; mono_name <- newNameAt (nameOccName name) nm_loc
- ; ev_vars <- newEvVars theta
- ; let mono_id = mkLocalId mono_name tau
- skol_info = SigSkol ctxt (idType poly_id) tv_prs
- skol_tvs = map snd tv_prs
-
- ; (ev_binds, (co_fn, matches'))
- <- checkConstraints skol_info skol_tvs ev_vars $
- tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
- tcExtendNameTyVarEnv tv_prs $
- setSrcSpan loc $
- tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau)
+ ; (wrap_gen, (wrap_res, matches'))
+ <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
+ tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
+ -- Unwraps multiple layers; e.g
+ -- f :: forall a. Eq a => forall b. Ord b => blah
+ -- NB: tcSkolemise makes fresh type variables
+ -- See Note [Instantiate sig with fresh variables]
+
+ let mono_id = mkLocalId mono_name rho_ty in
+ tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
+ -- Why mono_id in the BinderStack?
+ -- See Note [Relevant bindings and the binder stack]
+
+ setSrcSpan bind_loc $
+ tcMatchesFun (L nm_loc mono_name) matches
+ (mkCheckExpType rho_ty)
+
+ -- We make a funny AbsBinds, abstracting over nothing,
+ -- just so we haev somewhere to put the SpecPrags.
+ -- Otherwise we could just use the FunBind
+ -- Hence poly_id2 is just a clone of poly_id;
+ -- We re-use mono-name, but we could equally well use a fresh one
; let prag_sigs = lookupPragEnv prag_fn name
- ; spec_prags <- tcSpecPrags poly_id prag_sigs
+ poly_id2 = mkLocalId mono_name (idType poly_id)
+ ; spec_prags <- tcSpecPrags poly_id prag_sigs
; poly_id <- addInlinePrags poly_id prag_sigs
; mod <- getModule
- ; tick <- funBindTicks nm_loc mono_id mod prag_sigs
- ; let bind' = FunBind { fun_id = L nm_loc mono_id
+ ; tick <- funBindTicks nm_loc poly_id mod prag_sigs
+
+ ; let bind' = FunBind { fun_id = L nm_loc poly_id2
, fun_matches = matches'
- , fun_ext = co_fn
+ , fun_ext = wrap_gen <.> wrap_res
, fun_tick = tick }
export = ABE { abe_ext = noExtField
, abe_wrap = idHsWrapper
, abe_poly = poly_id
- , abe_mono = mono_id
+ , abe_mono = poly_id2
, abe_prags = SpecPrags spec_prags }
- abs_bind = L loc $
+ abs_bind = L bind_loc $
AbsBinds { abs_ext = noExtField
- , abs_tvs = skol_tvs
- , abs_ev_vars = ev_vars
- , abs_ev_binds = [ev_binds]
+ , abs_tvs = []
+ , abs_ev_vars = []
+ , abs_ev_binds = []
, abs_exports = [export]
- , abs_binds = unitBag (L loc bind')
+ , abs_binds = unitBag (L bind_loc bind')
, abs_sig = True }
; return (unitBag abs_bind, [poly_id]) }
@@ -862,7 +876,7 @@ mkExport prag_fn insoluble qtvs theta
-- an ambiguous type and have AllowAmbiguousType
-- e..g infer x :: forall a. F a -> Int
else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $
- tcSubType_NC sig_ctxt sel_poly_ty poly_ty
+ tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty
; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures
; when warn_missing_sigs $
@@ -943,8 +957,12 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
, sig_inst_theta = annotated_theta
, sig_inst_skols = annotated_tvs }))
= -- Choose quantifiers for a partial type signature
- do { psig_qtvbndr_prs <- zonkTyVarTyVarPairs annotated_tvs
- ; let psig_qtv_prs = mapSnd binderVar psig_qtvbndr_prs
+ do { let (psig_qtv_nms, psig_qtv_bndrs) = unzip annotated_tvs
+ ; psig_qtv_bndrs <- mapM zonkInvisTVBinder psig_qtv_bndrs
+ ; let psig_qtvs = map binderVar psig_qtv_bndrs
+ psig_qtv_set = mkVarSet psig_qtvs
+ psig_qtv_prs = psig_qtv_nms `zip` psig_qtvs
+
-- Check whether the quantified variables of the
-- partial signature have been unified together
@@ -958,17 +976,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
, not (tv `elem` qtvs) ]
- ; let psig_qtvbndrs = map snd psig_qtvbndr_prs
- psig_qtvs = mkVarSet (map snd psig_qtv_prs)
-
; annotated_theta <- zonkTcTypes annotated_theta
- ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx
+ ; (free_tvs, my_theta) <- choose_psig_context psig_qtv_set annotated_theta wcx
- ; let keep_me = free_tvs `unionVarSet` psig_qtvs
+ ; let keep_me = free_tvs `unionVarSet` psig_qtv_set
final_qtvs = [ mkTyVarBinder vis tv
| tv <- qtvs -- Pulling from qtvs maintains original order
, tv `elemVarSet` keep_me
- , let vis = case lookupVarBndr tv psig_qtvbndrs of
+ , let vis = case lookupVarBndr tv psig_qtv_bndrs of
Just spec -> spec
Nothing -> InferredSpec ]
@@ -1454,17 +1469,7 @@ tcExtendTyVarEnvFromSig sig_inst thing_inside
thing_inside
tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
--- Extend the TcBinderStack for the RHS of the binding, with
--- the monomorphic Id. That way, if we have, say
--- f = \x -> blah
--- and something goes wrong in 'blah', we get a "relevant binding"
--- looking like f :: alpha -> beta
--- This applies if 'f' has a type signature too:
--- f :: forall a. [a] -> [a]
--- f x = True
--- We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
--- If we had the *polymorphic* version of f in the TcBinderStack, it
--- would not be reported as relevant, because its type is closed
+-- See Note [Relevant bindings and the binder stack]
tcExtendIdBinderStackForRhs infos thing_inside
= tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
| MBI { mbi_mono_id = mono_id } <- infos ]
@@ -1480,7 +1485,22 @@ getMonoBindInfo tc_binds
get_info (TcPatBind infos _ _ _) rest = infos ++ rest
-{- Note [Typechecking pattern bindings]
+{- Note [Relevant bindings and the binder stack]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When typecking a binding we extend the TcBinderStack for the RHS of
+the binding, with the /monomorphic/ Id. That way, if we have, say
+ f = \x -> blah
+and something goes wrong in 'blah', we get a "relevant binding"
+looking like f :: alpha -> beta
+This applies if 'f' has a type signature too:
+ f :: forall a. [a] -> [a]
+ f x = True
+We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
+If we had the *polymorphic* version of f in the TcBinderStack, it
+would not be reported as relevant, because its type is closed.
+(See TcErrors.relevantBindings.)
+
+Note [Typechecking pattern bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Look at:
- typecheck/should_compile/ExPat
diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs
index ab5e021653..9f31d7938a 100644
--- a/compiler/GHC/Tc/Gen/Default.hs
+++ b/compiler/GHC/Tc/Gen/Default.hs
@@ -70,8 +70,8 @@ tcDefaults decls@(L locn (DefaultDecl _ _) : _)
tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type
tc_default_ty deflt_clss hs_ty
- = do { (ty, _kind) <- solveEqualities $
- tcLHsType hs_ty
+ = do { ty <- solveEqualities $
+ tcInferLHsType hs_ty
; ty <- zonkTcTypeToType ty -- establish Type invariants
; checkValidType DefaultDeclCtxt ty
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 2d6b25df10..b4c3b6275c 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -13,20 +13,15 @@
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
--- | Typecheck an expression
module GHC.Tc.Gen.Expr
- ( tcCheckExpr
- , tcLExpr, tcLExprNC, tcExpr
- , tcInferSigma
- , tcInferRho, tcInferRhoNC
- , tcSyntaxOp, tcSyntaxOpGen
- , SyntaxOpType(..)
- , synKnownType
- , tcCheckId
- , addAmbiguousNameErr
- , getFixedTyVars
- )
-where
+ ( tcCheckPolyExpr,
+ tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC,
+ tcInferSigma, tcInferRho, tcInferRhoNC,
+ tcExpr,
+ tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
+ tcCheckId,
+ addAmbiguousNameErr,
+ getFixedTyVars ) where
#include "HsVersions.h"
@@ -101,25 +96,35 @@ import qualified Data.Set as Set
************************************************************************
-}
-tcCheckExpr, tcCheckExprNC
+
+tcCheckPolyExpr, tcCheckPolyExprNC
:: LHsExpr GhcRn -- Expression to type check
-> TcSigmaType -- Expected type (could be a polytype)
-> TcM (LHsExpr GhcTc) -- Generalised expr with expected type
--- tcCheckExpr is a convenient place (frequent but not too frequent)
+-- tcCheckPolyExpr is a convenient place (frequent but not too frequent)
-- place to add context information.
-- The NC version does not do so, usually because the caller wants
-- to do so himself.
-tcCheckExpr expr res_ty
+tcCheckPolyExpr expr res_ty = tcPolyExpr expr (mkCheckExpType res_ty)
+tcCheckPolyExprNC expr res_ty = tcPolyExprNC expr (mkCheckExpType res_ty)
+
+-- These versions take an ExpType
+tcPolyExpr, tcPolyExprNC
+ :: LHsExpr GhcRn -> ExpSigmaType
+ -> TcM (LHsExpr GhcTcId)
+
+tcPolyExpr expr res_ty
= addExprCtxt expr $
- tcCheckExprNC expr res_ty
+ do { traceTc "tcPolyExpr" (ppr res_ty)
+ ; tcPolyExprNC expr res_ty }
-tcCheckExprNC (L loc expr) res_ty
+tcPolyExprNC (L loc expr) res_ty
= setSrcSpan loc $
- do { traceTc "tcCheckExprNC" (ppr res_ty)
- ; (wrap, expr') <- tcSkolemise GenSigCtxt res_ty $ \ _ res_ty ->
- tcExpr expr (mkCheckExpType res_ty)
+ do { traceTc "tcPolyExprNC" (ppr res_ty)
+ ; (wrap, expr') <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty ->
+ tcExpr expr res_ty
; return $ L loc (mkHsWrap wrap expr') }
---------------
@@ -134,6 +139,30 @@ tcInferSigma le@(L loc expr)
; return (L loc (applyHsArgs fun args), ty) }
---------------
+tcCheckMonoExpr, tcCheckMonoExprNC
+ :: LHsExpr GhcRn -- Expression to type check
+ -> TcRhoType -- Expected type
+ -- Definitely no foralls at the top
+ -> TcM (LHsExpr GhcTcId)
+tcCheckMonoExpr expr res_ty = tcMonoExpr expr (mkCheckExpType res_ty)
+tcCheckMonoExprNC expr res_ty = tcMonoExprNC expr (mkCheckExpType res_ty)
+
+tcMonoExpr, tcMonoExprNC
+ :: LHsExpr GhcRn -- Expression to type check
+ -> ExpRhoType -- Expected type
+ -- Definitely no foralls at the top
+ -> TcM (LHsExpr GhcTcId)
+
+tcMonoExpr expr res_ty
+ = addExprCtxt expr $
+ tcMonoExprNC expr res_ty
+
+tcMonoExprNC (L loc expr) res_ty
+ = setSrcSpan loc $
+ do { expr' <- tcExpr expr res_ty
+ ; return (L loc expr') }
+
+---------------
tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
-- Infer a *rho*-type. The return type is always instantiated.
tcInferRho le = addExprCtxt le (tcInferRhoNC le)
@@ -144,15 +173,11 @@ tcInferRhoNC (L loc expr)
; return (L loc expr', rho) }
-{-
-************************************************************************
+{- *********************************************************************
* *
tcExpr: the main expression typechecker
* *
-************************************************************************
-
-NB: The res_ty is always deeply skolemised.
--}
+********************************************************************* -}
tcLExpr, tcLExprNC
:: LHsExpr GhcRn -- Expression to type check
@@ -241,7 +266,7 @@ tcExpr e@(HsOverLabel _ mb_fromLabel l) res_ty
(mkEmptyWildCardBndrs (L loc (HsTyLit noExtField (HsStrTy NoSourceText l))))
tcExpr (HsLam x match) res_ty
- = do { (match', wrap) <- tcMatchLambda herald match_ctxt match res_ty
+ = do { (wrap, match') <- tcMatchLambda herald match_ctxt match res_ty
; return (mkHsWrap wrap (HsLam x match')) }
where
match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody }
@@ -252,7 +277,7 @@ tcExpr (HsLam x match) res_ty
text "has"]
tcExpr e@(HsLamCase x matches) res_ty
- = do { (matches', wrap)
+ = do { (wrap, matches')
<- tcMatchLambda msg match_ctxt matches res_ty
-- The laziness annotation is because we don't want to fail here
-- if there are multiple arguments
@@ -335,7 +360,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
; let doc = text "The first argument of ($) takes"
orig1 = lexprCtOrigin arg1
; (wrap_arg1, [arg2_sigma], op_res_ty) <-
- matchActualFunTys doc orig1 (Just (unLoc arg1)) 1 arg1_ty
+ matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty
-- We have (arg1 $ arg2)
-- So: arg1_ty = arg2_ty -> op_res_ty
@@ -351,7 +376,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
(tcTypeKind arg2_sigma) liftedTypeKind
-- Ignore the evidence. arg2_sigma must have type * or #,
-- because we know (arg2_sigma -> op_res_ty) is well-kinded
- -- (because otherwise matchActualFunTys would fail)
+ -- (because otherwise matchActualFunTysRho would fail)
-- So this 'unifyKind' will either succeed with Refl, or will
-- produce an insoluble constraint * ~ #, which we'll report later.
@@ -385,7 +410,8 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
; (op', op_ty) <- tcInferRhoNC op
; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
- <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
+ <- matchActualFunTysRho (mk_op_msg op) fn_orig
+ (Just (unLoc op)) 2 op_ty
-- You might think we should use tcInferApp here, but there is
-- too much impedance-matching, because tcApp may return wrappers as
-- well as type-checked arguments.
@@ -405,12 +431,13 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
tcExpr expr@(SectionR x op arg2) res_ty
= do { (op', op_ty) <- tcInferRhoNC op
; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
- <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
- ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
- (mkVisFunTy arg1_ty op_res_ty) res_ty
+ <- matchActualFunTysRho (mk_op_msg op) fn_orig
+ (Just (unLoc op)) 2 op_ty
; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2
- ; return ( mkHsWrap wrap_res $
- SectionR x (mkLHsWrap wrap_fun op') arg2' ) }
+ ; let expr' = SectionR x (mkLHsWrap wrap_fun op') arg2'
+ act_res_ty = mkVisFunTy arg1_ty op_res_ty
+ ; tcWrapResultMono expr expr' act_res_ty res_ty }
+
where
fn_orig = lexprCtOrigin op
-- It's important to use the origin of 'op', so that call-stacks
@@ -424,13 +451,12 @@ tcExpr expr@(SectionL x arg1 op) res_ty
| otherwise = 2
; (wrap_fn, (arg1_ty:arg_tys), op_res_ty)
- <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op))
- n_reqd_args op_ty
- ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr)
- (mkVisFunTys arg_tys op_res_ty) res_ty
+ <- matchActualFunTysRho (mk_op_msg op) fn_orig
+ (Just (unLoc op)) n_reqd_args op_ty
; arg1' <- tcArg (unLoc op) arg1 arg1_ty 1
- ; return ( mkHsWrap wrap_res $
- SectionL x arg1' (mkLHsWrap wrap_fn op') ) }
+ ; let expr' = SectionL x arg1' (mkLHsWrap wrap_fn op')
+ act_res_ty = mkVisFunTys arg_tys op_res_ty
+ ; tcWrapResultMono expr expr' act_res_ty res_ty }
where
fn_orig = lexprCtOrigin op
-- It's important to use the origin of 'op', so that call-stacks
@@ -460,19 +486,19 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty
; arg_tys <- case boxity of
{ Boxed -> newFlexiTyVarTys arity liftedTypeKind
; Unboxed -> replicateM arity newOpenFlexiTyVarTy }
- ; let actual_res_ty
- = mkVisFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args]
- (mkTupleTy1 boxity arg_tys)
- -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
-
- ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple")
- (Just expr)
- actual_res_ty res_ty
-- Handle tuple sections where
; tup_args1 <- tcTupArgs tup_args arg_tys
- ; return $ mkHsWrap wrap (ExplicitTuple x tup_args1 boxity) }
+ ; let expr' = ExplicitTuple x tup_args1 boxity
+ act_res_ty = mkVisFunTys [ty | (ty, (L _ (Missing _)))
+ <- arg_tys `zip` tup_args]
+ (mkTupleTy1 boxity arg_tys)
+ -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
+
+ ; traceTc "ExplicitTuple" (ppr act_res_ty $$ ppr res_ty)
+
+ ; tcWrapResultMono expr expr' act_res_ty res_ty }
tcExpr (ExplicitSum _ alt arity expr) res_ty
= do { let sum_tc = sumTyCon arity
@@ -480,7 +506,7 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty
; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty
; -- Drop levity vars, we don't care about them here
let arg_tys' = drop arity arg_tys
- ; expr' <- tcCheckExpr expr (arg_tys' `getNth` (alt - 1))
+ ; expr' <- tcCheckPolyExpr expr (arg_tys' `getNth` (alt - 1))
; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) }
-- This will see the empty list only when -XOverloadedLists.
@@ -502,7 +528,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty
; return (exprs', elt_ty) }
; return $ ExplicitList elt_ty (Just fln') exprs' }
- where tc_elt elt_ty expr = tcCheckExpr expr elt_ty
+ where tc_elt elt_ty expr = tcCheckPolyExpr expr elt_ty
{-
************************************************************************
@@ -527,6 +553,13 @@ tcExpr (HsCase x scrut matches) res_ty
--
-- But now, in the GADT world, we need to typecheck the scrutinee
-- first, to get type info that may be refined in the case alternatives
+
+ -- Typecheck the scrutinee. We use tcInferRho but tcInferSigma
+ -- would also be possible (tcMatchesCase accepts sigma-types)
+ -- Interesting litmus test: do these two behave the same?
+ -- case id of {..}
+ -- case (\v -> v) of {..}
+ -- This design choice is discussed in #17790
(scrut', scrut_ty) <- tcInferRho scrut
; traceTc "HsCase" (ppr scrut_ty)
@@ -550,9 +583,9 @@ tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty
= do { ((pred', b1', b2'), fun')
<- tcSyntaxOp IfOrigin fun [SynAny, SynAny, SynAny] res_ty $
\ [pred_ty, b1_ty, b2_ty] ->
- do { pred' <- tcCheckExpr pred pred_ty
- ; b1' <- tcCheckExpr b1 b1_ty
- ; b2' <- tcCheckExpr b2 b2_ty
+ do { pred' <- tcCheckPolyExpr pred pred_ty
+ ; b1' <- tcCheckPolyExpr b1 b1_ty
+ ; b2' <- tcCheckPolyExpr b2 b2_ty
; return (pred', b1', b2') }
; return (HsIf x fun' pred' b1' b2') }
@@ -591,7 +624,7 @@ tcExpr (HsStatic fvs expr) res_ty
addErrCtxt (hang (text "In the body of a static form:")
2 (ppr expr)
) $
- tcCheckExprNC expr expr_ty
+ tcCheckPolyExprNC expr expr_ty
-- Check that the free variables of the static form are closed.
-- It's OK to use nonDetEltsUniqSet here as the only side effects of
@@ -637,25 +670,26 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name
; checkMissingFields con_like rbinds
; (con_expr, con_sigma) <- tcInferId con_name
- ; (con_wrap, con_tau) <-
- topInstantiate (OccurrenceOf con_name) con_sigma
+ ; (con_wrap, con_tau) <- topInstantiate orig con_sigma
-- a shallow instantiation should really be enough for
-- a data constructor.
; let arity = conLikeArity con_like
Right (arg_tys, actual_res_ty) = tcSplitFunTysN arity con_tau
- ; case conLikeWrapId_maybe con_like of
- Nothing -> nonBidirectionalErr (conLikeName con_like)
- Just con_id -> do {
- res_wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "RecordCon")
- (Just expr) actual_res_ty res_ty
- ; rbinds' <- tcRecordBinds con_like arg_tys rbinds
- ; return $
- mkHsWrap res_wrap $
- RecordCon { rcon_ext = RecordConTc
- { rcon_con_like = con_like
- , rcon_con_expr = mkHsWrap con_wrap con_expr }
- , rcon_con_name = L loc con_id
- , rcon_flds = rbinds' } } }
+ ; case conLikeWrapId_maybe con_like of {
+ Nothing -> nonBidirectionalErr (conLikeName con_like) ;
+ Just con_id ->
+
+ do { rbinds' <- tcRecordBinds con_like arg_tys rbinds
+ ; let rcon_tc = RecordConTc
+ { rcon_con_like = con_like
+ , rcon_con_expr = mkHsWrap con_wrap con_expr }
+ expr' = RecordCon { rcon_ext = rcon_tc
+ , rcon_con_name = L loc con_id
+ , rcon_flds = rbinds' }
+
+ ; tcWrapResultMono expr expr' actual_res_ty res_ty } } }
+ where
+ orig = OccurrenceOf con_name
{-
Note [Type of a record update]
@@ -906,8 +940,6 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
scrut_ty = TcType.substTy scrut_subst con1_res_ty
con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
- ; wrap_res <- tcSubTypeHR (exprCtOrigin expr)
- (Just expr) rec_res_ty res_ty
; co_scrut <- unifyType (Just (unLoc record_expr)) record_rho scrut_ty
-- NB: normal unification is OK here (as opposed to subsumption),
-- because for this to work out, both record_rho and scrut_ty have
@@ -937,16 +969,16 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
; req_wrap <- instCallConstraints RecordUpdOrigin req_theta'
-- Phew!
- ; return $
- mkHsWrap wrap_res $
- RecordUpd { rupd_expr
- = mkLHsWrap fam_co (mkLHsWrapCo co_scrut record_expr')
- , rupd_flds = rbinds'
- , rupd_ext = RecordUpdTc
- { rupd_cons = relevant_cons
- , rupd_in_tys = scrut_inst_tys
- , rupd_out_tys = result_inst_tys
- , rupd_wrap = req_wrap }} }
+ ; let upd_tc = RecordUpdTc { rupd_cons = relevant_cons
+ , rupd_in_tys = scrut_inst_tys
+ , rupd_out_tys = result_inst_tys
+ , rupd_wrap = req_wrap }
+ expr' = RecordUpd { rupd_expr = mkLHsWrap fam_co $
+ mkLHsWrapCo co_scrut record_expr'
+ , rupd_flds = rbinds'
+ , rupd_ext = upd_tc }
+
+ ; tcWrapResult expr expr' rec_res_ty res_ty }
tcExpr e@(HsRecFld _ f) res_ty
= tcCheckRecSelId e f res_ty
@@ -1038,7 +1070,7 @@ tcArithSeq :: Maybe (SyntaxExpr GhcRn) -> ArithSeqInfo GhcRn -> ExpRhoType
tcArithSeq witness seq@(From expr) res_ty
= do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
- ; expr' <- tcCheckExpr expr elt_ty
+ ; expr' <- tcCheckPolyExpr expr elt_ty
; enum_from <- newMethodFromName (ArithSeqOrigin seq)
enumFromName [elt_ty]
; return $ mkHsWrap wrap $
@@ -1046,8 +1078,8 @@ tcArithSeq witness seq@(From expr) res_ty
tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
= do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
- ; expr1' <- tcCheckExpr expr1 elt_ty
- ; expr2' <- tcCheckExpr expr2 elt_ty
+ ; expr1' <- tcCheckPolyExpr expr1 elt_ty
+ ; expr2' <- tcCheckPolyExpr expr2 elt_ty
; enum_from_then <- newMethodFromName (ArithSeqOrigin seq)
enumFromThenName [elt_ty]
; return $ mkHsWrap wrap $
@@ -1055,8 +1087,8 @@ tcArithSeq witness seq@(FromThen expr1 expr2) res_ty
tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
= do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
- ; expr1' <- tcCheckExpr expr1 elt_ty
- ; expr2' <- tcCheckExpr expr2 elt_ty
+ ; expr1' <- tcCheckPolyExpr expr1 elt_ty
+ ; expr2' <- tcCheckPolyExpr expr2 elt_ty
; enum_from_to <- newMethodFromName (ArithSeqOrigin seq)
enumFromToName [elt_ty]
; return $ mkHsWrap wrap $
@@ -1064,9 +1096,9 @@ tcArithSeq witness seq@(FromTo expr1 expr2) res_ty
tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty
= do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty
- ; expr1' <- tcCheckExpr expr1 elt_ty
- ; expr2' <- tcCheckExpr expr2 elt_ty
- ; expr3' <- tcCheckExpr expr3 elt_ty
+ ; expr1' <- tcCheckPolyExpr expr1 elt_ty
+ ; expr2' <- tcCheckPolyExpr expr2 elt_ty
+ ; expr3' <- tcCheckPolyExpr expr3 elt_ty
; eft <- newMethodFromName (ArithSeqOrigin seq)
enumFromThenToName [elt_ty]
; return $ mkHsWrap wrap $
@@ -1251,13 +1283,11 @@ tcInferApp expr
Nothing -> thing_inside -- Don't set the location twice
Just loc -> setSrcSpan loc thing_inside
----------------------
tcInferApp_finish
:: HsExpr GhcRn -- Renamed function
-> HsExpr GhcTc -> TcSigmaType -- Function and its type
-> [LHsExprArgIn] -- Arguments
-> TcM (HsExpr GhcTc, [LHsExprArgOut], TcSigmaType)
-
tcInferApp_finish rn_fun tc_fun fun_sigma rn_args
= do { (tc_args, actual_res_ty) <- tcArgs rn_fun fun_sigma rn_args
; return (tc_fun, tc_args, actual_res_ty) }
@@ -1364,9 +1394,9 @@ tcArgs fun orig_fun_ty orig_args
_ -> ty_app_err upsilon_ty hs_ty_arg }
go n so_far fun_ty (HsEValArg loc arg : args)
- = do { (wrap, [arg_ty], res_ty)
- <- matchActualFunTysPart herald fun_orig (Just fun)
- n_val_args so_far 1 fun_ty
+ = do { (wrap, arg_ty, res_ty)
+ <- matchActualFunTySigma herald fun_orig (Just fun)
+ (n_val_args, so_far) fun_ty
; arg' <- tcArg fun arg arg_ty n
; (args', inner_res_ty) <- go (n+1) (arg_ty:so_far) res_ty args
; return ( addArgWrap wrap $ HsEValArg loc arg' : args'
@@ -1465,13 +1495,12 @@ tcArg :: HsExpr GhcRn -- The function (for error messages)
-> Int -- # of argument
-> TcM (LHsExpr GhcTc) -- Resulting argument
tcArg fun arg ty arg_no
- = addErrCtxt (funAppCtxt fun arg arg_no) $
- do { traceTc "tcArg {" $
- vcat [ text "arg #" <> ppr arg_no <+> dcolon <+> ppr ty
- , text "arg:" <+> ppr arg ]
- ; arg' <- tcCheckExprNC arg ty
- ; traceTc "tcArg }" empty
- ; return arg' }
+ = addErrCtxt (funAppCtxt fun arg arg_no) $
+ do { traceTc "tcArg" $
+ vcat [ ppr arg_no <+> text "of" <+> ppr fun
+ , text "arg type:" <+> ppr ty
+ , text "arg:" <+> ppr arg ]
+ ; tcCheckPolyExprNC arg ty }
----------------
tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTc]
@@ -1479,7 +1508,7 @@ tcTupArgs args tys
= ASSERT( equalLength args tys ) mapM go (args `zip` tys)
where
go (L l (Missing {}), arg_ty) = return (L l (Missing arg_ty))
- go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckExpr expr arg_ty
+ go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty
; return (L l (Present x expr')) }
---------------------------
@@ -1536,7 +1565,7 @@ tcSynArgE :: CtOrigin
-- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
tcSynArgE orig sigma_ty syn_ty thing_inside
= do { (skol_wrap, (result, ty_wrapper))
- <- tcSkolemise GenSigCtxt sigma_ty $ \ _ rho_ty ->
+ <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty ->
go rho_ty syn_ty
; return (result, skol_wrap <.> ty_wrapper) }
where
@@ -1554,11 +1583,11 @@ tcSynArgE orig sigma_ty syn_ty thing_inside
; return (result, mkWpCastN list_co) }
go rho_ty (SynFun arg_shape res_shape)
- = do { ( ( ( (result, arg_ty, res_ty)
- , res_wrapper ) -- :: res_ty_out "->" res_ty
- , arg_wrapper1, [], arg_wrapper2 ) -- :: arg_ty "->" arg_ty_out
- , match_wrapper ) -- :: (arg_ty -> res_ty) "->" rho_ty
- <- matchExpectedFunTys herald 1 (mkCheckExpType rho_ty) $
+ = do { ( match_wrapper -- :: (arg_ty -> res_ty) "->" rho_ty
+ , ( ( (result, arg_ty, res_ty)
+ , res_wrapper ) -- :: res_ty_out "->" res_ty
+ , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out
+ <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $
\ [arg_ty] res_ty ->
do { arg_tc_ty <- expTypeToType arg_ty
; res_tc_ty <- expTypeToType res_ty
@@ -1604,7 +1633,8 @@ tcSynArgA :: CtOrigin
-- and a wrapper to be applied to the overall expression
tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside
= do { (match_wrapper, arg_tys, res_ty)
- <- matchActualFunTys herald orig Nothing (length arg_shapes) sigma_ty
+ <- matchActualFunTysRho herald orig Nothing
+ (length arg_shapes) sigma_ty
-- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty)
; ((result, res_wrapper), arg_wrappers)
<- tc_syn_args_e arg_tys arg_shapes $ \ arg_results ->
@@ -1634,7 +1664,7 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside
= do { result <- thing_inside [res_ty]
; return (result, idHsWrapper) }
tc_syn_arg res_ty SynRho thing_inside
- = do { (inst_wrap, rho_ty) <- deeplyInstantiate orig res_ty
+ = do { (inst_wrap, rho_ty) <- topInstantiate orig res_ty
-- inst_wrap :: res_ty "->" rho_ty
; result <- thing_inside [rho_ty]
; return (result, inst_wrap) }
@@ -1648,7 +1678,7 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside
tc_syn_arg _ (SynFun {}) _
= pprPanic "tcSynArgA hits a SynFun" (ppr orig)
tc_syn_arg res_ty (SynType the_ty) thing_inside
- = do { wrap <- tcSubTypeO orig GenSigCtxt res_ty the_ty
+ = do { wrap <- tcSubType orig GenSigCtxt res_ty the_ty
; result <- thing_inside []
; return (result, wrap) }
@@ -1687,22 +1717,10 @@ in the other order, the extra signature in f2 is reqd.
tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
= setSrcSpan loc $ -- Sets the location for the implication constraint
- do { (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id
- ; given <- newEvVars theta
- ; traceTc "tcExprSig: CompleteSig" $
- vcat [ text "poly_id:" <+> ppr poly_id <+> dcolon <+> ppr (idType poly_id)
- , text "tv_prs:" <+> ppr tv_prs ]
-
- ; let skol_info = SigSkol ExprSigCtxt (idType poly_id) tv_prs
- skol_tvs = map snd tv_prs
- ; (ev_binds, expr') <- checkConstraints skol_info skol_tvs given $
- tcExtendNameTyVarEnv tv_prs $
- tcCheckExprNC expr tau
-
- ; let poly_wrap = mkWpTyLams skol_tvs
- <.> mkWpLams given
- <.> mkWpLet ev_binds
- ; return (mkLHsWrap poly_wrap expr', idType poly_id) }
+ do { let poly_ty = idType poly_id
+ ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty ->
+ tcCheckMonoExprNC expr rho_ty
+ ; return (mkLHsWrap wrap expr', poly_ty) }
tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
= setSrcSpan loc $ -- Sets the location for the implication constraint
@@ -1711,7 +1729,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
do { sig_inst <- tcInstSig sig
; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $
tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $
- tcCheckExprNC expr (sig_inst_tau sig_inst)
+ tcCheckPolyExprNC expr (sig_inst_tau sig_inst)
; return (expr', sig_inst) }
-- See Note [Partial expression signatures]
; let tau = sig_inst_tau sig_inst
@@ -1735,7 +1753,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
then return idHsWrapper -- Fast path; also avoids complaint when we infer
-- an ambiguous type and have AllowAmbiguousType
-- e..g infer x :: forall a. F a -> Int
- else tcSubType_NC ExprSigCtxt inferred_sigma my_sigma
+ else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma
; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
; let poly_wrap = wrap
@@ -2476,7 +2494,7 @@ tcRecordField :: ConLike -> Assoc Name Type
tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs
| Just field_ty <- assocMaybe flds_w_tys sel_name
= addErrCtxt (fieldCtxt field_lbl) $
- do { rhs' <- tcCheckExprNC rhs field_ty
+ do { rhs' <- tcCheckPolyExprNC rhs field_ty
; let field_id = mkUserLocal (nameOccName sel_name)
(nameUnique sel_name)
field_ty loc
@@ -2584,7 +2602,7 @@ addFunResCtxt has_args fun fun_res_ty env_ty
-- function types]
(_, _, fun_tau) = tcSplitNestedSigmaTys fun_res'
-- No need to call tcSplitNestedSigmaTys here, since env_ty is
- -- an ExpRhoTy, i.e., it's already deeply instantiated.
+ -- an ExpRhoTy, i.e., it's already instantiated.
(_, _, env_tau) = tcSplitSigmaTy env'
(args_fun, res_fun) = tcSplitFunTys fun_tau
(args_env, res_env) = tcSplitFunTys env_tau
diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot
index d9138a4d7e..1f26ef242a 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs-boot
+++ b/compiler/GHC/Tc/Gen/Expr.hs-boot
@@ -6,16 +6,26 @@ import GHC.Tc.Types ( TcM )
import GHC.Tc.Types.Origin ( CtOrigin )
import GHC.Hs.Extension ( GhcRn, GhcTcId )
-tcCheckExpr :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTcId)
-
-tcLExpr, tcLExprNC
- :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId)
-tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
-
-tcInferRho, tcInferRhoNC
- :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcRhoType)
-
-tcInferSigma :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcSigmaType)
+tcCheckPolyExpr ::
+ LHsExpr GhcRn
+ -> TcSigmaType
+ -> TcM (LHsExpr GhcTcId)
+
+tcMonoExpr, tcMonoExprNC ::
+ LHsExpr GhcRn
+ -> ExpRhoType
+ -> TcM (LHsExpr GhcTcId)
+tcCheckMonoExpr, tcCheckMonoExprNC ::
+ LHsExpr GhcRn
+ -> TcRhoType
+ -> TcM (LHsExpr GhcTcId)
+
+tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId)
+
+tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
+
+tcInferRho, tcInferRhoNC ::
+ LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcRhoType)
tcSyntaxOp :: CtOrigin
-> SyntaxExprRn
diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs
index 8163e6820d..06febcef33 100644
--- a/compiler/GHC/Tc/Gen/Foreign.hs
+++ b/compiler/GHC/Tc/Gen/Foreign.hs
@@ -388,7 +388,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe
= addErrCtxt (foreignDeclCtxt fo) $ do
sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty
- rhs <- tcCheckExpr (nlHsVar nm) sig_ty
+ rhs <- tcCheckPolyExpr (nlHsVar nm) sig_ty
(norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index cdbaab115b..1cd4e27c8d 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -31,8 +31,8 @@ module GHC.Tc.Gen.HsType (
bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol,
ContextKind(..),
- -- Type checking type and class decls
- bindTyClTyVars,
+ -- Type checking type and class decls, and instances thereof
+ bindTyClTyVars, tcFamTyPats,
etaExpandAlgTyCon, tcbVisibilities,
-- tyvars
@@ -46,13 +46,11 @@ module GHC.Tc.Gen.HsType (
tcNamedWildCardBinders,
tcHsLiftedType, tcHsOpenType,
tcHsLiftedTypeNC, tcHsOpenTypeNC,
- tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType,
- tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps,
+ tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType,
+ tcHsMbContext, tcHsContext, tcLHsPredType,
failIfEmitsConstraints,
solveEqualities, -- useful re-export
- typeLevelMode, kindLevelMode,
-
kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone,
-- Sort-checking kinds
@@ -115,6 +113,7 @@ import GHC.Driver.Session
import qualified GHC.LanguageExtensions as LangExt
import GHC.Data.Maybe
+import GHC.Data.Bag( unitBag )
import Data.List ( find )
import Control.Monad
@@ -159,6 +158,91 @@ checking until step (3).
Check types AND do validity checking
* *
************************************************************************
+
+Note [Keeping implicitly quantified variables in order]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When the user implicitly quantifies over variables (say, in a type
+signature), we need to come up with some ordering on these variables.
+This is done by bumping the TcLevel, bringing the tyvars into scope,
+and then type-checking the thing_inside. The constraints are all
+wrapped in an implication, which is then solved. Finally, we can
+zonk all the binders and then order them with scopedSort.
+
+It's critical to solve before zonking and ordering in order to uncover
+any unifications. You might worry that this eager solving could cause
+trouble elsewhere. I don't think it will. Because it will solve only
+in an increased TcLevel, it can't unify anything that was mentioned
+elsewhere. Additionally, we require that the order of implicitly
+quantified variables is manifest by the scope of these variables, so
+we're not going to learn more information later that will help order
+these variables.
+
+Note [Recipe for checking a signature]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Checking a user-written signature requires several steps:
+
+ 1. Generate constraints.
+ 2. Solve constraints.
+ 3. Promote tyvars and/or kind-generalize.
+ 4. Zonk.
+ 5. Check validity.
+
+There may be some surprises in here:
+
+Step 2 is necessary for two reasons: most signatures also bring
+implicitly quantified variables into scope, and solving is necessary
+to get these in the right order (see Note [Keeping implicitly
+quantified variables in order]). Additionally, solving is necessary in
+order to kind-generalize correctly: otherwise, we do not know which
+metavariables are left unsolved.
+
+Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
+kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
+metatyvars generated in the type may have a bumped TcLevel, because explicit
+foralls raise the TcLevel. To avoid these variables from ever being visible in
+the surrounding context, we must obey the following dictum:
+
+ Every metavariable in a type must either be
+ (A) generalized, or
+ (B) promoted, or See Note [Promotion in signatures]
+ (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType
+
+The kindGeneralize functions do not require pre-zonking; they zonk as they
+go.
+
+If you are actually doing kind-generalization, you need to bump the level
+before generating constraints, as we will only generalize variables with
+a TcLevel higher than the ambient one.
+
+After promoting/generalizing, we need to zonk again because both
+promoting and generalizing fill in metavariables.
+
+Note [Promotion in signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If an unsolved metavariable in a signature is not generalized
+(because we're not generalizing the construct -- e.g., pattern
+sig -- or because the metavars are constrained -- see kindGeneralizeSome)
+we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables]
+in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing
+and the reinstantiating with a fresh metavariable at the current level.
+So in some sense, we generalize *all* variables, but then re-instantiate
+some of them.
+
+Here is an example of why we must promote:
+ foo (x :: forall a. a -> Proxy b) = ...
+
+In the pattern signature, `b` is unbound, and will thus be brought into
+scope. We do not know its kind: it will be assigned kappa[2]. Note that
+kappa is at TcLevel 2, because it is invented under a forall. (A priori,
+the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel
+than the surrounding context.) This kappa cannot be solved for while checking
+the pattern signature (which is not kind-generalized). When we are checking
+the *body* of foo, though, we need to unify the type of x with the argument
+type of bar. At this point, the ambient TcLevel is 1, and spotting a
+matavariable with level 2 would violate the (WantedTvInv) invariant of
+Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing,
+we promote the metavariable to level 1. This is all done in kindGeneralizeNone.
+
-}
funsSigCtxt :: [Located Name] -> UserTypeCtxt
@@ -213,19 +297,21 @@ kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars
<- pushTcLevelM $
solveLocalEqualitiesX "kcClassSigType" $
bindImplicitTKBndrs_Skol sig_vars $
- tc_lhs_type typeLevelMode hs_ty liftedTypeKind
+ tcLHsType hs_ty liftedTypeKind
- ; emitResidualTvConstraint skol_info Nothing spec_tkvs
- tc_lvl wanted }
+ ; emitResidualTvConstraint skol_info spec_tkvs tc_lvl wanted }
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
-- Does not do validity checking
tcClassSigType skol_info names sig_ty
= addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
- snd <$> tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
+ do { (implic, ty) <- tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind)
+ ; emitImplication implic
+ ; return ty }
-- Do not zonk-to-Type, nor perform a validity check
-- We are in a knot with the class and associated types
-- Zonking and validity checking is done by tcClassDecl
+ --
-- No need to fail here if the type has an error:
-- If we're in the kind-checking phase, the solveEqualities
-- in kcTyClGroup catches the error
@@ -247,46 +333,36 @@ tcHsSigType ctxt sig_ty
do { traceTc "tcHsSigType {" (ppr sig_ty)
-- Generalise here: see Note [Kind generalisation]
- ; (insol, ty) <- tc_hs_sig_type skol_info sig_ty
- (expectedKindInCtxt ctxt)
- ; ty <- zonkTcType ty
+ ; (implic, ty) <- tc_hs_sig_type skol_info sig_ty (expectedKindInCtxt ctxt)
- ; when insol failM
- -- See Note [Fail fast if there are insoluble kind equalities] in GHC.Tc.Solver
+ -- Spit out the implication (and perhaps fail fast)
+ -- See Note [Failure in local type signatures] in GHC.Tc.Solver
+ ; emitFlatConstraints (mkImplicWC (unitBag implic))
+ ; ty <- zonkTcType ty
; checkValidType ctxt ty
; traceTc "end tcHsSigType }" (ppr ty)
; return ty }
where
skol_info = SigTypeSkol ctxt
--- Does validity checking and zonking.
-tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
-tcStandaloneKindSig (L _ kisig) = case kisig of
- StandaloneKindSig _ (L _ name) ksig ->
- let ctxt = StandaloneKindSigCtxt name in
- addSigCtxt ctxt (hsSigType ksig) $
- do { kind <- tcTopLHsType kindLevelMode ksig (expectedKindInCtxt ctxt)
- ; checkValidType ctxt kind
- ; return (name, kind) }
-
tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn
- -> ContextKind -> TcM (Bool, TcType)
+ -> ContextKind -> TcM (Implication, TcType)
-- Kind-checks/desugars an 'LHsSigType',
-- solve equalities,
-- and then kind-generalizes.
-- This will never emit constraints, as it uses solveEqualities internally.
-- No validity checking or zonking
--- Returns also a Bool indicating whether the type induced an insoluble constraint;
--- True <=> constraint is insoluble
+-- Returns also an implication for the unsolved constraints
tc_hs_sig_type skol_info hs_sig_type ctxt_kind
| HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
= do { (tc_lvl, (wanted, (spec_tkvs, ty)))
<- pushTcLevelM $
solveLocalEqualitiesX "tc_hs_sig_type" $
+ -- See Note [Failure in local type signatures]
bindImplicitTKBndrs_Skol sig_vars $
do { kind <- newExpectedKind ctxt_kind
- ; tc_lhs_type typeLevelMode hs_ty kind }
+ ; tcLHsType hs_ty kind }
-- Any remaining variables (unsolved in the solveLocalEqualities)
-- should be in the global tyvars, and therefore won't be quantified
@@ -301,18 +377,67 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
; let should_gen = not . (`elemVarSet` constrained)
; kvs <- kindGeneralizeSome should_gen ty1
- ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs)
- tc_lvl wanted
- ; return (insolubleWC wanted, mkInfForAllTys kvs ty1) }
+ -- Build an implication for any as-yet-unsolved kind equalities
+ -- See Note [Skolem escape in type signatures]
+ ; implic <- buildTvImplication skol_info (kvs ++ spec_tkvs) tc_lvl wanted
+
+ ; return (implic, mkInfForAllTys kvs ty1) }
+
+{- Note [Skolem escape in type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+tcHsSigType is tricky. Consider (T11142)
+ foo :: forall b. (forall k (a :: k). SameKind a b) -> ()
+This is ill-kinded becuase of a nested skolem-escape.
+
+That will show up as an un-solvable constraint in the implication
+returned by buildTvImplication in tc_hs_sig_type. See Note [Skolem
+escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable
+(the unification variable for b's kind is untouchable).
+
+Then, in GHC.Tc.Solver.emitFlatConstraints (called from tcHsSigType)
+we'll try to float out the constraint, be unable to do so, and fail.
+See GHC.Tc.Solver Note [Failure in local type signatures] for more
+detail on this.
+
+The separation between tcHsSigType and tc_hs_sig_type is because
+tcClassSigType wants to use the latter, but *not* fail fast, because
+there are skolems from the class decl which are in scope; but it's fine
+not to because tcClassDecl1 has a solveEqualities wrapped around all
+the tcClassSigType calls.
+
+That's why tcHsSigType does emitFlatConstraints (which fails fast) but
+tcClassSigType just does emitImplication (which does not). Ugh.
+
+c.f. see also Note [Skolem escape and forall-types]. The difference
+is that we don't need to simplify at a forall type, only at the
+top level of a signature.
+-}
+
+-- Does validity checking and zonking.
+tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind)
+tcStandaloneKindSig (L _ kisig) = case kisig of
+ StandaloneKindSig _ (L _ name) ksig ->
+ let ctxt = StandaloneKindSigCtxt name in
+ addSigCtxt ctxt (hsSigType ksig) $
+ do { let mode = mkMode KindLevel
+ ; kind <- tc_top_lhs_type mode ksig (expectedKindInCtxt ctxt)
+ ; checkValidType ctxt kind
+ ; return (name, kind) }
+
-tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
+tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
+tcTopLHsType hs_ty ctxt_kind
+ = tc_top_lhs_type (mkMode TypeLevel) hs_ty ctxt_kind
+
+tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where
-- we want to fully solve /all/ equalities, and report errors
-- Does zonking, but not validity checking because it's used
-- for things (like deriving and instances) that aren't
-- ordinary types
-tcTopLHsType mode hs_sig_type ctxt_kind
+-- Used for both types and kinds
+tc_top_lhs_type mode hs_sig_type ctxt_kind
| HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type
= do { traceTc "tcTopLHsType {" (ppr hs_ty)
; (spec_tkvs, ty)
@@ -340,7 +465,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind])
tcHsDeriv hs_ty
= do { ty <- checkNoErrs $ -- Avoid redundant error report
-- with "illegal deriving", below
- tcTopLHsType typeLevelMode hs_ty AnyKind
+ tcTopLHsType hs_ty AnyKind
; let (tvs, pred) = splitForAllTys ty
(kind_args, _) = splitFunTys (tcTypeKind pred)
; case getClassPredTys_maybe pred of
@@ -369,7 +494,7 @@ tcDerivStrategy mb_lds
tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy
tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy
tc_deriv_strategy (ViaStrategy ty) = do
- ty' <- checkNoErrs $ tcTopLHsType typeLevelMode ty AnyKind
+ ty' <- checkNoErrs $ tcTopLHsType ty AnyKind
let (via_tvs, via_pred) = splitForAllTys ty'
pure (ViaStrategy via_pred, via_tvs)
@@ -387,7 +512,7 @@ tcHsClsInstType user_ctxt hs_inst_ty
-- eagerly avoids follow-on errors when checkValidInstance
-- sees an unsolved coercion hole
inst_ty <- checkNoErrs $
- tcTopLHsType typeLevelMode hs_inst_ty (TheKind constraintKind)
+ tcTopLHsType hs_inst_ty (TheKind constraintKind)
; checkValidInstance user_ctxt hs_inst_ty inst_ty
; return inst_ty }
@@ -397,14 +522,15 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
tcHsTypeApp wc_ty kind
| HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
- = do { ty <- solveLocalEqualities "tcHsTypeApp" $
+ = do { mode <- mkHoleMode TypeLevel HM_VTA
+ -- HM_VTA: See Note [Wildcards in visible type application]
+ ; ty <- addTypeCtxt hs_ty $
+ solveLocalEqualities "tcHsTypeApp" $
-- We are looking at a user-written type, very like a
-- signature so we want to solve its equalities right now
- unsetWOptM Opt_WarnPartialTypeSignatures $
- setXOptM LangExt.PartialTypeSignatures $
- -- See Note [Wildcards in visible type application]
tcNamedWildCardBinders sig_wcs $ \ _ ->
- tcCheckLHsType hs_ty (TheKind kind)
+ tc_lhs_type mode hs_ty kind
+
-- We do not kind-generalize type applications: we just
-- instantiate with exactly what the user says.
-- See Note [No generalization in type application]
@@ -448,6 +574,31 @@ There is also the possibility of mentioning a wildcard
-}
+tcFamTyPats :: TyCon
+ -> HsTyPats GhcRn -- Patterns
+ -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind)
+-- Check the LHS of a type/data family instance
+-- e.g. type instance F ty1 .. tyn = ...
+-- Used for both type and data families
+tcFamTyPats fam_tc hs_pats
+ = do { traceTc "tcFamTyPats {" $
+ vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
+
+ ; mode <- mkHoleMode TypeLevel HM_FamPat
+ -- HM_FamPat: See Note [Wildcards in family instances] in
+ -- GHC.Rename.Module
+ ; let fun_ty = mkTyConApp fam_tc []
+ ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty hs_pats
+
+ ; traceTc "End tcFamTyPats }" $
+ vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ]
+
+ ; return (fam_app, res_kind) }
+ where
+ fam_name = tyConName fam_tc
+ fam_arity = tyConArity fam_tc
+ lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name))
+
{-
************************************************************************
* *
@@ -465,38 +616,38 @@ tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty
tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty
tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind
- ; tc_lhs_type typeLevelMode ty ek }
-tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind
+ ; tcLHsType ty ek }
+tcHsLiftedTypeNC ty = tcLHsType ty liftedTypeKind
-- Like tcHsType, but takes an expected kind
tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType
tcCheckLHsType hs_ty exp_kind
= addTypeCtxt hs_ty $
do { ek <- newExpectedKind exp_kind
- ; tc_lhs_type typeLevelMode hs_ty ek }
+ ; tcLHsType hs_ty ek }
-tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
+tcInferLHsType :: LHsType GhcRn -> TcM TcType
-- Called from outside: set the context
-tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
-
--- Like tcLHsType, but use it in a context where type synonyms and type families
--- do not need to be saturated, like in a GHCi :kind call
-tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
-tcLHsTypeUnsaturated hs_ty
- | Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty)
+tcInferLHsType hs_ty
= addTypeCtxt hs_ty $
- do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
- ; tcInferApps_nosat mode hs_fun_ty fun_ty hs_args }
- -- Notice the 'nosat'; do not instantiate trailing
- -- invisible arguments of a type family.
- -- See Note [Dealing with :kind]
+ do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty
+ ; return ty }
- | otherwise
+-- Used to check the argument of GHCi :kind
+-- Allow and report wildcards, e.g. :kind T _
+-- Do not saturate family applications: see Note [Dealing with :kind]
+tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
+tcInferLHsTypeUnsaturated hs_ty
= addTypeCtxt hs_ty $
- tc_infer_lhs_type mode hs_ty
-
- where
- mode = typeLevelMode
+ do { mode <- mkHoleMode TypeLevel HM_Sig -- Allow and report holes
+ ; case splitHsAppTys (unLoc hs_ty) of
+ Just (hs_fun_ty, hs_args)
+ -> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
+ ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args }
+ -- Notice the 'nosat'; do not instantiate trailing
+ -- invisible arguments of a type family.
+ -- See Note [Dealing with :kind]
+ Nothing -> tc_infer_lhs_type mode hs_ty }
{- Note [Dealing with :kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -507,7 +658,7 @@ Consider this GHCi command
We will only get the 'forall' if we /refrain/ from saturating those
invisible binders. But generally we /do/ saturate those invisible
-binders (see tcInferApps), and we want to do so for nested application
+binders (see tcInferTyApps), and we want to do so for nested application
even in GHCi. Consider for example (#16287)
ghci> type family F :: k
ghci> data T :: (forall k. k) -> Type
@@ -515,7 +666,7 @@ even in GHCi. Consider for example (#16287)
We want to reject this. It's just at the very top level that we want
to switch off saturation.
-So tcLHsTypeUnsaturated does a little special case for top level
+So tcInferLHsTypeUnsaturated does a little special case for top level
applications. Actually the common case is a bare variable, as above.
@@ -538,21 +689,46 @@ concern things that the renamer can't handle.
-- grow, at least to include the distinction between patterns and
-- not-patterns.
--
--- To find out where the mode is used, search for 'mode_level'
-data TcTyMode = TcTyMode { mode_level :: TypeOrKind }
-
-typeLevelMode :: TcTyMode
-typeLevelMode = TcTyMode { mode_level = TypeLevel }
-
-kindLevelMode :: TcTyMode
-kindLevelMode = TcTyMode { mode_level = KindLevel }
+-- To find out where the mode is used, search for 'mode_tyki'
+--
+-- This data type is purely local, not exported from this module
+data TcTyMode
+ = TcTyMode { mode_tyki :: TypeOrKind
+
+ -- See Note [Levels for wildcards]
+ -- Nothing <=> no wildcards expected
+ , mode_holes :: Maybe (TcLevel, HoleMode)
+ }
+
+-- HoleMode says how to treat the occurrences
+-- of anonymous wildcards; see tcAnonWildCardOcc
+data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int
+ | HM_FamPat -- Family instances: F _ Int = Bool
+ | HM_VTA -- Visible type and kind application:
+ -- f @(Maybe _)
+ -- Maybe @(_ -> _)
+
+mkMode :: TypeOrKind -> TcTyMode
+mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }
+
+mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
+mkHoleMode tyki hm
+ = do { lvl <- getTcLevel
+ ; return (TcTyMode { mode_tyki = tyki
+ , mode_holes = Just (lvl,hm) }) }
--- switch to kind level
kindLevel :: TcTyMode -> TcTyMode
-kindLevel mode = mode { mode_level = KindLevel }
+kindLevel mode = mode { mode_tyki = KindLevel }
+
+instance Outputable HoleMode where
+ ppr HM_Sig = text "HM_Sig"
+ ppr HM_FamPat = text "HM_FamPat"
+ ppr HM_VTA = text "HM_VTA"
instance Outputable TcTyMode where
- ppr = ppr . mode_level
+ ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
+ = text "TcTyMode" <+> braces (sep [ ppr tyki <> comma
+ , ppr hm ])
{-
Note [Bidirectional type checking]
@@ -627,11 +803,12 @@ tc_infer_hs_type mode (HsParTy _ t)
tc_infer_hs_type mode ty
| Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
- = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
- ; tcInferApps mode hs_fun_ty fun_ty hs_args }
+ = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
+ ; tcInferTyApps mode hs_fun_ty fun_ty hs_args }
tc_infer_hs_type mode (HsKindSig _ ty sig)
- = do { sig' <- tcLHsKindSig KindSigCtxt sig
+ = do { let mode' = mode { mode_tyki = KindLevel }
+ ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig
-- We must typecheck the kind signature, and solve all
-- its equalities etc; from this point on we may do
-- things like instantiate its foralls, so it needs
@@ -665,6 +842,10 @@ tc_infer_hs_type mode other_ty
; return (ty', kv) }
------------------------------------------
+tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
+tcLHsType hs_ty exp_kind
+ = tc_lhs_type (mkMode TypeLevel) hs_ty exp_kind
+
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
tc_lhs_type mode (L span ty) exp_kind
= setSrcSpan span $
@@ -718,18 +899,25 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
, hst_body = ty }) exp_kind
= do { (tclvl, wanted, (inv_tv_bndrs, ty'))
- <- pushLevelAndCaptureConstraints $
- bindExplicitTKBndrs_Skol hs_tvs $
+ <- pushLevelAndCaptureConstraints $
+ bindExplicitTKBndrs_Skol_M mode hs_tvs $
+ -- The _M variant passes on the mode from the type, to
+ -- any wildards in kind signatures on the forall'd variables
+ -- e.g. f :: _ -> Int -> forall (a :: _). blah
tc_lhs_type mode ty exp_kind
- -- Do not kind-generalise here! See Note [Kind generalisation]
- -- Why exp_kind? See Note [Body kind of HsForAllTy]
- ; let skol_info = ForAllSkol (ppr forall)
- m_telescope = Just (sep (map ppr hs_tvs))
+ -- Why exp_kind? See Note [Body kind of HsForAllTy]
- ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs
+ -- Do not kind-generalise here! See Note [Kind generalisation]
- ; emitResidualTvConstraint skol_info m_telescope (binderVars tv_bndrs) tclvl wanted
+ ; let skol_info = ForAllSkol (ppr forall) (sep (map ppr hs_tvs))
+ skol_tvs = binderVars inv_tv_bndrs
+ ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted
+ ; emitImplication implic
+ -- /Always/ emit this implication even if wanted is empty
+ -- We need the implication so that we check for a bad telescope
+ -- See Note [Skolem escape and forall-types]
+ ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs
; return (mkForAllTys tv_bndrs ty') }
where
construct_bndr :: TcInvisTVBinder -> TcM TcTyVarBinder
@@ -846,7 +1034,7 @@ tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
--------- Constraint types
tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
- = do { MASSERT( isTypeLevel (mode_level mode) )
+ = do { MASSERT( isTypeLevel (mode_tyki mode) )
; ty' <- tc_lhs_type mode ty liftedTypeKind
; let n' = mkStrLitTy $ hsIPNameFS n
; ipClass <- tcLookupClass ipClassName
@@ -875,7 +1063,7 @@ tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type _ wc@(HsWildCardTy _) ek = tcAnonWildCardOcc wc ek
+tc_hs_type mode ty@(HsWildCardTy _) ek = tcAnonWildCardOcc mode ty ek
{-
Note [Variable Specificity and Forall Visibility]
@@ -903,7 +1091,7 @@ Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
------------------------------------------
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
-> TcM TcType
-tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
+tc_fun_type mode ty1 ty2 exp_kind = case mode_tyki mode of
TypeLevel ->
do { arg_k <- newOpenTypeKind
; res_k <- newOpenTypeKind
@@ -917,46 +1105,10 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2')
liftedTypeKind exp_kind }
----------------------------
-tcAnonWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
-tcAnonWildCardOcc wc exp_kind
- = do { wc_tv <- newWildTyVar -- The wildcard's kind will be an un-filled-in meta tyvar
-
- ; part_tysig <- xoptM LangExt.PartialTypeSignatures
- ; warning <- woptM Opt_WarnPartialTypeSignatures
-
- ; unless (part_tysig && not warning) $
- emitAnonTypeHole wc_tv
- -- Why the 'unless' guard?
- -- See Note [Wildcards in visible kind application]
-
- ; checkExpectedKind wc (mkTyVarTy wc_tv)
- (tyVarKind wc_tv) exp_kind }
-
-{- Note [Wildcards in visible kind application]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are cases where users might want to pass in a wildcard as a visible kind
-argument, for instance:
-
-data T :: forall k1 k2. k1 → k2 → Type where
- MkT :: T a b
-x :: T @_ @Nat False n
-x = MkT
-
-So we should allow '@_' without emitting any hole constraints, and
-regardless of whether PartialTypeSignatures is enabled or not. But how would
-the typechecker know which '_' is being used in VKA and which is not when it
-calls emitNamedTypeHole in tcHsPartialSigType on all HsWildCardBndrs?
-The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
-but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
-And whenever we see a '@', we automatically turn on PartialTypeSignatures and
-turn off hole constraint warnings, and do not call emitAnonTypeHole
-under these conditions.
-See related Note [Wildcards in visible type application] here and
-Note [The wildcard story for types] in GHC.Hs.Type
+{- Note [Skolem escape and forall-types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Checking telescopes].
-Note [Skolem escape and forall-types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> ()
@@ -970,11 +1122,19 @@ unification variable, because it would be untouchable inside
this inner implication.
That's what the pushLevelAndCaptureConstraints, plus subsequent
-emitResidualTvConstraint is all about, when kind-checking
+buildTvImplication/emitImplication is all about, when kind-checking
HsForAllTy.
-Note that we don't need to /simplify/ the constraints here
-because we aren't generalising. We just capture them.
+Note that
+
+* We don't need to /simplify/ the constraints here
+ because we aren't generalising. We just capture them.
+
+* We can't use emitResidualTvConstraint, because that has a fast-path
+ for empty constraints. We can't take that fast path here, because
+ we must do the bad-telescope check even if there are no inner wanted
+ constraints. See Note [Checking telescopes] in
+ GHC.Tc.Types.Constraint. Lacking this check led to #16247.
-}
{- *********************************************************************
@@ -1117,14 +1277,14 @@ splitHsAppTys hs_ty
go f as = (f, as)
---------------------------
-tcInferAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
+tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
-- Version of tc_infer_lhs_type specialised for the head of an
-- application. In particular, for a HsTyVar (which includes type
--- constructors, it does not zoom off into tcInferApps and family
+-- constructors, it does not zoom off into tcInferTyApps and family
-- saturation
-tcInferAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
+tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
= tcTyVar mode tv
-tcInferAppHead mode ty
+tcInferTyAppHead mode ty
= tc_infer_lhs_type mode ty
---------------------------
@@ -1135,24 +1295,24 @@ tcInferAppHead mode ty
-- These kinds should be used to instantiate invisible kind variables;
-- they come from an enclosing class for an associated type/data family.
--
--- tcInferApps also arranges to saturate any trailing invisible arguments
+-- tcInferTyApps also arranges to saturate any trailing invisible arguments
-- of a type-family application, which is usually the right thing to do
--- tcInferApps_nosat does not do this saturation; it is used only
+-- tcInferTyApps_nosat does not do this saturation; it is used only
-- by ":kind" in GHCi
-tcInferApps, tcInferApps_nosat
+tcInferTyApps, tcInferTyApps_nosat
:: TcTyMode
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function
-> [LHsTypeArg GhcRn] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
-tcInferApps mode hs_ty fun hs_args
- = do { (f_args, res_k) <- tcInferApps_nosat mode hs_ty fun hs_args
+tcInferTyApps mode hs_ty fun hs_args
+ = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args
; saturateFamApp f_args res_k }
-tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
- = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args)
+tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
+ = do { traceTc "tcInferTyApps {" (ppr orig_hs_ty $$ ppr orig_hs_args)
; (f_args, res_k) <- go_init 1 fun orig_hs_args
- ; traceTc "tcInferApps }" (ppr f_args <+> dcolon <+> ppr res_k)
+ ; traceTc "tcInferTyApps }" (ppr f_args <+> dcolon <+> ppr res_k)
; return (f_args, res_k) }
where
@@ -1205,21 +1365,18 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
Anon InvisArg _ -> instantiate ki_binder inner_ki
Named (Bndr _ Specified) -> -- Visible kind application
- do { traceTc "tcInferApps (vis kind app)"
+ do { traceTc "tcInferTyApps (vis kind app)"
(vcat [ ppr ki_binder, ppr hs_ki_arg
, ppr (tyBinderType ki_binder)
, ppr subst ])
; let exp_kind = substTy subst $ tyBinderType ki_binder
-
+ ; arg_mode <- mkHoleMode KindLevel HM_VTA
+ -- HM_VKA: see Note [Wildcards in visible kind application]
; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $
- unsetWOptM Opt_WarnPartialTypeSignatures $
- setXOptM LangExt.PartialTypeSignatures $
- -- Urgh! see Note [Wildcards in visible kind application]
- -- ToDo: must kill this ridiculous messing with DynFlags
- tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind
+ tc_lhs_type arg_mode hs_ki_arg exp_kind
- ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind)
+ ; traceTc "tcInferTyApps (vis kind app)" (ppr exp_kind)
; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
; go (n+1) fun' subst' inner_ki hs_args }
@@ -1241,7 +1398,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
-- "normal" case
| otherwise
- -> do { traceTc "tcInferApps (vis normal app)"
+ -> do { traceTc "tcInferTyApps (vis normal app)"
(vcat [ ppr ki_binder
, ppr arg
, ppr (tyBinderType ki_binder)
@@ -1249,7 +1406,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
; let exp_kind = substTy subst $ tyBinderType ki_binder
; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
tc_lhs_type mode arg exp_kind
- ; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind)
+ ; traceTc "tcInferTyApps (vis normal app) 2" (ppr exp_kind)
; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
; go (n+1) fun' subst' inner_ki args }
@@ -1263,7 +1420,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
-- This zonk is essential, to expose the fruits
-- of matchExpectedFunKind to the 'go' loop
- ; traceTc "tcInferApps (no binder)" $
+ ; traceTc "tcInferTyApps (no binder)" $
vcat [ ppr fun <+> dcolon <+> ppr fun_ki
, ppr arrows_needed
, ppr co
@@ -1272,7 +1429,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
-- Use go_init to establish go's INVARIANT
where
instantiate ki_binder inner_ki
- = do { traceTc "tcInferApps (need to instantiate)"
+ = do { traceTc "tcInferTyApps (need to instantiate)"
(vcat [ ppr ki_binder, ppr subst])
; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
; go n (mkAppTy fun arg') subst' inner_ki all_args }
@@ -1375,7 +1532,7 @@ The way in which tcTypeKind can crash is in applications
if 'a' is a type variable whose kind doesn't have enough arrows
or foralls. (The crash is in piResultTys.)
-The loop in tcInferApps has to be very careful to maintain the (PKTI).
+The loop in tcInferTyApps has to be very careful to maintain the (PKTI).
For example, suppose
kappa is a unification variable
We have already unified kappa := Type
@@ -1387,7 +1544,7 @@ If we call tcTypeKind on that, we'll crash, because the (un-zonked)
kind of 'a' is just kappa, not an arrow kind. So we must zonk first.
So the type inference engine is very careful when building applications.
-This happens in tcInferApps. Suppose we are kind-checking the type (a Int),
+This happens in tcInferTyApps. Suppose we are kind-checking the type (a Int),
where (a :: kappa). Then in tcInferApps we'll run out of binders on
a's kind, so we'll call matchExpectedFunKind, and unify
kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
@@ -1530,10 +1687,10 @@ tcHsMbContext Nothing = return []
tcHsMbContext (Just cxt) = tcHsContext cxt
tcHsContext :: LHsContext GhcRn -> TcM [PredType]
-tcHsContext = tc_hs_context typeLevelMode
+tcHsContext cxt = tc_hs_context (mkMode TypeLevel) cxt
tcLHsPredType :: LHsType GhcRn -> TcM PredType
-tcLHsPredType = tc_lhs_pred typeLevelMode
+tcLHsPredType pred = tc_lhs_pred (mkMode TypeLevel) pred
tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
@@ -1553,7 +1710,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
ATcTyCon tc_tc
-> do { -- See Note [GADT kind self-reference]
- unless (isTypeLevel (mode_level mode))
+ unless (isTypeLevel (mode_tyki mode))
(promotionErr name TyConPE)
; check_tc tc_tc
; return (mkTyConTy tc_tc, tyConKind tc_tc) }
@@ -1584,7 +1741,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
where
check_tc :: TyCon -> TcM ()
check_tc tc = do { data_kinds <- xoptM LangExt.DataKinds
- ; unless (isTypeLevel (mode_level mode) ||
+ ; unless (isTypeLevel (mode_tyki mode) ||
data_kinds ||
isKindTyCon tc) $
promotionErr name NoDataKindsTC }
@@ -1731,8 +1888,6 @@ in the e2 example, we'll desugar the type, zonking the kind unification
variables as we go. When we encounter the unconstrained kappa, we
want to default it to '*', not to (Any *).
-Help functions for type applications
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-}
addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a
@@ -1744,98 +1899,12 @@ addTypeCtxt (L _ ty) thing
where
doc = text "In the type" <+> quotes (ppr ty)
-{-
-************************************************************************
+
+{- *********************************************************************
* *
Type-variable binders
-%* *
-%************************************************************************
-
-Note [Keeping implicitly quantified variables in order]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When the user implicitly quantifies over variables (say, in a type
-signature), we need to come up with some ordering on these variables.
-This is done by bumping the TcLevel, bringing the tyvars into scope,
-and then type-checking the thing_inside. The constraints are all
-wrapped in an implication, which is then solved. Finally, we can
-zonk all the binders and then order them with scopedSort.
-
-It's critical to solve before zonking and ordering in order to uncover
-any unifications. You might worry that this eager solving could cause
-trouble elsewhere. I don't think it will. Because it will solve only
-in an increased TcLevel, it can't unify anything that was mentioned
-elsewhere. Additionally, we require that the order of implicitly
-quantified variables is manifest by the scope of these variables, so
-we're not going to learn more information later that will help order
-these variables.
-
-Note [Recipe for checking a signature]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Checking a user-written signature requires several steps:
-
- 1. Generate constraints.
- 2. Solve constraints.
- 3. Promote tyvars and/or kind-generalize.
- 4. Zonk.
- 5. Check validity.
-
-There may be some surprises in here:
-
-Step 2 is necessary for two reasons: most signatures also bring
-implicitly quantified variables into scope, and solving is necessary
-to get these in the right order (see Note [Keeping implicitly
-quantified variables in order]). Additionally, solving is necessary in
-order to kind-generalize correctly: otherwise, we do not know which
-metavariables are left unsolved.
-
-Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
-kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
-metatyvars generated in the type may have a bumped TcLevel, because explicit
-foralls raise the TcLevel. To avoid these variables from ever being visible in
-the surrounding context, we must obey the following dictum:
-
- Every metavariable in a type must either be
- (A) generalized, or
- (B) promoted, or See Note [Promotion in signatures]
- (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType
-
-The kindGeneralize functions do not require pre-zonking; they zonk as they
-go.
-
-If you are actually doing kind-generalization, you need to bump the level
-before generating constraints, as we will only generalize variables with
-a TcLevel higher than the ambient one.
-
-After promoting/generalizing, we need to zonk again because both
-promoting and generalizing fill in metavariables.
-
-Note [Promotion in signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If an unsolved metavariable in a signature is not generalized
-(because we're not generalizing the construct -- e.g., pattern
-sig -- or because the metavars are constrained -- see kindGeneralizeSome)
-we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables]
-in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing
-and the reinstantiating with a fresh metavariable at the current level.
-So in some sense, we generalize *all* variables, but then re-instantiate
-some of them.
-
-Here is an example of why we must promote:
- foo (x :: forall a. a -> Proxy b) = ...
-
-In the pattern signature, `b` is unbound, and will thus be brought into
-scope. We do not know its kind: it will be assigned kappa[2]. Note that
-kappa is at TcLevel 2, because it is invented under a forall. (A priori,
-the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel
-than the surrounding context.) This kappa cannot be solved for while checking
-the pattern signature (which is not kind-generalized). When we are checking
-the *body* of foo, though, we need to unify the type of x with the argument
-type of bar. At this point, the ambient TcLevel is 1, and spotting a
-matavariable with level 2 would violate the (WantedTvInv) invariant of
-Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing,
-we promote the metavariable to level 1. This is all done in kindGeneralizeNone.
-
--}
+* *
+********************************************************************* -}
tcNamedWildCardBinders :: [Name]
-> ([(Name, TcTyVar)] -> TcM a)
@@ -1844,22 +1913,119 @@ tcNamedWildCardBinders :: [Name]
-- plain wildcards _ are anonymous and dealt with by HsWildCardTy
-- Soe Note [The wildcard story for types] in GHC.Hs.Type
tcNamedWildCardBinders wc_names thing_inside
- = do { wcs <- mapM (const newWildTyVar) wc_names
+ = do { wcs <- mapM newNamedWildTyVar wc_names
; let wc_prs = wc_names `zip` wcs
; tcExtendNameTyVarEnv wc_prs $
thing_inside wc_prs }
-newWildTyVar :: TcM TcTyVar
+newNamedWildTyVar :: Name -> TcM TcTyVar
-- ^ New unification variable '_' for a wildcard
-newWildTyVar
+newNamedWildTyVar _name -- Currently ignoring the "_x" wildcard name used in the type
= do { kind <- newMetaKindVar
- ; uniq <- newUnique
; details <- newMetaDetails TauTv
- ; let name = mkSysTvName uniq (fsLit "_")
- tyvar = mkTcTyVar name kind details
+ ; wc_name <- newMetaTyVarName (fsLit "w") -- See Note [Wildcard names]
+ ; let tyvar = mkTcTyVar wc_name kind details
; traceTc "newWildTyVar" (ppr tyvar)
; return tyvar }
+---------------------------
+tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
+tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
+ ty exp_kind
+ -- hole_lvl: see Note [Checking partial type signatures]
+ -- esp the bullet on nested forall types
+ = do { kv_details <- newTauTvDetailsAtLevel hole_lvl
+ ; kv_name <- newMetaTyVarName (fsLit "k")
+ ; wc_details <- newTauTvDetailsAtLevel hole_lvl
+ ; wc_name <- newMetaTyVarName (fsLit wc_nm)
+ ; let kv = mkTcTyVar kv_name liftedTypeKind kv_details
+ wc_kind = mkTyVarTy kv
+ wc_tv = mkTcTyVar wc_name wc_kind wc_details
+
+ ; traceTc "tcAnonWildCardOcc" (ppr hole_lvl <+> ppr emit_holes)
+ ; when emit_holes $
+ emitAnonTypeHole wc_tv
+ -- Why the 'when' guard?
+ -- See Note [Wildcards in visible kind application]
+
+ -- You might think that this would always just unify
+ -- wc_kind with exp_kind, so we could avoid even creating kv
+ -- But the level numbers might not allow that unification,
+ -- so we have to do it properly (T14140a)
+ ; checkExpectedKind ty (mkTyVarTy wc_tv) wc_kind exp_kind }
+ where
+ -- See Note [Wildcard names]
+ wc_nm = case hole_mode of
+ HM_Sig -> "w"
+ HM_FamPat -> "_"
+ HM_VTA -> "w"
+
+ emit_holes = case hole_mode of
+ HM_Sig -> True
+ HM_FamPat -> False
+ HM_VTA -> False
+
+tcAnonWildCardOcc mode ty _
+-- mode_holes is Nothing. Should not happen, because renamer
+-- should already have rejected holes in unexpected places
+ = pprPanic "tcWildCardOcc" (ppr mode $$ ppr ty)
+
+{- Note [Wildcard names]
+~~~~~~~~~~~~~~~~~~~~~~~~
+So we hackily use the mode_holes flag to control the name used
+for wildcards:
+
+* For proper holes (whether in a visible type application (VTA) or no),
+ we rename the '_' to 'w'. This is so that we see variables like 'w0'
+ or 'w1' in error messages, a vast improvement upon '_0' and '_1'. For
+ example, we prefer
+ Found type wildcard ‘_’ standing for ‘w0’
+ over
+ Found type wildcard ‘_’ standing for ‘_1’
+
+ Even in the VTA case, where we do not emit an error to be printed, we
+ want to do the renaming, as the variables may appear in other,
+ non-wildcard error messages.
+
+* However, holes in the left-hand sides of type families ("type
+ patterns") stand for type variables which we do not care to name --
+ much like the use of an underscore in an ordinary term-level
+ pattern. When we spot these, we neither wish to generate an error
+ message nor to rename the variable. We don't rename the variable so
+ that we can pretty-print a type family LHS as, e.g.,
+ F _ Int _ = ...
+ and not
+ F w1 Int w2 = ...
+
+ See also Note [Wildcards in family instances] in
+ GHC.Rename.Module. The choice of HM_FamPat is made in
+ tcFamTyPats. There is also some unsavory magic, relying on that
+ underscore, in GHC.Core.Coercion.tidyCoAxBndrsForUser.
+
+Note [Wildcards in visible kind application]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are cases where users might want to pass in a wildcard as a visible kind
+argument, for instance:
+
+data T :: forall k1 k2. k1 → k2 → Type where
+ MkT :: T a b
+x :: T @_ @Nat False n
+x = MkT
+
+So we should allow '@_' without emitting any hole constraints, and
+regardless of whether PartialTypeSignatures is enabled or not. But how
+would the typechecker know which '_' is being used in VKA and which is
+not when it calls emitNamedTypeHole in
+tcHsPartialSigType on all HsWildCardBndrs? The solution is to neither
+rename nor include unnamed wildcards in HsWildCardBndrs, but instead
+give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
+
+And whenever we see a '@', we set mode_holes to HM_VKA, so that
+we do not call emitAnonTypeHole in tcAnonWildCardOcc.
+See related Note [Wildcards in visible type application] here and
+Note [The wildcard story for types] in GHC.Hs.Type
+-}
+
{- *********************************************************************
* *
Kind inference for type declarations
@@ -2703,8 +2869,17 @@ bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
-> TcM a
-> TcM ([VarBndr TyVar flag], a)
-bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar)
-bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar)
+bindExplicitTKBndrs_Skol_M, bindExplicitTKBndrs_Tv_M
+ :: (OutputableBndrFlag flag)
+ => TcTyMode
+ -> [LHsTyVarBndr flag GhcRn]
+ -> TcM a
+ -> TcM ([VarBndr TyVar flag], a)
+
+bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) newSkolemTyVar)
+bindExplicitTKBndrs_Skol_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) newSkolemTyVar)
+bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) cloneTyVarTyVar)
+bindExplicitTKBndrs_Tv_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) cloneTyVarTyVar)
-- newSkolemTyVar: see Note [Non-cloning for tyvar binders]
-- cloneTyVarTyVar: see Note [Cloning for tyvar binders]
@@ -2752,13 +2927,13 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
; return ((Bndr tv (hsTyVarBndrFlag hs_tv)):tvs, res) }
-----------------
-tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
+tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr flag GhcRn -> TcM TcTyVar
-tcHsTyVarBndr new_tv (UserTyVar _ _ (L _ tv_nm))
+tcHsTyVarBndr _ new_tv (UserTyVar _ _ (L _ tv_nm))
= do { kind <- newMetaKindVar
; new_tv tv_nm kind }
-tcHsTyVarBndr new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
- = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
+tcHsTyVarBndr mode new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind)
+ = do { kind <- tc_lhs_kind_sig mode (TyVarBndrKindCtxt tv_nm) lhs_kind
; new_tv tv_nm kind }
-----------------
@@ -2861,15 +3036,14 @@ kindGeneralizeSome should_gen kind_or_type
; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen)
- ; (_, promoted) <- promoteTyVarSet (dVarSetToVarSet to_promote)
+ ; _ <- promoteTyVarSet to_promote
; qkvs <- quantifyTyVars dvs'
; traceTc "kindGeneralizeSome }" $
vcat [ text "Kind or type:" <+> ppr kind_or_type
, text "dvs:" <+> ppr dvs
, text "dvs':" <+> ppr dvs'
- , text "to_promote:" <+> pprTyVars (dVarSetElems to_promote)
- , text "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted)
+ , text "to_promote:" <+> ppr to_promote
, text "qkvs:" <+> pprTyVars qkvs ]
; return qkvs }
@@ -3046,6 +3220,7 @@ data DataSort
checkDataKindSig :: DataSort -> Kind -> TcM ()
checkDataKindSig data_sort kind = do
dflags <- getDynFlags
+ traceTc "checkDataKindSig" (ppr kind)
checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags)
where
pp_dec :: SDoc
@@ -3211,19 +3386,20 @@ tcHsPartialSigType ctxt sig_ty
, hsib_body = hs_ty } <- ib_ty
, (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTyInvis hs_ty
= addSigCtxt ctxt hs_ty $
- do { (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau)))
+ do { mode <- mkHoleMode TypeLevel HM_Sig
+ ; (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau)))
<- solveLocalEqualities "tcHsPartialSigType" $
- -- This solveLocalEqualiltes fails fast if there are
- -- insoluble equalities. See GHC.Tc.Solver
- -- Note [Fail fast if there are insoluble kind equalities]
+ -- See Note [Failure in local type signatures]
tcNamedWildCardBinders sig_wcs $ \ wcs ->
- bindImplicitTKBndrs_Tv implicit_hs_tvs $
- bindExplicitTKBndrs_Tv explicit_hs_tvs $
+ bindImplicitTKBndrs_Tv implicit_hs_tvs $
+ bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $
do { -- Instantiate the type-class context; but if there
-- is an extra-constraints wildcard, just discard it here
- (theta, wcx) <- tcPartialContext hs_ctxt
+ (theta, wcx) <- tcPartialContext mode hs_ctxt
- ; tau <- tcHsOpenType hs_tau
+ ; ek <- newOpenTypeKind
+ ; tau <- addTypeCtxt hs_tau $
+ tc_lhs_type mode hs_tau ek
; return (wcs, wcx, theta, tau) }
@@ -3241,10 +3417,12 @@ tcHsPartialSigType ctxt sig_ty
; mapM_ emitNamedTypeHole wcs
-- Zonk, so that any nested foralls can "see" their occurrences
- -- See Note [Checking partial type signatures], in
- -- the bullet on Nested foralls.
- ; theta <- mapM zonkTcType theta
- ; tau <- zonkTcType tau
+ -- See Note [Checking partial type signatures], and in particular
+ -- Note [Levels for wildcards]
+ ; implicit_tvbndrs <- mapM zonkInvisTVBinder implicit_tvbndrs
+ ; explicit_tvbndrs <- mapM zonkInvisTVBinder explicit_tvbndrs
+ ; theta <- mapM zonkTcType theta
+ ; tau <- zonkTcType tau
-- We return a proper (Name,InvisTVBinder) environment, to be sure that
-- we bring the right name into scope in the function body.
@@ -3259,16 +3437,16 @@ tcHsPartialSigType ctxt sig_ty
; traceTc "tcHsPartialSigType" (ppr tv_prs)
; return (wcs, wcx, tv_prs, theta, tau) }
-tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
-tcPartialContext hs_theta
+tcPartialContext :: TcTyMode -> HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
+tcPartialContext mode hs_theta
| Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
- , L wc_loc wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
+ , L wc_loc ty@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
= do { wc_tv_ty <- setSrcSpan wc_loc $
- tcAnonWildCardOcc wc constraintKind
- ; theta <- mapM tcLHsPredType hs_theta1
+ tcAnonWildCardOcc mode ty constraintKind
+ ; theta <- mapM (tc_lhs_pred mode) hs_theta1
; return (theta, Just wc_tv_ty) }
| otherwise
- = do { theta <- mapM tcLHsPredType hs_theta
+ = do { theta <- mapM (tc_lhs_pred mode) hs_theta
; return (theta, Nothing) }
{- Note [Checking partial type signatures]
@@ -3312,29 +3490,48 @@ we do the following
g x = True
It's really as if we'd written two distinct signatures.
-* Nested foralls. Consider
- f :: forall b. (forall a. a -> _) -> b
- We do /not/ allow the "_" to be instantiated to 'a'; but we do
- (as before) allow it to be instantiated to the (top level) 'b'.
- Why not? Because suppose
- f x = (x True, x 'c')
- We must instantiate that (forall a. a -> _) when typechecking
- f's body, so we must know precisely where all the a's are; they
- must not be hidden under (filled-in) unification variables!
-
- We achieve this in the usual way: we push a level at a forall,
- so now the unification variable for the "_" can't unify with
- 'a'.
-
-* Just as for ordinary signatures, we must zonk the type after
- kind-checking it, to ensure that all the nested forall binders can
- see their occurrenceds
+* Nested foralls. See Note [Levels for wildcards]
+
+* Just as for ordinary signatures, we must solve local equalities and
+ zonk the type after kind-checking it, to ensure that all the nested
+ forall binders can "see" their occurrenceds
Just as for ordinary signatures, this zonk also gets any Refl casts
out of the way of instantiation. Example: #18008 had
foo :: (forall a. (Show a => blah) |> Refl) -> _
and that Refl cast messed things up. See #18062.
+Note [Levels for wildcards]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ f :: forall b. (forall a. a -> _) -> b
+We do /not/ allow the "_" to be instantiated to 'a'; although we do
+(as before) allow it to be instantiated to the (top level) 'b'.
+Why not? Suppose
+ f x = (x True, x 'c')
+
+During typecking the RHS we must instantiate that (forall a. a -> _),
+so we must know /precisely/ where all the a's are; they must not be
+hidden under (possibly-not-yet-filled-in) unification variables!
+
+We achieve this as follows:
+
+- For /named/ wildcards such sas
+ g :: forall b. (forall la. a -> _x) -> b
+ there is no problem: we create them at the outer level (ie the
+ ambient level of teh signature itself), and push the level when we
+ go inside a forall. So now the unification variable for the "_x"
+ can't unify with skolem 'a'.
+
+- For /anonymous/ wildcards, such as 'f' above, we carry the ambient
+ level of the signature to the hole in the TcLevel part of the
+ mode_holes field of TcTyMode. Then, in tcAnonWildCardOcc we us that
+ level (and /not/ the level ambient at the occurrence of "_") to
+ create the unification variable for the wildcard. That is the sole
+ purpose of the TcLevel in the mode_holes field: to transport the
+ ambient level of the signature down to the anonymous wildcard
+ occurrences.
+
Note [Extra-constraint holes in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
@@ -3399,14 +3596,16 @@ tcHsPatSigType ctxt
, hsps_body = hs_ty })
= addSigCtxt ctxt hs_ty $
do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
+ ; mode <- mkHoleMode TypeLevel HM_Sig
; (wcs, sig_ty)
- <- solveLocalEqualities "tcHsPatSigType" $
- -- Always solve local equalities if possible,
- -- else casts get in the way of deep skolemisation
- -- (#16033)
+ <- addTypeCtxt hs_ty $
+ solveLocalEqualities "tcHsPatSigType" $
+ -- See Note [Failure in local type signatures]
+ -- and c.f #16033
tcNamedWildCardBinders sig_wcs $ \ wcs ->
tcExtendNameTyVarEnv sig_tkv_prs $
- do { sig_ty <- tcHsOpenType hs_ty
+ do { ek <- newOpenTypeKind
+ ; sig_ty <- tc_lhs_type mode hs_ty ek
; return (wcs, sig_ty) }
; mapM_ emitNamedTypeHole wcs
@@ -3509,10 +3708,15 @@ It does sort checking and desugaring at the same time, in one single pass.
tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig ctxt hs_kind
+ = tc_lhs_kind_sig (mkMode KindLevel) ctxt hs_kind
+
+tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
+tc_lhs_kind_sig mode ctxt hs_kind
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
-- Result is zonked
- = do { kind <- solveLocalEqualities "tcLHsKindSig" $
- tc_lhs_kind kindLevelMode hs_kind
+ = do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $
+ solveLocalEqualities "tcLHsKindSig" $
+ tc_lhs_type mode hs_kind liftedTypeKind
; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
-- No generalization:
; kindGeneralizeNone kind
@@ -3528,11 +3732,6 @@ tcLHsKindSig ctxt hs_kind
; traceTc "tcLHsKindSig2" (ppr kind)
; return kind }
-tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind
-tc_lhs_kind mode k
- = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $
- tc_lhs_type (kindLevel mode) k liftedTypeKind
-
promotionErr :: Name -> PromotionErr -> TcM a
promotionErr name err
= failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here")
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index 350be10236..b9eaad4adb 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -36,9 +36,10 @@ where
import GHC.Prelude
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRhoNC, tcInferRho
- , tcCheckId, tcLExpr, tcLExprNC, tcExpr
- , tcCheckExpr )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC
+ , tcMonoExpr, tcMonoExprNC, tcExpr
+ , tcCheckMonoExpr, tcCheckMonoExprNC
+ , tcCheckPolyExpr, tcCheckId )
import GHC.Types.Basic (LexicalFixity(..))
import GHC.Hs
@@ -79,17 +80,11 @@ import Control.Arrow ( second )
@FunMonoBind@. The second argument is the name of the function, which
is used in error messages. It checks that all the equations have the
same number of arguments before using @tcMatches@ to do the work.
-
-Note [Polymorphic expected type for tcMatchesFun]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-tcMatchesFun may be given a *sigma* (polymorphic) type
-so it must be prepared to use tcSkolemise to skolemise it.
-See Note [sig_tau may be polymorphic] in GHC.Tc.Gen.Pat.
-}
tcMatchesFun :: Located Name
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> ExpSigmaType -- Expected type of function
+ -> ExpRhoType -- Expected type of function
-> TcM (HsWrapper, MatchGroup GhcTcId (LHsExpr GhcTcId))
-- Returns type of body
tcMatchesFun fn@(L _ fun_name) matches exp_ty
@@ -102,20 +97,17 @@ tcMatchesFun fn@(L _ fun_name) matches exp_ty
traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty)
; checkArgs fun_name matches
- ; (wrap_gen, (wrap_fun, group))
- <- tcSkolemiseET (FunSigCtxt fun_name True) exp_ty $ \ exp_rho ->
- -- Note [Polymorphic expected type for tcMatchesFun]
- do { (matches', wrap_fun)
- <- matchExpectedFunTys herald arity exp_rho $
- \ pat_tys rhs_ty ->
- tcMatches match_ctxt pat_tys rhs_ty matches
- ; return (wrap_fun, matches') }
- ; return (wrap_gen <.> wrap_fun, group) }
+ ; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
+ -- NB: exp_type may be polymorphic, but
+ -- matchExpectedFunTys can cope with that
+ tcMatches match_ctxt pat_tys rhs_ty matches }
where
- arity = matchGroupArity matches
+ arity = matchGroupArity matches
herald = text "The equation(s) for"
<+> quotes (ppr fun_name) <+> text "have"
- what = FunRhs { mc_fun = fn, mc_fixity = Prefix, mc_strictness = strictness }
+ ctxt = GenSigCtxt -- Was: FunSigCtxt fun_name True
+ -- But that's wrong for f :: Int -> forall a. blah
+ what = FunRhs { mc_fun = fn, mc_fixity = Prefix, mc_strictness = strictness }
match_ctxt = MC { mc_what = what, mc_body = tcBody }
strictness
| [L _ match] <- unLoc $ mg_alts matches
@@ -144,10 +136,10 @@ tcMatchesCase ctxt scrut_ty matches res_ty
tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
-> TcMatchCtxt HsExpr
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> ExpRhoType -- deeply skolemised
- -> TcM (MatchGroup GhcTcId (LHsExpr GhcTcId), HsWrapper)
+ -> ExpRhoType
+ -> TcM (HsWrapper, MatchGroup GhcTcId (LHsExpr GhcTcId))
tcMatchLambda herald match_ctxt match res_ty
- = matchExpectedFunTys herald n_pats res_ty $ \ pat_tys rhs_ty ->
+ = matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty ->
tcMatches match_ctxt pat_tys rhs_ty match
where
n_pats | isEmptyMatchGroup match = 1 -- must be lambda-case
@@ -332,7 +324,7 @@ tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt)
tcBody :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId)
tcBody body res_ty
= do { traceTc "tcBody" (ppr res_ty)
- ; tcLExpr body res_ty
+ ; tcMonoExpr body res_ty
}
{-
@@ -412,7 +404,7 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside
tcGuardStmt :: TcExprStmtChecker
tcGuardStmt _ (BodyStmt _ guard _ _) res_ty thing_inside
- = do { guard' <- tcLExpr guard (mkCheckExpType boolTy)
+ = do { guard' <- tcCheckMonoExpr guard boolTy
; thing <- thing_inside res_ty
; return (BodyStmt boolTy guard' noSyntaxExpr noSyntaxExpr, thing) }
@@ -445,21 +437,21 @@ tcLcStmt :: TyCon -- The list type constructor ([])
-> TcExprStmtChecker
tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside
- = do { body' <- tcLExprNC body elt_ty
+ = do { body' <- tcMonoExprNC body elt_ty
; thing <- thing_inside (panic "tcLcStmt: thing_inside")
; return (LastStmt x body' noret noSyntaxExpr, thing) }
-- A generator, pat <- rhs
tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside
= do { pat_ty <- newFlexiTyVarTy liftedTypeKind
- ; rhs' <- tcLExpr rhs (mkCheckExpType $ mkTyConApp m_tc [pat_ty])
+ ; rhs' <- tcCheckMonoExpr rhs (mkTyConApp m_tc [pat_ty])
; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
thing_inside elt_ty
; return (mkTcBindStmt pat' rhs', thing) }
-- A boolean guard
tcLcStmt _ _ (BodyStmt _ rhs _ _) elt_ty thing_inside
- = do { rhs' <- tcLExpr rhs (mkCheckExpType boolTy)
+ = do { rhs' <- tcCheckMonoExpr rhs boolTy
; thing <- thing_inside elt_ty
; return (BodyStmt boolTy rhs' noSyntaxExpr noSyntaxExpr, thing) }
@@ -517,7 +509,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts
by_arrow $
poly_arg_ty `mkVisFunTy` poly_res_ty
- ; using' <- tcCheckExpr using using_poly_ty
+ ; using' <- tcCheckPolyExpr using using_poly_ty
; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
-- 'stmts' returns a result of type (m1_ty tuple_ty),
@@ -559,7 +551,7 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside
= do { (body', return_op')
<- tcSyntaxOp MCompOrigin return_op [SynRho] res_ty $
\ [a_ty] ->
- tcLExprNC body (mkCheckExpType a_ty)
+ tcCheckMonoExprNC body a_ty
; thing <- thing_inside (panic "tcMcStmt: thing_inside")
; return (LastStmt x body' noret return_op', thing) }
@@ -575,7 +567,7 @@ tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside
<- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn)
[SynRho, SynFun SynAny SynRho] res_ty $
\ [rhs_ty, pat_ty, new_res_ty] ->
- do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty)
+ do { rhs' <- tcCheckMonoExprNC rhs rhs_ty
; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
thing_inside (mkCheckExpType new_res_ty)
; return (rhs', pat', thing, new_res_ty) }
@@ -607,7 +599,7 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside
<- tcSyntaxOp MCompOrigin guard_op [SynAny]
(mkCheckExpType rhs_ty) $
\ [test_ty] ->
- tcLExpr rhs (mkCheckExpType test_ty)
+ tcCheckMonoExpr rhs test_ty
; thing <- thing_inside (mkCheckExpType new_res_ty)
; return (thing, rhs', rhs_ty, guard_op') }
; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) }
@@ -667,8 +659,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
(mkCheckExpType using_arg_ty) $ \res_ty' -> do
{ by' <- case by of
Nothing -> return Nothing
- Just e -> do { e' <- tcLExpr e
- (mkCheckExpType by_e_ty)
+ Just e -> do { e' <- tcCheckMonoExpr e by_e_ty
; return (Just e') }
-- Find the Ids (and hence types) of all old binders
@@ -693,7 +684,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
--------------- Typecheck the 'fmap' function -------------
; fmap_op' <- case form of
ThenForm -> return noExpr
- _ -> fmap unLoc . tcCheckExpr (noLoc fmap_op) $
+ _ -> fmap unLoc . tcCheckPolyExpr (noLoc fmap_op) $
mkInfForAllTy alphaTyVar $
mkInfForAllTy betaTyVar $
(alphaTy `mkVisFunTy` betaTy)
@@ -703,7 +694,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap
--------------- Typecheck the 'using' function -------------
-- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c))
- ; using' <- tcCheckExpr using using_poly_ty
+ ; using' <- tcCheckPolyExpr using using_poly_ty
; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using'
--------------- Building the bindersMap ----------------
@@ -765,7 +756,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside
(m_ty `mkAppTy` betaTy)
`mkVisFunTy`
(m_ty `mkAppTy` mkBoxedTupleTy [alphaTy, betaTy])
- ; mzip_op' <- unLoc `fmap` tcCheckExpr (noLoc mzip_op) mzip_ty
+ ; mzip_op' <- unLoc `fmap` tcCheckPolyExpr (noLoc mzip_op) mzip_ty
-- type dummies since we don't know all binder types yet
; id_tys_s <- (mapM . mapM) (const (newFlexiTyVarTy liftedTypeKind))
@@ -827,7 +818,7 @@ tcMcStmt _ stmt _ _
tcDoStmt :: TcExprStmtChecker
tcDoStmt _ (LastStmt x body noret _) res_ty thing_inside
- = do { body' <- tcLExprNC body res_ty
+ = do { body' <- tcMonoExprNC body res_ty
; thing <- thing_inside (panic "tcDoStmt: thing_inside")
; return (LastStmt x body' noret noSyntaxExpr, thing) }
@@ -840,7 +831,7 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside
((rhs', pat', new_res_ty, thing), bind_op')
<- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $
\ [rhs_ty, pat_ty, new_res_ty] ->
- do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty)
+ do { rhs' <- tcCheckMonoExprNC rhs rhs_ty
; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
thing_inside (mkCheckExpType new_res_ty)
; return (rhs', pat', new_res_ty, thing) }
@@ -873,7 +864,7 @@ tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside
; ((rhs', rhs_ty, thing), then_op')
<- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $
\ [rhs_ty, new_res_ty] ->
- do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty)
+ do { rhs' <- tcCheckMonoExprNC rhs rhs_ty
; thing <- thing_inside (mkCheckExpType new_res_ty)
; return (rhs', rhs_ty, thing) }
; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) }
@@ -1043,7 +1034,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside
}, pat_ty, exp_ty)
= setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $
addErrCtxt (pprStmtInCtxt ctxt (mkRnBindStmt pat rhs)) $
- do { rhs' <- tcLExprNC rhs (mkCheckExpType exp_ty)
+ do { rhs' <- tcCheckMonoExprNC rhs exp_ty
; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $
return ()
; fail_op' <- fmap join . forM fail_op $ \fail ->
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 58f64f84ae..4e30d4bc33 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -30,7 +30,7 @@ where
import GHC.Prelude
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho )
import GHC.Hs
import GHC.Tc.Utils.Zonk
@@ -397,43 +397,51 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
res) }
ViewPat _ expr pat -> do
- {
- -- We use tcInferRho here.
- -- If we have a view function with types like:
- -- blah -> forall b. burble
- -- then simple-subsumption means that 'forall b' won't be instantiated
- -- so we can typecheck the inner pattern with that type
- -- An exotic example:
- -- pair :: forall a. a -> forall b. b -> (a,b)
- -- f (pair True -> x) = ...here (x :: forall b. b -> (Bool,b))
- --
- -- TEMPORARY: pending simple subsumption, use tcInferSigma
- -- When removing this, remove it from Expr.hs-boot too
- ; (expr',expr_ty) <- tcInferSigma expr
+ { (expr',expr_ty) <- tcInferRho expr
+ -- Note [View patterns and polymorphism]
-- Expression must be a function
; let expr_orig = lexprCtOrigin expr
herald = text "A view pattern expression expects"
- ; (expr_wrap1, [inf_arg_ty], inf_res_ty)
- <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr_ty
- -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_ty)
+ ; (expr_wrap1, inf_arg_ty, inf_res_sigma)
+ <- matchActualFunTySigma herald expr_orig (Just (unLoc expr)) (1,[]) expr_ty
+ -- See Note [View patterns and polymorphism]
+ -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
-- Check that overall pattern is more polymorphic than arg type
; expr_wrap2 <- tc_sub_type penv pat_ty inf_arg_ty
-- expr_wrap2 :: pat_ty "->" inf_arg_ty
- -- Pattern must have inf_res_ty
- ; (pat', res) <- tc_lpat (mkCheckExpType inf_res_ty) penv pat thing_inside
+ -- Pattern must have inf_res_sigma
+ ; (pat', res) <- tc_lpat (mkCheckExpType inf_res_sigma) penv pat thing_inside
; pat_ty <- readExpType pat_ty
; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper
- pat_ty inf_res_ty doc
- -- expr_wrap2' :: (inf_arg_ty -> inf_res_ty) "->"
- -- (pat_ty -> inf_res_ty)
+ pat_ty inf_res_sigma doc
+ -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->"
+ -- (pat_ty -> inf_res_sigma)
expr_wrap = expr_wrap2' <.> expr_wrap1
doc = text "When checking the view pattern function:" <+> (ppr expr)
; return (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res)}
+{- Note [View patterns and polymorphism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this exotic example:
+ pair :: forall a. Bool -> a -> forall b. b -> (a,b)
+
+ f :: Int -> blah
+ f (pair True -> x) = ...here (x :: forall b. b -> (Int,b))
+
+The expresion (pair True) should have type
+ pair True :: Int -> forall b. b -> (Int,b)
+so that it is ready to consume the incoming Int. It should be an
+arrow type (t1 -> t2); hence using (tcInferRho expr).
+
+Then, when taking that arrow apart we want to get a *sigma* type
+(forall b. b->(Int,b)), because that's what we want to bind 'x' to.
+Fortunately that's what matchExpectedFunTySigma returns anyway.
+-}
+
-- Type signatures in patterns
-- See Note [Pattern coercions] below
SigPat _ pat sig_ty -> do
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index c788f15437..63377c74d5 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -199,7 +199,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs
do { -- See Note [Solve order for RULES]
((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
; (rhs', rhs_wanted) <- captureConstraints $
- tcLExpr rhs (mkCheckExpType rule_ty)
+ tcCheckMonoExpr rhs rule_ty
; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted
; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } }
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index fb313d9297..2ac2823fb5 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -635,6 +635,7 @@ to connect the two, something like
This wrapper is put in the TcSpecPrag, in the ABExport record of
the AbsBinds.
+
f :: (Eq a, Ix b) => a -> b -> Bool
{-# SPECIALISE f :: (Ix p, Ix q) => Int -> (p,q) -> Bool #-}
f = <poly_rhs>
@@ -674,12 +675,13 @@ delicate, but works.
Some wrinkles
-1. We don't use full-on tcSubType, because that does co and contra
- variance and that in turn will generate too complex a LHS for the
- RULE. So we use a single invocation of skolemise /
- topInstantiate in tcSpecWrapper. (Actually I think that even
- the "deeply" stuff may be too much, because it introduces lambdas,
- though I think it can be made to work without too much trouble.)
+1. In tcSpecWrapper, rather than calling tcSubType, we directly call
+ skolemise/instantiate. That is mainly because of wrinkle (2).
+
+ Historical note: in the past, tcSubType did co/contra stuff, which
+ could generate too complex a LHS for the RULE, which was another
+ reason for not using tcSubType. But that reason has gone away
+ with simple subsumption (#17775).
2. We need to take care with type families (#5821). Consider
type instance F Int = Bool
@@ -775,7 +777,7 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
-- See Note [Handling SPECIALISE pragmas], wrinkle 1
tcSpecWrapper ctxt poly_ty spec_ty
= do { (sk_wrap, inst_wrap)
- <- tcSkolemise ctxt spec_ty $ \ _ spec_tau ->
+ <- tcSkolemise ctxt spec_ty $ \ spec_tau ->
do { (inst_wrap, tau) <- topInstantiate orig poly_ty
; _ <- unifyType Nothing spec_tau tau
-- Deliberately ignore the evidence
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index 8a7b1b0c7f..f1233c55ed 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -288,7 +288,7 @@ tcPendingSplice m_var (PendingRnSplice flavour splice_name expr)
= do { meta_ty <- tcMetaTy meta_ty_name
-- Expected type of splice, e.g. m Exp
; let expected_type = mkAppTy m_var meta_ty
- ; expr' <- tcCheckExpr expr expected_type
+ ; expr' <- tcCheckPolyExpr expr expected_type
; return (PendingTcSplice splice_name expr') }
where
meta_ty_name = case flavour of
@@ -618,7 +618,7 @@ tcNestedSplice pop_stage (TcPending ps_var lie_var q@(QuoteWrapper _ m_var)) spl
; meta_exp_ty <- tcTExpTy m_var res_ty
; expr' <- setStage pop_stage $
setConstraintVar lie_var $
- tcLExpr expr (mkCheckExpType meta_exp_ty)
+ tcCheckMonoExpr expr meta_exp_ty
; untypeq <- tcLookupId unTypeQName
; let expr'' = mkHsApp
(mkLHsWrap (applyQuoteWrapper q)
@@ -647,7 +647,7 @@ tcTopSplice expr res_ty
-- Top level splices must still be of type Q (TExp a)
; meta_exp_ty <- tcTExpTy q_type res_ty
; q_expr <- tcTopSpliceExpr Typed $
- tcLExpr expr (mkCheckExpType meta_exp_ty)
+ tcCheckMonoExpr expr meta_exp_ty
; lcl_env <- getLclEnv
; let delayed_splice
= DelayedSplice lcl_env expr res_ty q_expr
@@ -684,7 +684,7 @@ runTopSplice (DelayedSplice lcl_env orig_expr res_ty q_expr)
captureConstraints $
addErrCtxt (spliceResultDoc zonked_q_expr) $ do
{ (exp3, _fvs) <- rnLExpr expr2
- ; tcLExpr exp3 (mkCheckExpType zonked_ty)}
+ ; tcCheckMonoExpr exp3 zonked_ty }
; ev <- simplifyTop wcs
; return $ unLoc (mkHsDictLet (EvBinds ev) res)
}
@@ -717,7 +717,7 @@ tcTopSpliceExpr :: SpliceType -> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc)
-- Note that set the level to Splice, regardless of the original level,
-- before typechecking the expression. For example:
-- f x = $( ...$(g 3) ... )
--- The recursive call to tcCheckExpr will simply expand the
+-- The recursive call to tcCheckPolyExpr will simply expand the
-- inner escape before dealing with the outer one
tcTopSpliceExpr isTypedSplice tc_action
@@ -1438,7 +1438,7 @@ reifyInstances th_nm th_tys
<- pushTcLevelM_ $
solveEqualities $ -- Avoid error cascade if there are unsolved
bindImplicitTKBndrs_Skol tv_names $
- fst <$> tcLHsType rn_ty
+ tcInferLHsType rn_ty
; ty <- zonkTcTypeToType ty
-- Substitute out the meta type variables
-- In particular, the type might have kind
View Lorry Controller Status