diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-02-02 18:23:11 +0000 |
|---|---|---|
| committer | Ben Gamari <ben@smart-cactus.org> | 2020-06-05 09:27:50 -0400 |
| commit | 2b792facab46f7cdd09d12e79499f4e0dcd4293f (patch) | |
| tree | f3bf2dffdd3c46744d3c1b0638948a1dfbd1b8f6 /compiler/GHC/Tc/Gen | |
| parent | af5e3a885ddd09dd5f550552c535af3661ff3dbf (diff) | |
| download | haskell-2b792facab46f7cdd09d12e79499f4e0dcd4293f.tar.gz | |
Simple subsumptionwip/T17775
This patch simplifies GHC to use simple subsumption.
Ticket #17775
Implements GHC proposal #287
https://github.com/ghc-proposals/ghc-proposals/blob/master/
proposals/0287-simplify-subsumption.rst
All the motivation is described there; I will not repeat it here.
The implementation payload:
* tcSubType and friends become noticably simpler, because it no
longer uses eta-expansion when checking subsumption.
* No deeplyInstantiate or deeplySkolemise
That in turn means that some tests fail, by design; they can all
be fixed by eta expansion. There is a list of such changes below.
Implementing the patch led me into a variety of sticky corners, so
the patch includes several othe changes, some quite significant:
* I made String wired-in, so that
"foo" :: String rather than
"foo" :: [Char]
This improves error messages, and fixes #15679
* The pattern match checker relies on knowing about in-scope equality
constraints, andd adds them to the desugarer's environment using
addTyCsDs. But the co_fn in a FunBind was missed, and for some reason
simple-subsumption ends up with dictionaries there. So I added a
call to addTyCsDs. This is really part of #18049.
* I moved the ic_telescope field out of Implication and into
ForAllSkol instead. This is a nice win; just expresses the code
much better.
* There was a bug in GHC.Tc.TyCl.Instance.tcDataFamInstHeader.
We called checkDataKindSig inside tc_kind_sig, /before/
solveEqualities and zonking. Obviously wrong, easily fixed.
* solveLocalEqualitiesX: there was a whole mess in here, around
failing fast enough. I discovered a bad latent bug where we
could successfully kind-check a type signature, and use it,
but have unsolved constraints that could fill in coercion
holes in that signature -- aargh.
It's all explained in Note [Failure in local type signatures]
in GHC.Tc.Solver. Much better now.
* I fixed a serious bug in anonymous type holes. IN
f :: Int -> (forall a. a -> _) -> Int
that "_" should be a unification variable at the /outer/
level; it cannot be instantiated to 'a'. This was plain
wrong. New fields mode_lvl and mode_holes in TcTyMode,
and auxiliary data type GHC.Tc.Gen.HsType.HoleMode.
This fixes #16292, but makes no progress towards the more
ambitious #16082
* I got sucked into an enormous refactoring of the reporting of
equality errors in GHC.Tc.Errors, especially in
mkEqErr1
mkTyVarEqErr
misMatchMsg
misMatchMsgOrCND
In particular, the very tricky mkExpectedActualMsg function
is gone.
It took me a full day. But the result is far easier to understand.
(Still not easy!) This led to various minor improvements in error
output, and an enormous number of test-case error wibbles.
One particular point: for occurs-check errors I now just say
Can't match 'a' against '[a]'
rather than using the intimidating language of "occurs check".
* Pretty-printing AbsBinds
Tests review
* Eta expansions
T11305: one eta expansion
T12082: one eta expansion (undefined)
T13585a: one eta expansion
T3102: one eta expansion
T3692: two eta expansions (tricky)
T2239: two eta expansions
T16473: one eta
determ004: two eta expansions (undefined)
annfail06: two eta (undefined)
T17923: four eta expansions (a strange program indeed!)
tcrun035: one eta expansion
* Ambiguity check at higher rank. Now that we have simple
subsumption, a type like
f :: (forall a. Eq a => Int) -> Int
is no longer ambiguous, because we could write
g :: (forall a. Eq a => Int) -> Int
g = f
and it'd typecheck just fine. But f's type is a bit
suspicious, and we might want to consider making the
ambiguity check do a check on each sub-term. Meanwhile,
these tests are accepted, whereas they were previously
rejected as ambiguous:
T7220a
T15438
T10503
T9222
* Some more interesting error message wibbles
T13381: Fine: one error (Int ~ Exp Int)
rather than two (Int ~ Exp Int, Exp Int ~ Int)
T9834: Small change in error (improvement)
T10619: Improved
T2414: Small change, due to order of unification, fine
T2534: A very simple case in which a change of unification order
means we get tow unsolved constraints instead of one
tc211: bizarre impredicative tests; just accept this for now
Updates Cabal and haddock submodules.
Metric Increase:
T12150
T12234
T5837
haddock.base
Metric Decrease:
haddock.compiler
haddock.Cabal
haddock.base
Merge note: This appears to break the
`UnliftedNewtypesDifficultUnification` test. It has been marked as
broken in the interest of merging.
(cherry picked from commit 66b7b195cb3dce93ed5078b80bf568efae904cc5)
Diffstat (limited to 'compiler/GHC/Tc/Gen')
| -rw-r--r-- | compiler/GHC/Tc/Gen/Arrow.hs | 15 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Bind.hs | 148 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Default.hs | 4 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Expr.hs | 288 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Expr.hs-boot | 30 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Foreign.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/HsType.hs | 831 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Match.hs | 75 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Pat.hs | 52 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Rule.hs | 2 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Sig.hs | 16 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Gen/Splice.hs | 12 |
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 |