diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 5a259b6a80b19e95c3760c709a5d47309309f991..5e74682fdfb8f29e1ae7226b64ff365cbb1e7533 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -77,7 +77,7 @@ module GHC.Core.Type (
mkCastTy, mkCoercionTy, splitCastTy_maybe,
ErrorMsgType,
- userTypeError_maybe, pprUserTypeErrorTy,
+ userTypeError_maybe, deepUserTypeError_maybe, pprUserTypeErrorTy,
coAxNthLHS,
stripCoercionTy,
@@ -290,8 +290,7 @@ import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Data.FastString
-import Control.Monad ( guard )
-import GHC.Data.Maybe ( orElse, isJust )
+import GHC.Data.Maybe ( orElse, isJust, firstJust )
-- $type_classification
-- #type_classification#
@@ -1236,13 +1235,41 @@ type ErrorMsgType = Type
-- | Is this type a custom user error?
-- If so, give us the error message.
userTypeError_maybe :: Type -> Maybe ErrorMsgType
-userTypeError_maybe t
- = do { (tc, _kind : msg : _) <- splitTyConApp_maybe t
+userTypeError_maybe ty
+ | Just ty' <- coreView ty = userTypeError_maybe ty'
+userTypeError_maybe (TyConApp tc (_kind : msg : _))
+ | tyConName tc == errorMessageTypeErrorFamName
-- There may be more than 2 arguments, if the type error is
-- used as a type constructor (e.g. at kind `Type -> Type`).
+ = Just msg
+userTypeError_maybe _
+ = Nothing
+
+deepUserTypeError_maybe :: Type -> Maybe ErrorMsgType
+-- Look for custom user error, deeply inside the type
+deepUserTypeError_maybe ty
+ | Just ty' <- coreView ty = userTypeError_maybe ty'
+deepUserTypeError_maybe (TyConApp tc tys)
+ | tyConName tc == errorMessageTypeErrorFamName
+ , _kind : msg : _ <- tys
+ -- There may be more than 2 arguments, if the type error is
+ -- used as a type constructor (e.g. at kind `Type -> Type`).
+ = Just msg
- ; guard (tyConName tc == errorMessageTypeErrorFamName)
- ; return msg }
+ | tyConMustBeSaturated tc -- Don't go looking for user type errors
+ -- inside type family arguments (see #20241).
+ = foldr (firstJust . deepUserTypeError_maybe) Nothing (drop (tyConArity tc) tys)
+ | otherwise
+ = foldr (firstJust . deepUserTypeError_maybe) Nothing tys
+deepUserTypeError_maybe (ForAllTy _ ty) = deepUserTypeError_maybe ty
+deepUserTypeError_maybe (FunTy { ft_arg = arg, ft_res = res })
+ = deepUserTypeError_maybe arg `firstJust` deepUserTypeError_maybe res
+deepUserTypeError_maybe (AppTy t1 t2)
+ = deepUserTypeError_maybe t1 `firstJust` deepUserTypeError_maybe t2
+deepUserTypeError_maybe (CastTy ty _)
+ = deepUserTypeError_maybe ty
+deepUserTypeError_maybe _ -- TyVarTy, CoercionTy, LitTy
+ = Nothing
-- | Render a type corresponding to a user type error into a SDoc.
pprUserTypeErrorTy :: ErrorMsgType -> SDoc
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 0d1539922796b3ccb9710eaeff4999dd4995abe1..e4ec0325ecde2fdfa3646f309659a1a5e22e2ba4 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -5006,9 +5006,9 @@ tidySigSkol env cx ty tv_prs
where
(env', tv') = tidy_tv_bndr env tv
- tidy_ty env ty@(FunTy af w arg res) -- Look under c => t
- | isInvisibleFunArg af
- = ty { ft_mult = tidy_ty env w
+ tidy_ty env ty@(FunTy { ft_mult = w, ft_arg = arg, ft_res = res })
+ = -- Look under c => t and t1 -> t2
+ ty { ft_mult = tidy_ty env w
, ft_arg = tidyType env arg
, ft_res = tidy_ty env res }
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 7387cd7275caf805de5f7ff3281b123e3801138f..ee6c2fe599d0b51ebe8593b55a146401d044e263 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -642,8 +642,10 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- Rule ITVDQ from the GHC Proposal #281
go1 delta acc so_far fun_ty ((EValArg { eva_arg = ValArg arg }) : rest_args)
| Just (tvb, body) <- tcSplitForAllTyVarBinder_maybe fun_ty
- , binderFlag tvb == Required
- = do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
+ = assertPpr (binderFlag tvb == Required) (ppr fun_ty $$ ppr arg) $
+ -- Any invisible binders have been instantiated by IALL above,
+ -- so this forall must be visible (i.e. Required)
+ do { (ty_arg, inst_body) <- tcVDQ fun_conc_tvs (tvb, body) arg
; let wrap = mkWpTyApps [ty_arg]
; go delta (addArgWrap wrap acc) so_far inst_body rest_args }
@@ -731,7 +733,8 @@ tcInstFun do_ql inst_final (tc_fun, fun_ctxt) fun_sigma rn_args
-- taking apart the arrow type (a -> Int).
matchActualFunTy herald
(Just $ HsExprTcThing tc_fun)
- (n_val_args, so_far) fun_ty
+ (n_val_args, fun_sigma) fun_ty
+
; (delta', arg') <- if do_ql
then addArgCtxt ctxt arg $
-- Context needed for constraints
diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs
index 9de6772ca67ff7477d0763dd8f8e9b3af8393155..868cd86edf5c35c3ffebb0ff67547c5de5451f76 100644
--- a/compiler/GHC/Tc/Gen/Arrow.hs
+++ b/compiler/GHC/Tc/Gen/Arrow.hs
@@ -263,8 +263,8 @@ tc_cmd env cmd@(HsCmdLam x lam_variant match) cmd_ty
LamSingle -> id -- Avoids clutter in the vanilla-lambda form
_ -> addErrCtxt (cmdCtxt cmd)) $
do { let match_ctxt = ArrowLamAlt lam_variant
- ; checkArgCounts (Just (ArrowMatchCtxt match_ctxt)) match
- ; (wrap, match') <- tcCmdMatchLambda env match_ctxt match cmd_ty
+ ; arity <- checkArgCounts match
+ ; (wrap, match') <- tcCmdMatchLambda env match_ctxt arity match cmd_ty
; return (mkHsCmdWrap wrap (HsCmdLam x lam_variant match')) }
-------------------------------------------
@@ -327,14 +327,14 @@ tcCmdMatches env scrut_ty matches (stk, res_ty)
-- | Typechecking for 'HsCmdLam' and 'HsCmdLamCase'.
tcCmdMatchLambda :: CmdEnv
-> HsArrowMatchContext
+ -> Arity
-> MatchGroup GhcRn (LHsCmd GhcRn)
-> CmdType
-> TcM (HsWrapper, MatchGroup GhcTc (LHsCmd GhcTc))
-tcCmdMatchLambda env
- ctxt
+tcCmdMatchLambda env ctxt arity
mg@MG { mg_alts = L l matches, mg_ext = origin }
(cmd_stk, res_ty)
- = do { (co, arg_tys, cmd_stk') <- matchExpectedCmdArgs n_pats cmd_stk
+ = do { (co, arg_tys, cmd_stk') <- matchExpectedCmdArgs arity cmd_stk
; let check_arg_tys = map (unrestricted . mkCheckExpType) arg_tys
; matches' <- forM matches $
@@ -346,9 +346,6 @@ tcCmdMatchLambda env
; return (mkWpCastN co, mg') }
where
- n_pats | isEmptyMatchGroup mg = 1 -- must be lambda-case
- | otherwise = matchGroupArity mg
-
-- Check the patterns, and the GRHSs inside
tc_match arg_tys cmd_stk' (L mtch_loc (Match { m_pats = pats, m_grhss = grhss }))
= do { (pats', grhss') <- setSrcSpanA mtch_loc $
@@ -371,7 +368,7 @@ tcCmdMatchLambda env
tc_grhs stk_ty res_ty (GRHS x guards body)
= do { (guards', rhs') <- tcStmtsAndThen pg_ctxt tcGuardStmt guards res_ty $
\ res_ty -> tcCmd env body
- (stk_ty, checkingExpType "tc_grhs" res_ty)
+ (stk_ty, checkingExpType res_ty)
; return (GRHS x guards' rhs') }
matchExpectedCmdArgs :: Arity -> TcType -> TcM (TcCoercionN, [TcTypeFRR], TcType)
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs
index f6bf57bbf6f3169c598dde3884b4ddc8df73a842..68f1edfbd1e38f47922d5ec86fb4cb7d6f12b056 100644
--- a/compiler/GHC/Tc/Gen/Bind.hs
+++ b/compiler/GHC/Tc/Gen/Bind.hs
@@ -622,29 +622,29 @@ tcPolyCheck :: TcPragEnv
-- it is a FunBind
-- it has a complete type signature,
tcPolyCheck prag_fn
- (CSig { sig_bndr = poly_id, sig_ctxt = ctxt, sig_loc = sig_loc })
+ sig@(CSig { sig_bndr = poly_id, sig_ctxt = ctxt })
(L bind_loc (FunBind { fun_id = L nm_loc name
, fun_matches = matches }))
- = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
+ = do { traceTc "tcPolyCheck" (ppr sig)
+ -- Make a new Name, whose SrcSpan is nm_loc. For a ClassOp
+ -- The original Name, in the FunBind{fun_id}, is bound in the
+ -- class declaration, whereas we want a Name bound right here.
+ -- We pass mono_name to tcFunBindMatches which in turn puts it in
+ -- the BinderStack, whence it shows up in "Relevant bindings.."
; mono_name <- newNameAt (nameOccName name) (locA nm_loc)
+
; mult <- tcMultAnn (HsNoMultAnn noExtField)
; (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: tcSkolemiseScoped makes fresh type variables
- -- See Note [Instantiate sig with fresh variables]
+ <- tcSkolemiseCompleteSig sig $ \invis_pat_tys rho_ty ->
let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
-- Why mono_id in the BinderStack?
-- See Note [Relevant bindings and the binder stack]
- setSrcSpanA bind_loc $
- tcFunBindMatches (L nm_loc (idName mono_id)) mult matches
- (mkCheckExpType rho_ty)
+ setSrcSpanA bind_loc $
+ tcFunBindMatches ctxt mono_name mult matches invis_pat_tys (mkCheckExpType rho_ty)
-- We make a funny AbsBinds, abstracting over nothing,
-- just so we have somewhere to put the SpecPrags.
@@ -1373,7 +1373,7 @@ tcMonoBinds is_rec sig_fn no_gen
-- function so that in type error messages we show the
-- type of the thing whose rhs we are type checking.
-- See Note [Relevant bindings and the binder stack]
- tcFunBindMatches (L nm_loc name) mult matches exp_ty
+ tcFunBindMatches (InfSigCtxt name) name mult matches [] exp_ty
; mono_id <- newLetBndr no_gen name mult rhs_ty'
; return (unitBag $ L b_loc $
@@ -1648,9 +1648,11 @@ tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
loc mult matches)
= tcExtendIdBinderStackForRhs [info] $
tcExtendTyVarEnvForRhs mb_sig $
- do { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
- ; (co_fn, matches') <- tcFunBindMatches (L (noAnnSrcSpan loc) (idName mono_id)) mult
- matches (mkCheckExpType $ idType mono_id)
+ do { let mono_ty = idType mono_id
+ mono_name = idName mono_id
+ ; traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr mono_ty)
+ ; (co_fn, matches') <- tcFunBindMatches (InfSigCtxt mono_name) mono_name mult
+ matches [] (mkCheckExpType mono_ty)
; return ( FunBind { fun_id = L (noAnnSrcSpan loc) mono_id
, fun_matches = matches'
, fun_ext = (co_fn, [])
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index b8c7fd49635feaa338176e057d5cd74de268cd50..d944d9e72fbd1d9cc1706f45f813ad5d3fc47981 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -20,7 +20,7 @@ module GHC.Tc.Gen.Expr
tcCheckMonoExpr, tcCheckMonoExprNC,
tcMonoExpr, tcMonoExprNC,
tcInferRho, tcInferRhoNC,
- tcPolyExpr, tcExpr,
+ tcPolyLExpr, tcPolyExpr, tcExpr, tcPolyLExprSig,
tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
tcCheckId,
) where
@@ -56,7 +56,8 @@ import GHC.Core.FamInstEnv ( FamInstEnvs )
import GHC.Rename.Env ( addUsedGRE, getUpdFieldLbls )
import GHC.Tc.Utils.Env
import GHC.Tc.Gen.Arrow
-import GHC.Tc.Gen.Match
+import GHC.Tc.Gen.Match( tcBody, tcLambdaMatches, tcCaseMatches
+ , tcGRHSList, tcDoStmts )
import GHC.Tc.Gen.HsType
import GHC.Tc.Utils.TcMType
import GHC.Tc.Zonk.TcType
@@ -98,7 +99,6 @@ import qualified Data.List.NonEmpty as NE
************************************************************************
-}
-
tcCheckPolyExpr, tcCheckPolyExprNC
:: LHsExpr GhcRn -- Expression to type check
-> TcSigmaType -- Expected type (could be a polytype)
@@ -112,6 +112,7 @@ tcCheckPolyExpr, tcCheckPolyExprNC
tcCheckPolyExpr expr res_ty = tcPolyLExpr expr (mkCheckExpType res_ty)
tcCheckPolyExprNC expr res_ty = tcPolyLExprNC expr (mkCheckExpType res_ty)
+-----------------
-- These versions take an ExpType
tcPolyLExpr, tcPolyLExprNC :: LHsExpr GhcRn -> ExpSigmaType
-> TcM (LHsExpr GhcTc)
@@ -127,6 +128,112 @@ tcPolyLExprNC (L loc expr) res_ty
do { expr' <- tcPolyExpr expr res_ty
; return (L loc expr') }
+-----------------
+tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
+tcPolyExpr e (Infer inf) = tcExpr e (Infer inf)
+tcPolyExpr e (Check ty) = tcPolyExprCheck e (Left ty)
+
+-----------------
+tcPolyLExprSig :: LHsExpr GhcRn -> TcCompleteSig -> TcM (LHsExpr GhcTc)
+tcPolyLExprSig (L loc expr) sig
+ = setSrcSpanA loc $
+ -- No addExprCtxt. For (e :: ty) we don't want generate
+ -- In the expression e
+ -- In the expression e :: ty
+ -- We have already got an error-context for (e::ty), so when we
+ -- get to `e`, just add the location
+ do { traceTc "tcPolyLExprSig" (ppr loc $$ ppr expr)
+ ; expr' <- tcPolyExprCheck expr (Right sig)
+ ; return (L loc expr') }
+
+-----------------
+tcPolyExprCheck :: HsExpr GhcRn
+ -> Either TcSigmaType TcCompleteSig
+ -> TcM (HsExpr GhcTc)
+-- tcPolyExpCheck deals with the special case for HsLam, in case the pushed-down
+-- type is a forall-type. E.g. (\@a -> blah) :: forall b. b -> Int
+--
+-- The (Either TcSigmaType TcCompleteSig) deals with:
+-- Left ty: (f e) pushes f's argument type `ty` into `e`
+-- Right sig: (e :: sig) pushes `sig` into `e`
+-- The Either stuff is entirely local to this function and its immediate callers.
+--
+-- See Note [Skolemisation overview] in GHC.Tc.Utils.Unify
+
+tcPolyExprCheck expr res_ty
+ = outer_skolemise res_ty $ \pat_tys rho_ty ->
+ let
+ -- tc_body is a little loop that looks past parentheses
+ tc_body (HsPar x (L loc e))
+ = setSrcSpanA loc $
+ do { e' <- tc_body e
+ ; return (HsPar x (L loc e')) }
+
+ -- The special case for lambda: go to tcLambdaMatches, passing pat_tys
+ tc_body e@(HsLam x lam_variant matches)
+ = do { (wrap, matches') <- tcLambdaMatches e lam_variant matches pat_tys
+ (mkCheckExpType rho_ty)
+ -- NB: tcLambdaMatches concludes with deep skolemisation,
+ -- if DeepSubsumption is on; hence no need to do that here
+ ; return (mkHsWrap wrap $ HsLam x lam_variant matches') }
+
+ -- The general case: just do deep skolemisation if necessary,
+ -- before handing off to tcExpr
+ tc_body e = do { ds_flag <- getDeepSubsumptionFlag
+ ; inner_skolemise ds_flag rho_ty $ \rho_ty' ->
+ tcExpr e (mkCheckExpType rho_ty') }
+ in tc_body expr
+ where
+ -- `outer_skolemise` is used always
+ -- It only does shallow skolemisation
+ -- It always makes an implication constraint if deferred-errors is on
+ outer_skolemise :: Either TcSigmaType TcCompleteSig
+ -> ([ExpPatType] -> TcRhoType -> TcM (HsExpr GhcTc))
+ -> TcM (HsExpr GhcTc)
+ outer_skolemise (Left ty) thing_inside
+ = do { (wrap, expr') <- tcSkolemiseExpectedType ty thing_inside
+ ; return (mkHsWrap wrap expr') }
+ outer_skolemise (Right sig) thing_inside
+ = do { (wrap, expr') <- tcSkolemiseCompleteSig sig thing_inside
+ ; return (mkHsWrap wrap expr') }
+
+ -- inner_skolemise is used when we do not have a lambda
+ -- With deep skolemisation we must remember to deeply skolemise
+ -- after the (always-shallow) tcSkolemiseCompleteSig
+ inner_skolemise :: DeepSubsumptionFlag -> TcRhoType
+ -> (TcRhoType -> TcM (HsExpr GhcTc)) -> TcM (HsExpr GhcTc)
+ inner_skolemise Shallow rho_ty thing_inside
+ = -- We have already done shallow skolemisation, so nothing further to do
+ thing_inside rho_ty
+ inner_skolemise Deep rho_ty thing_inside
+ = -- Try deep skolemisation
+ do { (wrap, expr') <- tcSkolemise Deep ctxt rho_ty thing_inside
+ ; return (mkHsWrap wrap expr') }
+
+ ctxt = case res_ty of
+ Left {} -> GenSigCtxt
+ Right sig -> sig_ctxt sig
+
+
+{- *********************************************************************
+* *
+ tcExpr: the main expression typechecker
+* *
+********************************************************************* -}
+
+tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
+-- Infer a *rho*-type. The return type is always instantiated.
+tcInferRho (L loc expr)
+ = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad
+ addExprCtxt expr $ -- Note [Error contexts in generated code]
+ do { (expr', rho) <- tcInfer (tcExpr expr)
+ ; return (L loc expr', rho) }
+
+tcInferRhoNC (L loc expr)
+ = setSrcSpanA loc $
+ do { (expr', rho) <- tcInfer (tcExpr expr)
+ ; return (L loc expr', rho) }
+
---------------
tcCheckMonoExpr, tcCheckMonoExprNC
:: LHsExpr GhcRn -- Expression to type check
@@ -136,6 +243,7 @@ tcCheckMonoExpr, tcCheckMonoExprNC
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
@@ -154,33 +262,6 @@ tcMonoExprNC (L loc 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 (L loc expr)
- = setSrcSpanA loc $ -- Set location /first/; see GHC.Tc.Utils.Monad
- addExprCtxt expr $ -- Note [Error contexts in generated code]
- do { (expr', rho) <- tcInfer (tcExpr expr)
- ; return (L loc expr', rho) }
-
-tcInferRhoNC (L loc expr)
- = setSrcSpanA loc $
- do { (expr', rho) <- tcInfer (tcExpr expr)
- ; return (L loc expr', rho) }
-
-
-{- *********************************************************************
-* *
- tcExpr: the main expression typechecker
-* *
-********************************************************************* -}
-
-tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
-tcPolyExpr expr res_ty
- = do { traceTc "tcPolyExpr" (ppr res_ty)
- ; (wrap, expr') <- tcSkolemiseExpType GenSigCtxt res_ty $ \ res_ty ->
- tcExpr expr res_ty
- ; return $ mkHsWrap wrap expr' }
-
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-- Use tcApp to typecheck applications, which are treated specially
@@ -262,11 +343,8 @@ tcExpr e@(HsIPVar _ x) res_ty
origin = IPOccOrigin x
tcExpr e@(HsLam x lam_variant matches) res_ty
- = do { (wrap, matches') <- tcLambdaMatches herald matches res_ty
+ = do { (wrap, matches') <- tcLambdaMatches e lam_variant matches [] res_ty
; return (mkHsWrap wrap $ HsLam x lam_variant matches') }
- where
- herald = ExpectedFunTyLam lam_variant e
-
{-
************************************************************************
@@ -408,10 +486,9 @@ Not using 'sup' caused #23814.
-}
tcExpr (HsMultiIf _ alts) res_ty
- = do { (ues, alts') <- mapAndUnzipM (\alt -> tcCollectingUsage $
- wrapLocMA (tcGRHS IfAlt tcBody res_ty) alt) alts
+ = do { alts' <- tcGRHSList IfAlt tcBody alts res_ty
+ -- See Note [MultiWayIf linearity checking]
; res_ty <- readExpType res_ty
- ; tcEmitBindingUsage (supUEs ues) -- See Note [MultiWayIf linearity checking]
; return (HsMultiIf res_ty alts') }
tcExpr (HsDo _ do_or_lc stmts) res_ty
@@ -825,8 +902,8 @@ tcSynArgE :: CtOrigin
-- ^ returns a wrapper :: (type of right shape) "->" (type passed in)
tcSynArgE orig op sigma_ty syn_ty thing_inside
= do { (skol_wrap, (result, ty_wrapper))
- <- tcTopSkolemise GenSigCtxt sigma_ty
- (\ rho_ty -> go rho_ty syn_ty)
+ <- tcSkolemise Shallow GenSigCtxt sigma_ty $ \rho_ty ->
+ go rho_ty syn_ty
; return (result, skol_wrap <.> ty_wrapper) }
where
go rho_ty SynAny
@@ -895,8 +972,7 @@ tcSynArgA :: CtOrigin
-- and a wrapper to be applied to the overall expression
tcSynArgA orig op sigma_ty arg_shapes res_shape thing_inside
= do { (match_wrapper, arg_tys, res_ty)
- <- matchActualFunTys herald orig Nothing
- (length arg_shapes) sigma_ty
+ <- matchActualFunTys herald orig (length arg_shapes) sigma_ty
-- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty)
; ((result, res_wrapper), arg_wrappers)
<- tc_syn_args_e (map scaledThing arg_tys) arg_shapes $ \ arg_results arg_res_mults ->
diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot
index 6850e8aed207d754ee60eb6b6e645540ed24fd4f..bb94df58dccafd43c439b576e0d212a0cc17ae8b 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs-boot
+++ b/compiler/GHC/Tc/Gen/Expr.hs-boot
@@ -5,6 +5,7 @@ import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, TcSigmaTypeFRR
, SyntaxOpType
, ExpType, ExpRhoType, ExpSigmaType )
import GHC.Tc.Types ( TcM )
+import GHC.Tc.Types.BasicTypes( TcCompleteSig )
import GHC.Tc.Types.Origin ( CtOrigin )
import GHC.Core.Type ( Mult )
import GHC.Hs.Extension ( GhcRn, GhcTc )
@@ -23,6 +24,9 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
-> TcRhoType
-> TcM (LHsExpr GhcTc)
+tcPolyLExpr :: LHsExpr GhcRn -> ExpSigmaType -> TcM (LHsExpr GhcTc)
+tcPolyLExprSig :: LHsExpr GhcRn -> TcCompleteSig -> TcM (LHsExpr GhcTc)
+
tcPolyExpr :: HsExpr GhcRn -> ExpSigmaType -> TcM (HsExpr GhcTc)
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
@@ -42,4 +46,3 @@ tcSyntaxOpGen :: CtOrigin
-> SyntaxOpType
-> ([TcSigmaTypeFRR] -> [Mult] -> TcM a)
-> TcM (a, SyntaxExprTc)
-
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index e5d7d7a4c996bbc5076419cc6cb734af96e74042..88ec0ae7a75c29a9099667b08e841f3bd32c3fa8 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -23,14 +23,13 @@ module GHC.Tc.Gen.Head
, leadingValArgs, isVisibleArg, pprHsExprArgTc
, tcInferAppHead, tcInferAppHead_maybe
- , tcInferId, tcCheckId
- , obviousSig
+ , tcInferId, tcCheckId, obviousSig
, tyConOf, tyConOfET, fieldNotInType
, nonBidirectionalErr
, addHeadCtxt, addExprCtxt, addStmtCtxt, addFunResCtxt ) where
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckMonoExprNC, tcCheckPolyExprNC )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckPolyExprNC, tcPolyLExprSig )
import GHC.Prelude
import GHC.Hs
@@ -40,7 +39,7 @@ import GHC.Tc.Gen.HsType
import GHC.Rename.Unbound ( unknownNameSuggestions, WhatLooking(..) )
import GHC.Tc.Gen.Bind( chooseInferredQuantifiers )
-import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig, lhsSigWcTypeContextSpan )
+import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig )
import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Unify
@@ -82,7 +81,7 @@ import GHC.Driver.Env
import GHC.Driver.DynFlags
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
-import GHC.Utils.Panic.Plain
+import GHC.Utils.Panic
import qualified GHC.LanguageExtensions as LangExt
import GHC.Data.Maybe
@@ -997,21 +996,17 @@ tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
tcExprWithSig expr hs_ty
= do { sig_info <- checkNoErrs $ -- Avoid error cascade
tcUserTypeSig loc hs_ty Nothing
- ; (expr', poly_ty) <- tcExprSig ctxt expr sig_info
+ ; (expr', poly_ty) <- tcExprSig expr sig_info
; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
where
loc = getLocA (dropWildCards hs_ty)
- ctxt = ExprSigCtxt (lhsSigWcTypeContextSpan hs_ty)
-tcExprSig :: UserTypeCtxt -> LHsExpr GhcRn -> TcIdSig -> TcM (LHsExpr GhcTc, TcSigmaType)
-tcExprSig ctxt expr (TcCompleteSig (CSig { sig_bndr = poly_id, sig_loc = loc }))
- = setSrcSpan loc $ -- Sets the location for the implication constraint
- do { let poly_ty = idType poly_id
- ; (wrap, expr') <- tcSkolemiseScoped ctxt poly_ty $ \rho_ty ->
- tcCheckMonoExprNC expr rho_ty
- ; return (mkLHsWrap wrap expr', poly_ty) }
+tcExprSig :: LHsExpr GhcRn -> TcIdSig -> TcM (LHsExpr GhcTc, TcSigmaType)
+tcExprSig expr (TcCompleteSig sig)
+ = do { expr' <- tcPolyLExprSig expr sig
+ ; return (expr', idType (sig_bndr sig)) }
-tcExprSig _ expr sig@(TcPartialSig (PSig { psig_name = name, psig_loc = loc }))
+tcExprSig expr sig@(TcPartialSig (PSig { psig_name = name, psig_loc = loc }))
= setSrcSpan loc $ -- Sets the location for the implication constraint
do { (tclvl, wanted, (expr', sig_inst))
<- pushLevelAndCaptureConstraints $
@@ -1102,8 +1097,7 @@ tcInferOverLit lit@(OverLit { ol_val = val
thing = NameThing from_name
mb_thing = Just thing
herald = ExpectedFunTyArg thing (HsLit noAnn hs_lit)
- ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing
- (1, []) from_ty
+ ; (wrap2, sarg_ty, res_ty) <- matchActualFunTy herald mb_thing (1, from_ty) from_ty
; co <- unifyType mb_thing (hsLitType hs_lit) (scaledThing sarg_ty)
-- See Note [Source locations for implicit function calls] in GHC.Iface.Ext.Ast
diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs
index c45200d1321e99e68ae2b3cdf26f42082279646d..576d27d1a36e1d70792fbc51e19e42c8c1b997bb 100644
--- a/compiler/GHC/Tc/Gen/Match.hs
+++ b/compiler/GHC/Tc/Gen/Match.hs
@@ -1,10 +1,10 @@
-
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@@ -17,11 +17,10 @@
-- | Typecheck some @Matches@
module GHC.Tc.Gen.Match
( tcFunBindMatches
- , tcGRHS
- , tcGRHSsPat
, tcCaseMatches
, tcLambdaMatches
- , TcMatchAltChecker
+ , tcGRHSList
+ , tcGRHSsPat
, TcStmtChecker
, TcExprStmtChecker
, TcCmdStmtChecker
@@ -38,9 +37,9 @@ where
import GHC.Prelude
import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC
- , tcMonoExpr, tcMonoExprNC, tcExpr
+ , tcMonoExprNC, tcExpr
, tcCheckMonoExpr, tcCheckMonoExprNC
- , tcCheckPolyExpr )
+ , tcCheckPolyExpr, tcPolyLExpr )
import GHC.Rename.Utils ( bindLocalNames, isIrrefutableHsPat )
import GHC.Tc.Errors.Types
@@ -73,11 +72,10 @@ import GHC.Utils.Panic
import GHC.Utils.Misc
import GHC.Driver.DynFlags ( getDynFlags )
-import GHC.Types.Fixity (LexicalFixity(..))
import GHC.Types.Name
import GHC.Types.Id
import GHC.Types.SrcLoc
-import GHC.Types.Basic
+import GHC.Types.Basic( Arity, isDoExpansionGenerated )
import Control.Monad
import Control.Arrow ( second )
@@ -95,47 +93,73 @@ import qualified GHC.LanguageExtensions as LangExt
************************************************************************
`tcFunBindMatches` typechecks a `[Match]` list which occurs in a
-`FunMonoBind`. The second argument is the name of the function, which
+`FunBind`. 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.
-}
-tcFunBindMatches :: LocatedN Name -- MatchContext Id
- -> Mult -- The multiplicity of the binder
+tcFunBindMatches :: UserTypeCtxt
+ -> Name -- Function name
+ -> Mult -- The multiplicity of the binder
-> MatchGroup GhcRn (LHsExpr GhcRn)
- -> ExpRhoType -- Expected type of function
+ -> [ExpPatType] -- Scoped skolemised binders
+ -> ExpRhoType -- Expected type of function; caller
+ -- has skolemised any outer forall's
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
- -- Returns type of body
-tcFunBindMatches fun_name mult matches exp_ty
- = do { -- Check that they all have the same no of arguments
- -- Location is in the monad, set the caller so that
- -- any inter-equation error messages get some vaguely
- -- sensible location. Note: we have to do this odd
- -- ann-grabbing, because we don't always have annotations in
- -- hand when we call tcFunBindMatches...
- traceTc "tcFunBindMatches" (ppr fun_name $$ ppr mult $$ ppr exp_ty $$ ppr arity)
- ; checkArgCounts (Just what) matches
-
- ; (wrapper, (mult_co_wrap, r)) <- matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
- -- NB: exp_type may be polymorphic, but
- -- matchExpectedFunTys can cope with that
- tcScalingUsage mult $
- -- Makes sure that if the binding is unrestricted, it counts as
- -- consuming its rhs Many times.
- tcMatches tcBody pat_tys rhs_ty matches
+-- See Note [Skolemisation overview] in GHC.Tc.Utils.Unify
+tcFunBindMatches ctxt fun_name mult matches invis_pat_tys exp_ty
+ = assertPpr (funBindPrecondition matches) (pprMatches matches) $
+ do { -- Check that they all have the same no of arguments
+ arity <- checkArgCounts matches
+
+ ; traceTc "tcFunBindMatches 1" (ppr fun_name $$ ppr mult $$ ppr exp_ty $$ ppr arity)
+
+ ; (wrap_fun, (wrap_mult, r))
+ <- matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty ->
+ tcScalingUsage mult $
+ -- Makes sure that if the binding is unrestricted, it counts as
+ -- consuming its rhs Many times.
+
+ do { traceTc "tcFunBindMatches 2" (vcat [ pprUserTypeCtxt ctxt, ppr invis_pat_tys
+ , ppr pat_tys $$ ppr rhs_ty ])
+ ; tcMatches tcBody (invis_pat_tys ++ pat_tys) rhs_ty matches }
+
+ ; return (wrap_fun <.> wrap_mult, r) }
+ where
+ herald = ExpectedFunTyMatches (NameThing fun_name) matches
+
+funBindPrecondition :: MatchGroup GhcRn (LHsExpr GhcRn) -> Bool
+funBindPrecondition (MG { mg_alts = L _ alts })
+ = not (null alts) && all is_fun_rhs alts
+ where
+ is_fun_rhs (L _ (Match { m_ctxt = FunRhs {} })) = True
+ is_fun_rhs _ = False
+
+tcLambdaMatches :: HsExpr GhcRn -> HsLamVariant
+ -> MatchGroup GhcRn (LHsExpr GhcRn)
+ -> [ExpPatType] -- Already skolemised
+ -> ExpSigmaType -- NB can be a sigma-type
+ -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
+tcLambdaMatches e lam_variant matches invis_pat_tys res_ty
+ = do { arity <- checkArgCounts matches
+ -- Check argument counts since this is also used for \cases
+
+ ; (wrapper, (mult_co_wrap, r))
+ <- matchExpectedFunTys herald GenSigCtxt arity res_ty $ \ pat_tys rhs_ty ->
+ tcMatches tc_body (invis_pat_tys ++ pat_tys) rhs_ty matches
+
; return (wrapper <.> mult_co_wrap, r) }
where
- arity = matchGroupArity matches
- herald = ExpectedFunTyMatches (NameThing (unLoc fun_name)) matches
- ctxt = GenSigCtxt -- Was: FunSigCtxt fun_name True
- -- But that's wrong for f :: Int -> forall a. blah
- what = FunRhs { mc_fun = fun_name, mc_fixity = Prefix, mc_strictness = strictness }
- strictness
- | [L _ match] <- unLoc $ mg_alts matches
- , FunRhs{ mc_strictness = SrcStrict } <- m_ctxt match
- = SrcStrict
- | otherwise
- = NoSrcStrict
+ herald = ExpectedFunTyLam lam_variant e
+ -- See Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
+
+ tc_body | isDoExpansionGenerated (mg_ext matches)
+ -- See Part 3. B. of Note [Expanding HsDo with XXExprGhcRn] in
+ -- `GHC.Tc.Gen.Do`. Testcase: Typeable1
+ = tcBodyNC -- NB: Do not add any error contexts
+ -- It has already been done
+ | otherwise
+ = tcBody
{-
@tcCaseMatches@ doesn't do the argument-count check because the
@@ -143,41 +167,18 @@ parser guarantees that each equation has exactly one argument.
-}
tcCaseMatches :: (AnnoBody body, Outputable (body GhcTc))
- => TcMatchAltChecker body -- ^ Case context
- -> Scaled TcSigmaTypeFRR -- ^ Type of scrutinee
+ => TcMatchAltChecker body -- ^ Typecheck the alternative RHSS
+ -> Scaled TcSigmaTypeFRR -- ^ Type of scrutinee
-> MatchGroup GhcRn (LocatedA (body GhcRn)) -- ^ The case alternatives
-> ExpRhoType -- ^ Type of the whole case expression
-> TcM (HsWrapper, MatchGroup GhcTc (LocatedA (body GhcTc)))
- -- Translated alternatives
- -- wrapper goes from MatchGroup's ty to expected ty
+ -- Translated alternatives
+ -- wrapper goes from MatchGroup's ty to expected ty
-tcCaseMatches ctxt (Scaled scrut_mult scrut_ty) matches res_ty
- = tcMatches ctxt [ExpFunPatTy (Scaled scrut_mult (mkCheckExpType scrut_ty))] res_ty matches
-
-tcLambdaMatches :: ExpectedFunTyOrigin -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify
- -> MatchGroup GhcRn (LHsExpr GhcRn)
- -> ExpRhoType
- -> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
-tcLambdaMatches herald match res_ty
- = do { checkArgCounts Nothing match
- ; (wrapper, (mult_co_wrap, r)) <- matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty ->
- -- checking argument counts since this is also used for \cases
- tcMatches match_alt_checker pat_tys rhs_ty match
- ; return (wrapper <.> mult_co_wrap, r) }
- where
- n_pats | isEmptyMatchGroup match = 1 -- must be lambda-case
- | otherwise = matchGroupArity match
-
- match_alt_checker
- | isDoExpansionGenerated (mg_ext match)
- -- See Part 3. B. of Note [Expanding HsDo with XXExprGhcRn] in `GHC.Tc.Gen.Do`. Testcase: Typeable1
- = tcBodyNC -- NB: Do not add any error contexts
- -- It has already been done
- | otherwise
- = tcBody
+tcCaseMatches tc_body (Scaled scrut_mult scrut_ty) matches res_ty
+ = tcMatches tc_body [ExpFunPatTy (Scaled scrut_mult (mkCheckExpType scrut_ty))] res_ty matches
-- @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
-
tcGRHSsPat :: Mult -> GRHSs GhcRn (LHsExpr GhcRn) -> ExpRhoType
-> TcM (GRHSs GhcTc (LHsExpr GhcTc))
-- Used for pattern bindings
@@ -228,8 +229,8 @@ tcMatches :: (AnnoBody body, Outputable (body GhcTc))
-> MatchGroup GhcRn (LocatedA (body GhcRn))
-> TcM (HsWrapper, MatchGroup GhcTc (LocatedA (body GhcTc)))
-tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
- , mg_ext = origin })
+tcMatches tc_body pat_tys rhs_ty (MG { mg_alts = L l matches
+ , mg_ext = origin })
| null matches -- Deal with case e of {}
-- Since there are no branches, no one else will fill in rhs_ty
-- when in inference mode, so we must do it ourselves,
@@ -242,7 +243,7 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches
}) }
| otherwise
- = do { umatches <- mapM (tcCollectingUsage . tcMatch ctxt pat_tys rhs_ty) matches
+ = do { umatches <- mapM (tcCollectingUsage . tcMatch tc_body pat_tys rhs_ty) matches
; let (usages, wmatches) = unzip umatches
; let (wrappers, matches') = unzip wmatches
; let wrapper = mconcat wrappers
@@ -269,37 +270,32 @@ tcMatch :: (AnnoBody body)
-> LMatch GhcRn (LocatedA (body GhcRn))
-> TcM (HsWrapper, LMatch GhcTc (LocatedA (body GhcTc)))
-tcMatch alt_checker pat_tys rhs_ty match
- = do { (L loc (wrapper, r)) <- wrapLocMA (tc_match alt_checker pat_tys rhs_ty) match
+tcMatch tc_body pat_tys rhs_ty match
+ = do { (L loc (wrapper, r)) <- wrapLocMA (tc_match pat_tys rhs_ty) match
; return (wrapper, L loc r) }
where
- tc_match match_alt_checker pat_tys rhs_ty
+ tc_match pat_tys rhs_ty
match@(Match { m_ctxt = ctxt, m_pats = pats, m_grhss = grhss })
- = add_match_ctxt match $
+ = add_match_ctxt $
do { (pats', (wrapper, grhss')) <- tcMatchPats ctxt pats pat_tys $
- tcGRHSs ctxt match_alt_checker grhss rhs_ty
- ; return (wrapper, Match { m_ext = noAnn
- , m_ctxt = ctxt
- , m_pats = filter_out_type_pats pats'
+ tcGRHSs ctxt tc_body grhss rhs_ty
+ -- NB: pats' are just the /value/ patterns
+ -- See Note [tcMatchPats] in GHC.Tc.Gen.Pat
+
+ ; return (wrapper, Match { m_ext = noAnn
+ , m_ctxt = ctxt
+ , m_pats = pats'
, m_grhss = grhss' }) }
+ where
-- For (\x -> e), tcExpr has already said "In the expression \x->e"
-- so we don't want to add "In the lambda abstraction \x->e"
-- But for \cases with many alternatives, it is helpful to say
-- which particular alternative we are looking at
- add_match_ctxt match thing_inside
- = case (m_ctxt match) of
+ add_match_ctxt thing_inside = case ctxt of
LamAlt LamSingle -> thing_inside
StmtCtxt (HsDoStmt{}) -> thing_inside -- this is an expanded do stmt
_ -> addErrCtxt (pprMatchInCtxt match) thing_inside
- -- We filter out type patterns because we have no use for them in HsToCore.
- -- Type variable bindings have already been converted to HsWrappers.
- filter_out_type_pats :: [LPat GhcTc] -> [LPat GhcTc]
- filter_out_type_pats = filterByList (map is_fun_pat_ty pat_tys)
- where
- is_fun_pat_ty ExpFunPatTy{} = True
- is_fun_pat_ty ExpForAllPatTy{} = False
-
-------------
tcGRHSs :: AnnoBody body
=> HsMatchContextRn
@@ -312,24 +308,30 @@ tcGRHSs :: AnnoBody body
-- f = \(x::forall a.a->a) -> <stuff>
-- We used to force it to be a monotype when there was more than one guard
-- but we don't need to do that any more
-tcGRHSs ctxt alt_checker (GRHSs _ grhss binds) res_ty
- = do { (binds', wrapper, grhss')
- <- tcLocalBinds binds $ do
- { ugrhss <- mapM (tcCollectingUsage . wrapLocMA (tcGRHS ctxt alt_checker res_ty)) grhss
- ; let (usages, grhss') = unzip ugrhss
- ; tcEmitBindingUsage $ supUEs usages
- ; return grhss' }
+tcGRHSs ctxt tc_body (GRHSs _ grhss binds) res_ty
+ = do { (binds', wrapper, grhss') <- tcLocalBinds binds $ do
+ tcGRHSList ctxt tc_body grhss res_ty
; return (wrapper, GRHSs emptyComments grhss' binds') }
--------------
-tcGRHS :: HsMatchContextRn -> TcMatchAltChecker body -> ExpRhoType -> GRHS GhcRn (LocatedA (body GhcRn))
- -> TcM (GRHS GhcTc (LocatedA (body GhcTc)))
-tcGRHS ctxt alt_checker res_ty (GRHS _ guards rhs)
- = do { (guards', rhs')
- <- tcStmtsAndThen stmt_ctxt tcGuardStmt guards res_ty $
- alt_checker rhs
- ; return (GRHS noAnn guards' rhs') }
- where
- stmt_ctxt = PatGuard ctxt
+
+tcGRHSList :: forall body. AnnoBody body
+ => HsMatchContextRn -> TcMatchAltChecker body
+ -> [LGRHS GhcRn (LocatedA (body GhcRn))] -> ExpRhoType
+ -> TcM [LGRHS GhcTc (LocatedA (body GhcTc))]
+tcGRHSList ctxt tc_body grhss res_ty
+ = do { (usages, grhss') <- mapAndUnzipM (wrapLocSndMA tc_alt) grhss
+ ; tcEmitBindingUsage $ supUEs usages
+ ; return grhss' }
+ where
+ stmt_ctxt = PatGuard ctxt
+
+ tc_alt :: GRHS GhcRn (LocatedA (body GhcRn))
+ -> TcM (UsageEnv, GRHS GhcTc (LocatedA (body GhcTc)))
+ tc_alt (GRHS _ guards rhs)
+ = tcCollectingUsage $
+ do { (guards', rhs')
+ <- tcStmtsAndThen stmt_ctxt tcGuardStmt guards res_ty $
+ tc_body rhs
+ ; return (GRHS noAnn guards' rhs') }
{-
************************************************************************
@@ -376,7 +378,7 @@ tcDoStmts ctxt@GhciStmtCtxt _ _ = pprPanic "tcDoStmts" (pprHsDoFlavour ctxt)
tcBody :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTc)
tcBody body res_ty
= do { traceTc "tcBody" (ppr res_ty)
- ; tcMonoExpr body res_ty
+ ; tcPolyLExpr body res_ty
}
tcBodyNC :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTc)
@@ -1199,29 +1201,34 @@ the variables they bind into scope, and typecheck the thing_inside.
-}
-- | @checkArgCounts@ takes a @[RenamedMatch]@ and decides whether the same
--- number of args are used in each equation.
+-- number of /required/ args are used in each equation.
+-- Returns the arity, the number of required args
+-- E.g. f @a True y = ...
+-- f False z = ...
+-- The MatchGroup for `f` has arity 2, not 3
checkArgCounts :: AnnoBody body
- => Maybe HsMatchContextRn
- -> MatchGroup GhcRn (LocatedA (body GhcRn))
- -> TcM ()
-checkArgCounts _ (MG { mg_alts = L _ [] })
- = return ()
-checkArgCounts mb_ctxt (MG { mg_alts = L _ (match1:matches) })
+ => MatchGroup GhcRn (LocatedA (body GhcRn))
+ -> TcM Arity
+checkArgCounts (MG { mg_alts = L _ [] })
+ = return 1 -- See Note [Empty MatchGroups] in GHC.Rename.Bind
+ -- case e of {} or \case {}
+ -- Both have arity 1
+
+checkArgCounts (MG { mg_alts = L _ (match1:matches) })
| null matches -- There was only one match; nothing to check
- = return ()
+ = return n_args1
-- Two or more matches: check that they agree on arity
| Just bad_matches <- mb_bad_matches
- = failWithTc $ TcRnMatchesHaveDiffNumArgs ctxt
+ = failWithTc $ TcRnMatchesHaveDiffNumArgs (m_ctxt (unLoc match1))
$ MatchArgMatches match1 bad_matches
| otherwise
- = return ()
+ = return n_args1
where
- ctxt = case mb_ctxt of
- Nothing -> m_ctxt (unLoc match1)
- Just x -> x
- n_args1 = args_in_match match1
- mb_bad_matches = NE.nonEmpty [m | m <- matches, args_in_match m /= n_args1]
-
- args_in_match :: (LocatedA (Match GhcRn body1) -> Int)
- args_in_match (L _ (Match { m_pats = pats })) = length pats
+ n_args1 = reqd_args_in_match match1
+ mb_bad_matches = NE.nonEmpty [m | m <- matches, reqd_args_in_match m /= n_args1]
+
+ reqd_args_in_match :: LocatedA (Match GhcRn body1) -> Arity
+ -- Counts the number of /required/ args in the match
+ -- IMPORTANT: THIS WILL NEED TO CHANGE WHEN @ty BECOMES A PATTERN
+ reqd_args_in_match (L _ (Match { m_pats = pats })) = length pats
diff --git a/compiler/GHC/Tc/Gen/Match.hs-boot b/compiler/GHC/Tc/Gen/Match.hs-boot
index d48a5974336d7a84e033d3921f15492caf70bcfa..724c579bd0a64db40a58dd843136ed9938ef18e3 100644
--- a/compiler/GHC/Tc/Gen/Match.hs-boot
+++ b/compiler/GHC/Tc/Gen/Match.hs-boot
@@ -1,19 +1,21 @@
module GHC.Tc.Gen.Match where
import GHC.Hs ( GRHSs, MatchGroup, LHsExpr, Mult )
-import GHC.Tc.Types.Evidence ( HsWrapper )
-import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType )
+import GHC.Tc.Utils.TcType( ExpSigmaType, ExpRhoType, ExpPatType )
import GHC.Tc.Types ( TcM )
+import GHC.Tc.Types.Origin ( UserTypeCtxt )
+import GHC.Tc.Types.Evidence ( HsWrapper )
+import GHC.Types.Name ( Name )
import GHC.Hs.Extension ( GhcRn, GhcTc )
-import GHC.Parser.Annotation ( LocatedN )
-import GHC.Types.Name (Name)
tcGRHSsPat :: Mult
-> GRHSs GhcRn (LHsExpr GhcRn)
-> ExpRhoType
-> TcM (GRHSs GhcTc (LHsExpr GhcTc))
-tcFunBindMatches :: LocatedN Name
+tcFunBindMatches :: UserTypeCtxt
+ -> Name
-> Mult
-> MatchGroup GhcRn (LHsExpr GhcRn)
+ -> [ExpPatType]
-> ExpSigmaType
-> TcM (HsWrapper, MatchGroup GhcTc (LHsExpr GhcTc))
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 64a9d8f24176a62fb90cb1dea7b558a3a51d89fe..2c22abb29f82e2502420c50da677c2946dd707c7 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1,6 +1,7 @@
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeFamilies #-}
@@ -123,27 +124,75 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside
not_xstrict _ = checkManyPattern pat_ty
-----------------
-tcMatchPats :: HsMatchContextRn
+tcMatchPats :: forall a.
+ HsMatchContextRn
-> [LPat GhcRn] -- ^ patterns
-> [ExpPatType] -- ^ types of the patterns
-> TcM a -- ^ checker for the body
-> TcM ([LPat GhcTc], a)
-
--- This is the externally-callable wrapper function
--- Typecheck the patterns, extend the environment to bind the variables,
--- do the thing inside, use any existentially-bound dictionaries to
--- discharge parts of the returning LIE, and deal with pattern type
--- signatures
-
--- 1. Initialise the PatState
--- 2. Check the patterns
--- 3. Check the body
--- 4. Check that no existentials escape
-
-tcMatchPats ctxt pats pat_tys thing_inside
- = tc_tt_lpats pat_tys penv pats thing_inside
+-- See Note [tcMatchPats]
+--
+-- PRECONDITION:
+-- number of visible Pats in pats
+-- (@a is invisible)
+-- = number of visible ExpPatTypes in pat_tys
+-- (ExpForAllPatTy v is visible iff b is Required)
+--
+-- POSTCONDITION:
+-- Returns only the /value/ patterns; see Note [tcMatchPats]
+
+tcMatchPats match_ctxt pats pat_tys thing_inside
+ = assertPpr (count isVisibleExpPatType pat_tys == length pats)
+ (ppr pats $$ ppr pat_tys) $
+ -- Check PRECONDITION
+ -- When we get @patterns the (length pats) will change
+ do { err_ctxt <- getErrCtxt
+ ; let loop :: [LPat GhcRn] -> [ExpPatType] -> TcM ([LPat GhcTc], a)
+
+ -- No more patterns. Discard excess pat_tys;
+ -- they should all be invisible. Example:
+ -- f :: Int -> forall a b. blah
+ -- f x @p = rhs
+ -- We will call tcMatchPats with
+ -- pats = [x, @p]
+ -- pat_tys = [Int, @a, @b]
+ loop [] pat_tys
+ = assertPpr (not (any isVisibleExpPatType pat_tys)) (ppr pats $$ ppr pat_tys) $
+ do { res <- setErrCtxt err_ctxt thing_inside
+ ; return ([], res) }
+
+ -- ExpFunPatTy: expecting a value pattern
+ -- tc_lpat will error if it sees a @t type pattern
+ loop (pat : pats) (ExpFunPatTy pat_ty : pat_tys)
+ = do { (p, (ps, res)) <- tc_lpat pat_ty penv pat $
+ loop pats pat_tys
+ ; return (p:ps, res) }
+
+ -- ExpForAllPat: expecting a type pattern
+ loop (pat : pats) (ExpForAllPatTy bndr : pat_tys)
+ | Bndr tv vis <- bndr
+ , isVisibleForAllTyFlag vis
+ = do { (_p, (ps, res)) <- tc_forall_lpat tv penv pat $
+ loop pats pat_tys
+
+ ; return (ps, res) }
+
+ -- Invisible forall in type, and an @a type pattern
+ -- Add an equation here when we have these
+ -- E.g. f :: forall a. Bool -> a -> blah
+ -- f @b True x = rhs1 -- b is bound to skolem a
+ -- f @c False y = rhs2 -- c is bound to skolem a
+
+ | otherwise -- Discard invisible pat_ty
+ = loop (pat:pats) pat_tys
+
+ loop pats@(_:_) [] = pprPanic "tcMatchPats" (ppr pats)
+ -- Failure of PRECONDITION
+
+ ; loop pats pat_tys }
where
- penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }
+ penv = PE { pe_lazy = False, pe_ctxt = LamPat match_ctxt, pe_orig = PatOrigin }
+
tcInferPat :: FixedRuntimeRepContext
-> HsMatchContextRn
@@ -174,7 +223,26 @@ tcCheckPat_O ctxt orig pat (Scaled pat_mult pat_ty) thing_inside
penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
-{-
+{- Note [tcMatchPats]
+~~~~~~~~~~~~~~~~~~~~~
+tcMatchPats is the externally-callable wrapper function for
+ function definitions f p1 .. pn = rhs
+ lambdas \p1 .. pn -> body
+Typecheck the patterns, extend the environment to bind the variables, do the
+thing inside, use any existentially-bound dictionaries to discharge parts of
+the returning LIE, and deal with pattern type signatures
+
+It takes the list of patterns writen by the user, but it returns only the
+/value/ patterns. For example:
+ f :: forall a. forall b -> a -> Mabye b -> blah
+ f @a w x (Just y) = ....
+tcMatchPats returns only the /value/ patterns [x, Just y]. Why? The
+desugarer expects only value patterns. (We could change that, but we would
+have to do so carefullly.) However, distinguishing value patterns from type
+patterns is a bit tricky; e.g. the `w` in this example. So it's very
+convenient to filter them out right here.
+
+
************************************************************************
* *
PatEnv, PatCtxt, LetBndrSpec
@@ -371,14 +439,6 @@ tc_lpat pat_ty penv (L span pat) thing_inside
thing_inside
; return (L span pat', res) }
-tc_tt_lpat :: ExpPatType
- -> Checker (LPat GhcRn) (LPat GhcTc)
-tc_tt_lpat pat_ty penv (L span pat) thing_inside
- = setSrcSpanA span $
- do { (pat', res) <- maybeWrapPatCtxt pat (tc_tt_pat pat_ty penv pat)
- thing_inside
- ; return (L span pat', res) }
-
tc_lpats :: [Scaled ExpSigmaTypeFRR]
-> Checker [LPat GhcRn] [LPat GhcTc]
tc_lpats tys penv pats
@@ -387,38 +447,33 @@ tc_lpats tys penv pats
penv
(zipEqual "tc_lpats" pats tys)
-tc_tt_lpats :: [ExpPatType] -> Checker [LPat GhcRn] [LPat GhcTc]
-tc_tt_lpats tys penv pats
- = assertPpr (equalLength pats tys) (ppr pats $$ ppr tys) $
- tcMultiple (\ penv' (p,t) -> tc_tt_lpat t penv' p)
- penv
- (zipEqual "tc_tt_lpats" pats tys)
-
--------------------
-- See Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify.
checkManyPattern :: Scaled a -> TcM HsWrapper
checkManyPattern pat_ty = tcSubMult NonLinearPatternOrigin ManyTy (scaledMult pat_ty)
-tc_tt_pat
- :: ExpPatType
- -- ^ Fully refined result type
- -> Checker (Pat GhcRn) (Pat GhcTc)
- -- ^ Translated pattern
-tc_tt_pat pat_ty penv (ParPat x pat) thing_inside = do
- { (pat', res) <- tc_tt_lpat pat_ty penv pat thing_inside
- ; return (ParPat x pat', res) }
-tc_tt_pat (ExpFunPatTy pat_ty) penv pat thing_inside = tc_pat pat_ty penv pat thing_inside
-tc_tt_pat (ExpForAllPatTy tv) penv pat thing_inside = tc_forall_pat penv (pat, tv) thing_inside
-tc_forall_pat :: Checker (Pat GhcRn, TcTyVar) (Pat GhcTc)
-tc_forall_pat _ (EmbTyPat _ tp, tv) thing_inside
+tc_forall_lpat :: TcTyVar -> Checker (LPat GhcRn) (LPat GhcTc)
+tc_forall_lpat tv penv (L span pat) thing_inside
+ = setSrcSpanA span $
+ do { (pat', res) <- maybeWrapPatCtxt pat (tc_forall_pat tv penv pat)
+ thing_inside
+ ; return (L span pat', res) }
+
+tc_forall_pat :: TcTyVar -> Checker (Pat GhcRn) (Pat GhcTc)
+tc_forall_pat tv penv (ParPat x lpat) thing_inside
+ = do { (lpat', res) <- tc_forall_lpat tv penv lpat thing_inside
+ ; return (ParPat x lpat', res) }
+
+tc_forall_pat tv _ (EmbTyPat _ tp) thing_inside
-- The entire type pattern is guarded with the `type` herald:
-- f (type t) (x :: t) = ...
-- This special case is not necessary for correctness but avoids
-- a redundant `ExpansionPat` node.
= do { (arg_ty, result) <- tc_ty_pat tp tv thing_inside
; return (EmbTyPat arg_ty tp, result) }
-tc_forall_pat _ (pat, tv) thing_inside
+
+tc_forall_pat tv _ pat thing_inside
-- The type pattern is not guarded with the `type` herald, or perhaps
-- only parts of it are, e.g.
-- f (t :: Type) (x :: t) = ... -- no `type` herald
@@ -565,7 +620,7 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of
-- Expression must be a function
; let herald = ExpectedFunTyViewPat $ unLoc expr
; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)
- <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,[]) expr_ty
+ <- matchActualFunTy herald (Just . HsExprRnThing $ unLoc expr) (1,expr_ty) expr_ty
-- See Note [View patterns and polymorphism]
-- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_sigma)
diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs
index eee5e648cdce5b8bb35740056267950518686c9a..edd3f651dda5358408a94774a754ca2ed4bf8ee9 100644
--- a/compiler/GHC/Tc/Gen/Sig.hs
+++ b/compiler/GHC/Tc/Gen/Sig.hs
@@ -41,7 +41,7 @@ import GHC.Tc.Zonk.Type
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType
import GHC.Tc.Validity ( checkValidType )
-import GHC.Tc.Utils.Unify( tcTopSkolemise, unifyType )
+import GHC.Tc.Utils.Unify( DeepSubsumptionFlag(..), tcSkolemise, unifyType )
import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
import GHC.Tc.Utils.Env( tcLookupId )
import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
@@ -519,7 +519,6 @@ tcInstSig hs_sig@(TcPartialSig (PSig { psig_hs_ty = hs_ty
; traceTc "End partial sig }" (ppr inst_sig)
; return inst_sig }
-
{- Note [Pattern bindings and complete signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
@@ -806,7 +805,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)
- <- tcTopSkolemise ctxt spec_ty $ \ spec_tau ->
+ <- tcSkolemise Shallow 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/Types.hs b/compiler/GHC/Tc/Types.hs
index fe3aa4b5e88a8b17dd714ba28c05385cc3bcaf33..4e091bd3d2381c83192084c8c2e9e915d263fe01 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -71,8 +71,8 @@ module GHC.Tc.Types(
TcSigInfo(..), TcIdSig(..),
TcCompleteSig(..), TcPartialSig(..), TcPatSynSig(..),
TcIdSigInst(..),
- isPartialSig, hasCompleteSig,
- tcIdSigLoc, tcSigInfoName, completeSigPolyId_maybe,
+ isPartialSig, hasCompleteSig, tcSigInfoName, tcIdSigLoc,
+ completeSigPolyId_maybe,
-- Misc other types
TcId,
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index a5639af6fd197ebf2d5f399195b7b96602571c6c..82e60727aa91291dde711c230754d13a0f7f8d38 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -160,10 +160,14 @@ data UserTypeCtxt
-- | Report Redundant Constraints.
data ReportRedundantConstraints
= NoRRC -- ^ Don't report redundant constraints
- | WantRRC SrcSpan -- ^ Report redundant constraints, and here
- -- is the SrcSpan for the constraints
- -- E.g. f :: (Eq a, Ord b) => blah
- -- The span is for the (Eq a, Ord b)
+
+ | WantRRC SrcSpan -- ^ Report redundant constraints
+ -- The SrcSpan is for the constraints
+ -- E.g. f :: (Eq a, Ord b) => blah
+ -- The span is for the (Eq a, Ord b)
+ -- We need to record the span here because we have
+ -- long since discarded the HsType in favour of a Type
+
deriving( Eq ) -- Just for checkSkolInfoAnon
reportRedundantConstraints :: ReportRedundantConstraints -> Bool
@@ -436,7 +440,7 @@ in the right place. So we proceed as follows:
whatever it tidies to, say a''; and then we walk over the type
replacing the binder a by the tidied version a'', to give
forall a''. Eq a'' => forall b''. b'' -> a''
- We need to do this under (=>) arrows, to match what topSkolemise
+ We need to do this under (=>) arrows and (->), to match what skolemisation
does.
* Typically a'' will have a nice pretty name like "a", but the point is
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs
index 6ce7aea8788cf16ce62593f143f62c30577f2da9..5a7e4f101669512ecc4aef7413597dc32a573cf9 100644
--- a/compiler/GHC/Tc/Utils/Instantiate.hs
+++ b/compiler/GHC/Tc/Utils/Instantiate.hs
@@ -19,7 +19,7 @@ module GHC.Tc.Utils.Instantiate (
tcInstType, tcInstTypeBndrs,
tcSkolemiseInvisibleBndrs,
- tcInstSkolTyVars, tcInstSkolTyVarsX,
+ tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarBndrsX,
tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
freshenTyVarBndrs, freshenCoVarBndrsX,
@@ -157,9 +157,10 @@ Examples:
= ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2
-This second example is the reason for the recursive 'go'
-function in topSkolemise: we must remove successive layers
-of foralls and (=>).
+This second example is the reason for the recursive 'go' function in
+topSkolemise: we remove successive layers of foralls and (=>). This
+is really just an optimisation; see wrinkle (SK1) in GHC.Tc.Utils.Unify
+Note [Skolemisation overview].
In general,
if topSkolemise ty = (wrap, tvs, evs, rho)
@@ -172,8 +173,8 @@ In general,
topSkolemise :: SkolemInfo
-> TcSigmaType
-> TcM ( HsWrapper
- , [(Name,TyVar)] -- All skolemised variables
- , [EvVar] -- All "given"s
+ , [(Name,TcInvisTVBinder)] -- All skolemised variables
+ , [EvVar] -- All "given"s
, TcRhoType )
-- See Note [Skolemisation]
topSkolemise skolem_info ty
@@ -183,13 +184,17 @@ topSkolemise skolem_info ty
-- Why recursive? See Note [Skolemisation]
go subst wrap tv_prs ev_vars ty
- | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty
+ | (bndrs, theta, inner_ty) <- tcSplitSigmaTyBndrs ty
+ , let tvs = binderVars bndrs
, not (null tvs && null theta)
- = do { (subst', tvs1) <- tcInstSkolTyVarsX skolem_info subst tvs
- ; ev_vars1 <- newEvVars (substTheta subst' theta)
+ = do { (subst', bndrs1) <- tcInstSkolTyVarBndrsX skolem_info subst bndrs
+ ; let tvs1 = binderVars bndrs1
+ ; traceTc "topSkol" (vcat [ ppr tvs <+> vcat (map (ppr . getSrcSpan) tvs)
+ , ppr tvs1 <+> vcat (map (ppr . getSrcSpan) tvs1) ])
+ ; ev_vars1 <- newEvVars (substTheta subst' theta)
; go subst'
(wrap <.> mkWpTyLams tvs1 <.> mkWpEvLams ev_vars1)
- (tv_prs ++ (map tyVarName tvs `zip` tvs1))
+ (tv_prs ++ (map tyVarName tvs `zip` bndrs1))
(ev_vars ++ ev_vars1)
inner_ty }
@@ -514,6 +519,13 @@ tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
tcInstSkolTyVarsX skol_info = tcInstSkolTyVarsPushLevel skol_info False
+tcInstSkolTyVarBndrsX :: SkolemInfo -> Subst -> [VarBndr TyCoVar vis] -> TcM (Subst, [VarBndr TyCoVar vis])
+tcInstSkolTyVarBndrsX skol_info subs bndrs = do
+ (subst', bndrs') <- tcInstSkolTyVarsX skol_info subs (binderVars bndrs)
+ pure (subst', zipWith mkForAllTyBinder flags bndrs')
+ where
+ flags = binderFlags bndrs
+
tcInstSuperSkolTyVars :: SkolemInfo -> [TyVar] -> TcM (Subst, [TcTyVar])
-- See Note [Skolemising type variables]
-- This version freshens the names and creates "super skolems";
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 7b7867235ef31744709cb2473fd774be5e2ff27d..8b34b54adb8c66d95c939ab6225b95560fd5f578 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -55,7 +55,7 @@ module GHC.Tc.Utils.TcMType (
--------------------------------
-- Instantiation
- newMetaTyVars, newMetaTyVarX, newMetaTyVarsX,
+ newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, newMetaTyVarBndrsX,
newMetaTyVarTyVarX,
newTyVarTyVar, cloneTyVarTyVar,
newConcreteTyVarX,
@@ -1022,6 +1022,13 @@ newMetaTyVarsX :: Subst -> [TyVar] -> TcM (Subst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst
+newMetaTyVarBndrsX :: Subst -> [VarBndr TyVar vis] -> TcM (Subst, [VarBndr TcTyVar vis])
+newMetaTyVarBndrsX subst bndrs = do
+ (subst, bndrs') <- newMetaTyVarsX subst (binderVars bndrs)
+ pure (subst, zipWith mkForAllTyBinder flags bndrs')
+ where
+ flags = binderFlags bndrs
+
newMetaTyVarX :: Subst -> TyVar -> TcM (Subst, TcTyVar)
-- Make a new unification variable tyvar whose Name and Kind come from
-- an existing TyVar. We substitute kind variables in the kind.
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index bcefd9d6d576462edfceb4081b0b51a9e49ebfb2..40da653b1d8e5199eb6de43e5f8ce5b4a1701100 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -33,7 +33,8 @@ module GHC.Tc.Utils.TcType (
mkCheckExpType,
checkingExpType_maybe, checkingExpType,
- ExpPatType(..),
+ ExpPatType(..), mkCheckExpFunPatTy, mkInvisExpPatType,
+ isVisibleExpPatType, isExpFunPatType,
SyntaxOpType(..), synKnownType, mkSynFunTys,
@@ -76,7 +77,7 @@ module GHC.Tc.Utils.TcType (
tcSplitTyConApp, tcSplitTyConApp_maybe,
tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcSplitAppTyNoView_maybe,
- tcSplitSigmaTy, tcSplitNestedSigmaTys, tcSplitIOType_maybe,
+ tcSplitSigmaTy, tcSplitSigmaTyBndrs, tcSplitNestedSigmaTys, tcSplitIOType_maybe,
---------------------------------
-- Predicates.
@@ -453,16 +454,30 @@ checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe (Check ty) = Just ty
checkingExpType_maybe (Infer {}) = Nothing
--- | Returns the expected type when in checking mode. Panics if in inference
--- mode.
-checkingExpType :: String -> ExpType -> TcType
-checkingExpType _ (Check ty) = ty
-checkingExpType err et = pprPanic "checkingExpType" (text err $$ ppr et)
+-- | Returns the expected type when in checking mode.
+-- Panics if in inference mode.
+checkingExpType :: ExpType -> TcType
+checkingExpType (Check ty) = ty
+checkingExpType et@(Infer {}) = pprPanic "checkingExpType" (ppr et)
-- Expected type of a pattern in a lambda or a function left-hand side.
data ExpPatType =
ExpFunPatTy (Scaled ExpSigmaTypeFRR) -- the type A of a function A -> B
- | ExpForAllPatTy TcTyVar -- the binder (a::A) of forall (a::A) -> B
+ | ExpForAllPatTy ForAllTyBinder -- the binder (a::A) of forall (a::A) -> B or forall (a :: A). B
+
+mkCheckExpFunPatTy :: Scaled TcType -> ExpPatType
+mkCheckExpFunPatTy (Scaled mult ty) = ExpFunPatTy (Scaled mult (mkCheckExpType ty))
+
+mkInvisExpPatType :: InvisTyBinder -> ExpPatType
+mkInvisExpPatType (Bndr tv spec) = ExpForAllPatTy (Bndr tv (Invisible spec))
+
+isVisibleExpPatType :: ExpPatType -> Bool
+isVisibleExpPatType (ExpForAllPatTy (Bndr _ vis)) = isVisibleForAllTyFlag vis
+isVisibleExpPatType (ExpFunPatTy {}) = True
+
+isExpFunPatType :: ExpPatType -> Bool
+isExpFunPatType ExpFunPatTy{} = True
+isExpFunPatType ExpForAllPatTy{} = False
instance Outputable ExpPatType where
ppr (ExpFunPatTy t) = ppr t
@@ -559,7 +574,7 @@ TcTyVar. This is very convenient to a consumer of a SkolemTv, but it is
a bit awkward for the /producer/. Why? Because sometimes we can't produce
the SkolemInfo until we have the TcTyVars!
-Example: in `GHC.Tc.Utils.Unify.tcTopSkolemise` we create SkolemTvs whose
+Example: in `GHC.Tc.Utils.Unify.tcSkolemise` we create SkolemTvs whose
`SkolemInfo` is `SigSkol`, whose arguments in turn mention the newly-created
SkolemTvs. So we a RecrusiveDo idiom, like this:
@@ -1435,6 +1450,11 @@ tcSplitSigmaTy ty = case tcSplitForAllInvisTyVars ty of
(tvs, rho) -> case tcSplitPhiTy rho of
(theta, tau) -> (tvs, theta, tau)
+tcSplitSigmaTyBndrs :: Type -> ([TcInvisTVBinder], ThetaType, Type)
+tcSplitSigmaTyBndrs ty = case tcSplitForAllInvisTVBinders ty of
+ (tvs, rho) -> case tcSplitPhiTy rho of
+ (theta, tau) -> (tvs, theta, tau)
+
-- | Split a sigma type into its parts, going underneath as many arrows
-- and foralls as possible. See Note [tcSplitNestedSigmaTys]
tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type)
@@ -1862,18 +1882,22 @@ See also GHC.Tc.TyCl.Utils.checkClassCycles.
-}
isSigmaTy :: TcType -> Bool
--- isSigmaTy returns true of any qualified type. It doesn't
--- *necessarily* have any foralls. E.g
--- f :: (?x::Int) => Int -> Int
-isSigmaTy ty | Just ty' <- coreView ty = isSigmaTy ty'
-isSigmaTy (ForAllTy {}) = True
+-- isSigmaTy returns true of any type with /invisible/ quantifiers at the top:
+-- forall a. blah
+-- Eq a => blah
+-- ?x::Int => blah
+-- But not
+-- forall a -> blah
+isSigmaTy (ForAllTy (Bndr _ af) _) = isInvisibleForAllTyFlag af
isSigmaTy (FunTy { ft_af = af }) = isInvisibleFunArg af
+isSigmaTy ty | Just ty' <- coreView ty = isSigmaTy ty'
isSigmaTy _ = False
+
isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType]
-isRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
-isRhoTy (ForAllTy {}) = False
+isRhoTy (ForAllTy (Bndr _ af) _) = isVisibleForAllTyFlag af
isRhoTy (FunTy { ft_af = af }) = isVisibleFunArg af
+isRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
isRhoTy _ = True
-- | Like 'isRhoTy', but also says 'True' for 'Infer' types
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 08f54b5051e465136a9c752eedb998930aebd16b..43de138d4aef552f5660cf78cda2238fe7986fa0 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -13,12 +13,15 @@
module GHC.Tc.Utils.Unify (
-- Full-blown subsumption
tcWrapResult, tcWrapResultO, tcWrapResultMono,
- tcTopSkolemise, tcSkolemiseScoped, tcSkolemiseExpType,
tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS,
tcSubTypeAmbiguity, tcSubMult,
checkConstraints, checkTvConstraints,
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
+ -- Skolemisation
+ DeepSubsumptionFlag(..), getDeepSubsumptionFlag,
+ tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
+
-- Various unifications
unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
unifyTypeAndEmit, promoteTcType,
@@ -70,6 +73,7 @@ import qualified GHC.LanguageExtensions as LangExt
import GHC.Builtin.Types
import GHC.Types.Name
+import GHC.Types.Id( idType )
import GHC.Types.Var as Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
@@ -108,10 +112,9 @@ matchActualFunTy
-- ^ See Note [Herald for matchExpectedFunTys]
-> Maybe TypedThing
-- ^ The thing with type TcSigmaType
- -> (Arity, [Scaled TcSigmaType])
+ -> (Arity, TcType)
-- ^ Total number of value args in the call, and
- -- types of values args to which function has
- -- been applied already (reversed)
+ -- the original function type
-- (Both are used only for error messages)
-> TcRhoType
-- ^ Type to analyse: a TcRhoType
@@ -173,27 +176,23 @@ matchActualFunTy herald mb_thing err_info fun_ty
------------
defer fun_ty
- = do { arg_ty <- newOpenFlexiFRRTyVarTy (FRRExpectedFunTy herald 1)
+ = do { arg_ty <- new_check_arg_ty herald 1
; res_ty <- newOpenFlexiTyVarTy
- ; mult <- newFlexiTyVarTy multiplicityTy
- ; let unif_fun_ty = tcMkVisFunTy mult arg_ty res_ty
+ ; let unif_fun_ty = mkScaledFunTys [arg_ty] res_ty
; co <- unifyType mb_thing fun_ty unif_fun_ty
- ; return (mkWpCastN co, Scaled mult arg_ty, res_ty) }
+ ; return (mkWpCastN co, arg_ty, res_ty) }
------------
mk_ctxt :: TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
- mk_ctxt res_ty env = mkFunTysMsg env herald [Anon t visArgTypeLike | t <- reverse arg_tys_so_far]
- res_ty n_val_args_in_call
- (n_val_args_in_call, arg_tys_so_far) = err_info
+ mk_ctxt _res_ty = mkFunTysMsg herald err_info
{- Note [matchActualFunTy error handling]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
matchActualFunTy is made much more complicated by the
desire to produce good error messages. Consider the application
f @Int x y
-In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments,
-and then call matchActualFunTysPart for each individual value
-argument. It, in turn, must instantiate any type/dictionary args,
+In GHC.Tc.Gen.Head.tcInstFun we instantiate the function type, one
+argument at a time. It must instantiate any type/dictionary args,
before looking for an arrow type.
But if it doesn't find an arrow type, it wants to generate a message
@@ -217,7 +216,6 @@ Ugh!
-- See Note [Return arguments with a fixed RuntimeRep].
matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpectedFunTys]
-> CtOrigin
- -> Maybe TypedThing -- ^ the thing with type TcSigmaType
-> Arity
-> TcSigmaType
-> TcM (HsWrapper, [Scaled TcSigmaTypeFRR], TcRhoType)
@@ -225,8 +223,8 @@ matchActualFunTys :: ExpectedFunTyOrigin -- ^ See Note [Herald for matchExpected
-- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
-- and res_ty is a RhoType
-- NB: the returned type is top-instantiated; it's a RhoType
-matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty
- = go n_val_args_wanted [] fun_ty
+matchActualFunTys herald ct_orig n_val_args_wanted top_ty
+ = go n_val_args_wanted [] top_ty
where
go n so_far fun_ty
| not (isRhoTy fun_ty)
@@ -238,8 +236,8 @@ matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty
go n so_far fun_ty
= do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy
- herald mb_thing
- (n_val_args_wanted, so_far)
+ herald Nothing
+ (n_val_args_wanted, top_ty)
fun_ty
; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty
@@ -250,10 +248,390 @@ matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty
{-
************************************************************************
* *
- matchExpected functions
+ Skolemisation and matchExpectedFunTys
* *
************************************************************************
+Note [Skolemisation overview]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose f :: (forall a. a->a) -> blah, and we have the application (f e)
+Then we want to typecheck `e` pushing in the type `forall a. a->a`. But we
+need to be careful:
+
+* Roughly speaking, in (tcPolyExpr e (forall a b. rho)), we skolemise `a` and `b`,
+ and then call (tcExpr e rho)
+
+* But not quite! We must be careful if `e` is a type lambda (\ @p @q -> blah).
+ Then we want to line up the skolemised variables `a`,`b`
+ with `p`,`q`, so we can't just call (tcExpr (\ @p @q -> blah) rho)
+
+* A very similar situation arises with
+ (\ @p @q -> blah) :: forall a b. rho
+ Again, we must line up `p`, `q` with the skolemised `a` and `b`.
+
+* Another similar situation arises with
+ g :: forall a b. rho
+ g @p @q x y = ....
+ Here again when skolemising `a` and `b` we must be careful to match them up
+ with `p` and `q`.
+
+OK, so how exactly do we check @p binders in lambdas? First note that we only
+we only attempt to deal with @p binders when /checking/. We don't do inference for
+(\ @a -> blah), not yet anyway.
+
+For checking, there are two cases to consider:
+ * Function LHS, where the function has a type signature
+ f :: forall a. a -> forall b. [b] -> blah
+ f @p x @q y = ...
+
+ * Lambda \ @p x @q y -> ...
+ \cases { @p x @q y -> ... }
+ (\case p behaves like \cases { p -> ... }, and p is always a term pattern.)
+
+Both ultimately handled by matchExpectedFunTys.
+
+* Function LHS case is handled by `GHC.Tc.Gen.Bind.tcPolyCheck`:
+ * It calls `tcSkolemiseCompleteSig`
+ * Passes the skolemised variables into `tcFunBindMatches`
+ * Which uses `matchExpectedFunTys` to decompose the function type to
+ match the arguments
+ * And then passes the (skolemised-variables ++ arg tys) on to `tcMatches`
+
+* For the Lambda case there are two sub-cases:
+ * An expression with a type signature: (\ @a x y -> blah) :: hs_ty
+ This is handled by `GHC.Tc.Gen.Head.tcExprWithSig`, which kind-checks
+ the signature and hands off to `tcExprPolyCheck` vai `tcPolyLExprSig`
+ Note that the foralls at the top of hs_ty scope over the expression.
+
+ * A higher order call: h e, where h :: poly_ty -> blah
+ This is handlded by `GHC.Tc.Gen.Expr.tcPolyExpr`, which (in the
+ checking case) again hands off to `tcExprPolyCheck`. Here there is
+ no type-variable scoping to worry about.
+
+ So both sub-cases end up in `GHC.Tc.Gen.Expr.tcPolyExprCheck`
+ * This skolemises the /top-level/ invisible binders, but remembers
+ the binders as [ExpPatType]
+ * Then it looks for a lambda, and if so, calls `tcLambdaMatches` passing in
+ the skolemised binders so they can be matched up with the lambda binders.
+ * Otherwise it does deep-skolemisation if DeepSubsumption is on,
+ and then calls tcExpr to typecheck `e`
+
+ The outer skolemisation in tcPolyExprCheck is done using
+ * tcSkolemiseCompleteSig when there is a user-written signature
+ * tcSkolemiseGeneral when the polytype just comes from the context e.g. (f e)
+ The former just calls the latter, so the two cases differ only slightly:
+ * Both do shallow skolemisation
+ * Both go via checkConstraints, which uses implicationNeeded to decide whether
+ to build an implication constraint even if there /are/ no skolems.
+ See Note [When to build an implication] below.
+
+ The difference between the two cases is that `tcSkolemiseCompleteSig`
+ also brings the outer type variables into scope. It would do no
+ harm to do so in both cases, but I found that (to my surprise) doing
+ so caused a non-trivial (1%-ish) perf hit on the compiler.
+
+* `tcFunBindMatches` and `tcLambdaMatches` both use `matchExpectedFunTys`, which
+ ensures that any trailing invisible binders are skolemised; and does so deeply
+ if DeepSubsumption is on.
+
+ This corresponds to the plan: "skolemise at the '=' of a function binding or
+ at the '->' of a lambda binding". (See #17594 and "Plan B2".)
+
+Some wrinkles
+
+(SK1) tcSkolemiseGeneral and tcSkolemiseCompleteSig make fresh type variables
+ See Note [Instantiate sig with fresh variables]
+
+(SK2) All skolemisation (even without DeepSubsumption) builds just one implication
+ constraint for a nested forall like:
+ forall a. Eq a => forall b. Ord b => blah
+ The implication constraint will look like
+ forall a b. (Eq a, Ord b) => <constraints>
+ See the loop in GHC.Tc.Utils.Instantiate.topSkolemise.
+ This is just an optimisation; it would be fine to generate one implication
+ constraint for each nesting layer.
+
+Some examples:
+
+* f :: forall a b. blah
+ f @p x = rhs
+ `tcPolyCheck` calls `tcSkolemiseCompleteSig` to skolemise the signature, and
+ then calls `tcFunBindMatches` passing in [a_sk, b_sk], the skolemsed
+ variables. The latter ultimately calls `tcMatches`, and thence `tcMatchPats`.
+ The latter matches up the `a_sk` with `@p`, and discards the `b_sk`.
+
+* f :: forall (a::Type) (b::a). blah
+ f @(p::b) x = rhs
+ `tcSkolemiseCompleteSig` brings `a` and `b` into scope, bound to `a_sk` and `b_sk` resp.
+ When `tcMatchPats` typechecks the pattern `@(p::b)` it'll find that `b` is in
+ scope (as a result of tcSkolemiseCompleteSig) which is a bit strange. But
+ it'll then unify the kinds `Type ~ b`, which will fail as it should.
+
+* f :: Int -> forall (a::Type) (b::a). blah
+ f x @p = rhs
+ `matchExpectedFunTys` does shallow skolemisation eagerly, so we'll skolemise the
+ forall a b. Then `tcMatchPats` will bind [p :-> a_sk], and discard `b_sk`.
+ Discarding the `b_sk` means that
+ f x @p = \ @q -> blah
+ or f x @p = let .. in \ @q -> blah
+ will both be rejected: this is Plan B2: skolemise at the "=".
+
+* Suppose DeepSubsumption is on
+ f :: forall a. a -> forall b. b -> b -> forall z. z
+ f @p x @q y = rhs
+ The `tcSkolemiseCompleteSig` uses shallow skolemisation, so it only skolemises
+ and brings into scope [a :-> a_sk]. Then `matchExpectedFunTys` skolemises the
+ forall b, because it needs to expose two value arguments. Finally
+ `matchExpectedFunTys` concludes with deeply skolemising the remaining type.
+
+ So we end up with `[p :-> a_sk, q :-> b_sk]`. Notice that we must not
+ deeply-skolemise /first/ or we'd get the tyvars [a_sk, b_sk, c_sk] which would
+ not line up with the patterns [@p, x, @q, y]
+-}
+
+tcSkolemiseGeneral
+ :: DeepSubsumptionFlag
+ -> UserTypeCtxt
+ -> TcType -> TcType -- top_ty and expected_ty
+ -- Here, top_ty is the type we started to skolemise; used only in SigSkol
+ -- - expected_ty is the type we are actually skolemising
+ -- matchExpectedFunTys walks down the type, skolemising as it goes,
+ -- keeping the same top_ty, but successively smaller expected_tys
+ -> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
+ -> TcM (HsWrapper, result)
+tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
+ | definitely_mono ds_flag expected_ty
+ -- Fast path for a very very common case: no skolemisation to do
+ -- But still call checkConstraints in case we need an implication regardless
+ = do { let sig_skol = SigSkol ctxt top_ty []
+ ; (ev_binds, result) <- checkConstraints sig_skol [] [] $
+ thing_inside [] expected_ty
+ ; return (mkWpLet ev_binds, result) }
+
+ | otherwise
+ = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ ; rec { (wrap, tv_prs, given, rho_ty) <- case ds_flag of
+ Deep -> deeplySkolemise skol_info expected_ty
+ Shallow -> topSkolemise skol_info expected_ty
+ ; let sig_skol = SigSkol ctxt top_ty (map (fmap binderVar) tv_prs)
+ ; skol_info <- mkSkolemInfo sig_skol }
+
+ ; let skol_tvs = map (binderVar . snd) tv_prs
+ ; traceTc "tcSkolemiseGeneral" (pprUserTypeCtxt ctxt <+> ppr skol_tvs <+> ppr given)
+ ; (ev_binds, result) <- checkConstraints sig_skol skol_tvs given $
+ thing_inside tv_prs rho_ty
+
+ ; return (wrap <.> mkWpLet ev_binds, result) }
+ -- The ev_binds returned by checkConstraints is very
+ -- often empty, in which case mkWpLet is a no-op
+
+tcSkolemiseCompleteSig :: TcCompleteSig
+ -> ([ExpPatType] -> TcRhoType -> TcM result)
+ -> TcM (HsWrapper, result)
+-- ^ The wrapper has type: spec_ty ~> expected_ty
+-- See Note [Skolemisation] for the differences between
+-- tcSkolemiseCompleteSig and tcTopSkolemise
+
+tcSkolemiseCompleteSig (CSig { sig_bndr = poly_id, sig_ctxt = ctxt, sig_loc = loc })
+ thing_inside
+ = do { cur_loc <- getSrcSpanM
+ ; let poly_ty = idType poly_id
+ ; setSrcSpan loc $ -- Sets the location for the implication constraint
+ tcSkolemiseGeneral Shallow ctxt poly_ty poly_ty $ \tv_prs rho_ty ->
+ setSrcSpan cur_loc $ -- Revert to the original location
+ tcExtendNameTyVarEnv (map (fmap binderVar) tv_prs) $
+ thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty }
+
+tcSkolemiseExpectedType :: TcSigmaType
+ -> ([ExpPatType] -> TcRhoType -> TcM result)
+ -> TcM (HsWrapper, result)
+-- Just like tcSkolemiseCompleteSig, except that we don't have a user-written
+-- type signature, we only have a type comimg from the context.
+-- Eg. f :: (forall a. blah) -> blah
+-- In the call (f e) we will call tcSkolemiseExpectedType on (forall a.blah)
+-- before typececking `e`
+tcSkolemiseExpectedType exp_ty thing_inside
+ = tcSkolemiseGeneral Shallow GenSigCtxt exp_ty exp_ty $ \tv_prs rho_ty ->
+ thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty
+
+tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType
+ -> (TcRhoType -> TcM result)
+ -> TcM (HsWrapper, result)
+tcSkolemise ds_flag ctxt expected_ty thing_inside
+ = tcSkolemiseGeneral ds_flag ctxt expected_ty expected_ty $ \_ rho_ty ->
+ thing_inside rho_ty
+
+checkConstraints :: SkolemInfoAnon
+ -> [TcTyVar] -- Skolems
+ -> [EvVar] -- Given
+ -> TcM result
+ -> TcM (TcEvBinds, result)
+-- checkConstraints is careful to build an implication even if
+-- `skol_tvs` and `given` are both empty, under certain circumstances
+-- See Note [When to build an implication]
+checkConstraints skol_info skol_tvs given thing_inside
+ = do { implication_needed <- implicationNeeded skol_info skol_tvs given
+
+ ; if implication_needed
+ then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+ ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
+ ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
+ ; emitImplications implics
+ ; return (ev_binds, result) }
+
+ else -- Fast path. We check every function argument with tcCheckPolyExpr,
+ -- which uses tcTopSkolemise and hence checkConstraints.
+ -- So this fast path is well-exercised
+ do { res <- thing_inside
+ ; return (emptyTcEvBinds, res) } }
+
+checkTvConstraints :: SkolemInfo
+ -> [TcTyVar] -- Skolem tyvars
+ -> TcM result
+ -> TcM result
+
+checkTvConstraints skol_info skol_tvs thing_inside
+ = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
+ ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
+ ; return result }
+
+emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
+ -> TcLevel -> WantedConstraints -> TcM ()
+emitResidualTvConstraint skol_info skol_tvs tclvl wanted
+ | not (isEmptyWC wanted) ||
+ checkTelescopeSkol skol_info_anon
+ = -- checkTelescopeSkol: in this case, /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] in
+ -- GHC.Tc.Gen.HsType
+ do { implic <- buildTvImplication skol_info_anon skol_tvs tclvl wanted
+ ; emitImplication implic }
+
+ | otherwise -- Empty 'wanted', emit nothing
+ = return ()
+ where
+ skol_info_anon = getSkolemInfo skol_info
+
+buildTvImplication :: SkolemInfoAnon -> [TcTyVar]
+ -> TcLevel -> WantedConstraints -> TcM Implication
+buildTvImplication skol_info skol_tvs tclvl wanted
+ = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
+ do { ev_binds <- newNoTcEvBinds -- Used for equalities only, so all the constraints
+ -- are solved by filling in coercion holes, not
+ -- by creating a value-level evidence binding
+ ; implic <- newImplication
+
+ ; let implic' = implic { ic_tclvl = tclvl
+ , ic_skols = skol_tvs
+ , ic_given_eqs = NoGivenEqs
+ , ic_wanted = wanted
+ , ic_binds = ev_binds
+ , ic_info = skol_info }
+
+ ; checkImplicationInvariants implic'
+ ; return implic' }
+
+implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
+-- See Note [When to build an implication]
+implicationNeeded skol_info skol_tvs given
+ | null skol_tvs
+ , null given
+ , not (alwaysBuildImplication skol_info)
+ = -- Empty skolems and givens
+ do { tc_lvl <- getTcLevel
+ ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
+ then return False -- already inside an implication
+ else
+ do { dflags <- getDynFlags -- If any deferral can happen,
+ -- we must build an implication
+ ; return (gopt Opt_DeferTypeErrors dflags ||
+ gopt Opt_DeferTypedHoles dflags ||
+ gopt Opt_DeferOutOfScopeVariables dflags) } }
+
+ | otherwise -- Non-empty skolems or givens
+ = return True -- Definitely need an implication
+
+alwaysBuildImplication :: SkolemInfoAnon -> Bool
+-- See Note [When to build an implication]
+alwaysBuildImplication _ = False
+
+{- Commmented out for now while I figure out about error messages.
+ See #14185
+
+alwaysBuildImplication (SigSkol ctxt _ _)
+ = case ctxt of
+ FunSigCtxt {} -> True -- RHS of a binding with a signature
+ _ -> False
+alwaysBuildImplication (RuleSkol {}) = True
+alwaysBuildImplication (InstSkol {}) = True
+alwaysBuildImplication (FamInstSkol {}) = True
+alwaysBuildImplication _ = False
+-}
+
+buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar]
+ -> [EvVar] -> WantedConstraints
+ -> TcM (Bag Implication, TcEvBinds)
+buildImplicationFor tclvl skol_info skol_tvs given wanted
+ | isEmptyWC wanted && null given
+ -- Optimisation : if there are no wanteds, and no givens
+ -- don't generate an implication at all.
+ -- Reason for the (null given): we don't want to lose
+ -- the "inaccessible alternative" error check
+ = return (emptyBag, emptyTcEvBinds)
+
+ | otherwise
+ = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
+ -- Why allow TyVarTvs? Because implicitly declared kind variables in
+ -- non-CUSK type declarations are TyVarTvs, and we need to bring them
+ -- into scope as a skolem in an implication. This is OK, though,
+ -- because TyVarTvs will always remain tyvars, even after unification.
+ do { ev_binds_var <- newTcEvBinds
+ ; implic <- newImplication
+ ; let implic' = implic { ic_tclvl = tclvl
+ , ic_skols = skol_tvs
+ , ic_given = given
+ , ic_wanted = wanted
+ , ic_binds = ev_binds_var
+ , ic_info = skol_info }
+ ; checkImplicationInvariants implic'
+
+ ; return (unitBag implic', TcEvBinds ev_binds_var) }
+
+{- Note [When to build an implication]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have some 'skolems' and some 'givens', and we are
+considering whether to wrap the constraints in their scope into an
+implication. We must /always/ do so if either 'skolems' or 'givens' are
+non-empty. But what if both are empty? You might think we could
+always drop the implication. Other things being equal, the fewer
+implications the better. Less clutter and overhead. But we must
+take care:
+
+* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
+ we'll make a /term-level/ evidence binding for 'g = error "blah"'.
+ We must have an EvBindsVar those bindings!, otherwise they end up as
+ top-level unlifted bindings, which are verboten. This only matters
+ at top level, so we check for that
+ See also Note [Deferred errors for coercion holes] in GHC.Tc.Errors.
+ cf #14149 for an example of what goes wrong.
+
+* This is /necessary/ for top level but may be /desirable/ even for
+ nested bindings, because if the deferred coercion is bound too far
+ out it will be reported even if that thunk (say) is not evaluated.
+
+* If you have
+ f :: Int; f = f_blah
+ g :: Bool; g = g_blah
+ If we don't build an implication for f or g (no tyvars, no givens),
+ the constraints for f_blah and g_blah are solved together. And that
+ can yield /very/ confusing error messages, because we can get
+ [W] C Int b1 -- from f_blah
+ [W] C Int b2 -- from g_blan
+ and fundeps can yield [W] b1 ~ b2, even though the two functions have
+ literally nothing to do with each other. #14185 is an example.
+ Building an implication keeps them separate.
+
Note [Herald for matchExpectedFunTys]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The 'herald' always looks like:
@@ -374,62 +752,108 @@ matchExpectedFunTys :: forall a.
ExpectedFunTyOrigin -- See Note [Herald for matchExpectedFunTys]
-> UserTypeCtxt
-> Arity
- -> ExpRhoType -- Skolemised
+ -> ExpSigmaType
-> ([ExpPatType] -> ExpRhoType -> TcM a)
-> TcM (HsWrapper, a)
-- If matchExpectedFunTys n ty = (wrap, _)
-- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty,
-- where [t1, ..., tn], ty_r are passed to the thing_inside
-matchExpectedFunTys herald ctx arity orig_ty thing_inside
- = case orig_ty of
- Check ty -> go [] arity ty
- _ -> defer [] arity orig_ty
+--
+-- Unconditionally concludes by skolemising any trailing invisible
+-- binders and, if DeepSubsumption is on, it does so deeply.
+--
+-- Postcondition:
+-- If exp_ty is Check {}, then [ExpPatType] and ExpRhoType results are all Check{}
+-- If exp_ty is Infer {}, then [ExpPatType] and ExpRhoType results are all Infer{}
+matchExpectedFunTys herald _ arity (Infer inf_res) thing_inside
+ = do { arg_tys <- mapM (new_infer_arg_ty herald) [1 .. arity]
+ ; res_ty <- newInferExpType
+ ; result <- thing_inside (map ExpFunPatTy arg_tys) res_ty
+ ; arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) arg_tys
+ ; res_ty <- readExpType res_ty
+ ; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res
+ ; return (mkWpCastN co, result) }
+
+matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
+ = check 0 [] top_ty
where
- -- Skolemise any /invisible/ foralls /before/ the zero-arg case
- -- so that we guarantee to return a rho-type
- go acc_arg_tys n ty
- | (tvs, theta, _) <- tcSplitSigmaTy ty -- Invisible binders only!
- , not (null tvs && null theta) -- Visible ones handled below
- = do { (wrap_gen, (wrap_res, result)) <- tcTopSkolemise ctx ty $ \ty' ->
- go acc_arg_tys n ty'
+ check :: Arity -> [ExpPatType] -> TcSigmaType -> TcM (HsWrapper, a)
+ -- `check` is called only in the Check{} case
+ -- It collects rev_pat_tys in reversed order
+ -- n_so_far is the number of /visible/ arguments seen so far:
+ -- i.e. length (filterOut isExpForAllPatTyInvis rev_pat_tys)
+
+ -- Do shallow skolemisation if there are top-level invisible quantifiers
+ check n_so_far rev_pat_tys ty
+ | isSigmaTy ty -- Type has invisible quantifiers
+ = do { (wrap_gen, (wrap_res, result))
+ <- tcSkolemiseGeneral Shallow ctx top_ty ty $ \tv_bndrs ty' ->
+ let rev_pat_tys' = reverse (map (mkInvisExpPatType . snd) tv_bndrs)
+ ++ rev_pat_tys
+ in check n_so_far rev_pat_tys' ty'
; return (wrap_gen <.> wrap_res, result) }
- -- No more args; do this /before/ coreView, so
- -- that we do not unnecessarily unwrap synonyms
- go acc_arg_tys 0 rho_ty
- = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType rho_ty)
- ; return (idHsWrapper, result) }
-
- go acc_arg_tys n ty
- | Just ty' <- coreView ty = go acc_arg_tys n ty'
+ -- (n_so_far == arity): no more args
+ -- rho_ty has no top-level quantifiers
+ -- If there is deep subsumption, do deep skolemisation
+ check n_so_far rev_pat_tys rho_ty
+ | n_so_far == arity
+ = do { let pat_tys = reverse rev_pat_tys
+ ; ds_flag <- getDeepSubsumptionFlag
+ ; case ds_flag of
+ Shallow -> do { res <- thing_inside pat_tys (mkCheckExpType rho_ty)
+ ; return (idHsWrapper, res) }
+ Deep -> tcSkolemiseGeneral Deep ctx top_ty rho_ty $ \_ rho_ty ->
+ -- "_" drop the /deeply/-skolemise binders
+ -- They do not line up with binders in the Match
+ thing_inside pat_tys (mkCheckExpType rho_ty) }
+
+ -- NOW do coreView. We didn't do it before, so that we do not unnecessarily
+ -- unwrap a synonym in the returned rho_ty
+ check n_so_far rev_pat_tys ty
+ | Just ty' <- coreView ty = check n_so_far rev_pat_tys ty'
-- Decompose /visible/ (forall a -> blah), to give an ExpForAllPat
-- NB: invisible binders are handled by tcSplitSigmaTy/tcTopSkolemise above
-- NB: visible foralls "count" for the Arity argument; they correspond
-- to syntactically visible patterns in the source program
-- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
- go acc_arg_tys n ty
- | Just (Bndr tv vis, ty') <- splitForAllForAllTyBinder_maybe ty
- , Required <- vis
- = let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
- in goVdq init_subst acc_arg_tys n ty tv ty'
+ check n_so_far rev_pat_tys ty
+ | Just (Bndr tv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty
+ = assertPpr (isVisibleForAllTyFlag vis) (ppr ty) $
+ -- isSigmaTy case above has dealt with /invisible/ quantifiers,
+ -- so this one must be /visible/ (= Required)
+ do { let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
+ -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+ -- in GHC.Tc.Utils.TcType
+ ; rec { (subst', [tv']) <- tcInstSkolTyVarsX skol_info init_subst [tv]
+ ; let tv_prs = [(tyVarName tv, tv')]
+ ; skol_info <- mkSkolemInfo (SigSkol ctx top_ty tv_prs) }
+ ; let body_ty' = substTy subst' body_ty
+ pat_ty = ExpForAllPatTy (mkForAllTyBinder Required tv')
+ ; (ev_binds, (wrap_res, result)) <- checkConstraints (getSkolemInfo skol_info) [tv'] [] $
+ check (n_so_far+1) (pat_ty : rev_pat_tys) body_ty'
+ ; let wrap_gen = mkWpVisTyLam tv' body_ty' <.> mkWpLet ev_binds
+ ; return (wrap_gen <.> wrap_res, result) }
- go acc_arg_tys n (FunTy { ft_af = af, ft_mult = mult, ft_arg = arg_ty, ft_res = res_ty })
+ check n_so_far rev_pat_tys (FunTy { ft_af = af, ft_mult = mult
+ , ft_arg = arg_ty, ft_res = res_ty })
= assert (isVisibleFunArg af) $
- do { let arg_pos = 1 + length acc_arg_tys -- for error messages only
+ do { let arg_pos = n_so_far + 1
; (arg_co, arg_ty) <- hasFixedRuntimeRep (FRRExpectedFunTy herald arg_pos) arg_ty
- ; (wrap_res, result) <- go ((ExpFunPatTy $ Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys)
- (n-1) res_ty
+ ; (wrap_res, result) <- check arg_pos
+ (mkCheckExpFunPatTy (Scaled mult arg_ty) : rev_pat_tys)
+ res_ty
; let wrap_arg = mkWpCastN arg_co
fun_wrap = mkWpFun wrap_arg wrap_res (Scaled mult arg_ty) res_ty
; return (fun_wrap, result) }
- go acc_arg_tys n ty@(TyVarTy tv)
+ check n_so_far rev_pat_tys ty@(TyVarTy tv)
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
- Indirect ty' -> go acc_arg_tys n ty'
- Flexi -> defer acc_arg_tys n (mkCheckExpType ty) }
+ Indirect ty' -> check n_so_far rev_pat_tys ty'
+ Flexi -> defer n_so_far rev_pat_tys ty }
-- In all other cases we bale out into ordinary unification
-- However unlike the meta-tyvar case, we are sure that the
@@ -446,74 +870,51 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
--
-- But in that case we add specialized type into error context
-- anyway, because it may be useful. See also #9605.
- go acc_arg_tys n ty = addErrCtxtM (mk_ctxt acc_arg_tys ty) $
- defer acc_arg_tys n (mkCheckExpType ty)
-
- goVdq subst acc_arg_tys n expected_ty tv ty =
- do { rec { (subst', [tv']) <- tcInstSkolTyVarsX skol_info subst [tv]
- ; let tv_prs = [(tyVarName tv, tv')]
- ; skol_info <- mkSkolemInfo (SigSkol ctx expected_ty tv_prs) }
- ; let ty' = substTy subst' ty
- ; (ev_binds, (wrap_res, result)) <-
- checkConstraints (getSkolemInfo skol_info) [tv'] [] $
- go (ExpForAllPatTy tv' : acc_arg_tys) (n - 1) ty'
- ; let wrap_gen = mkWpVisTyLam tv' ty' <.> mkWpLet ev_binds
- ; return (wrap_gen <.> wrap_res, result) }
+ check n_so_far rev_pat_tys res_ty
+ = addErrCtxtM (mkFunTysMsg herald (arity, top_ty)) $
+ defer n_so_far rev_pat_tys res_ty
------------
- defer :: [ExpPatType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a)
- defer acc_arg_tys n fun_ty
- = do { let last_acc_arg_pos = length acc_arg_tys
- ; more_arg_tys <- mapM new_exp_arg_ty [last_acc_arg_pos + 1 .. last_acc_arg_pos + n]
- ; res_ty <- newInferExpType
- ; result <- thing_inside (reverse acc_arg_tys ++ map ExpFunPatTy more_arg_tys) res_ty
- ; more_arg_tys <- mapM (\(Scaled m t) -> Scaled m <$> readExpType t) more_arg_tys
- ; res_ty <- readExpType res_ty
- ; let unif_fun_ty = mkScaledFunTys more_arg_tys res_ty
- ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty
- -- Not a good origin at all :-(
- ; return (wrap, result) }
-
- new_exp_arg_ty :: Int -> TcM (Scaled ExpSigmaTypeFRR)
- new_exp_arg_ty arg_pos -- position for error messages only
- = mkScaled <$> newFlexiTyVarTy multiplicityTy
- <*> newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
+ defer :: Arity -> [ExpPatType] -> TcRhoType -> TcM (HsWrapper, a)
+ defer n_so_far rev_pat_tys fun_ty
+ = do { more_arg_tys <- mapM (new_check_arg_ty herald) [n_so_far + 1 .. arity]
+ ; let all_pats = reverse rev_pat_tys ++ map mkCheckExpFunPatTy more_arg_tys
+ ; res_ty <- newOpenFlexiTyVarTy
+ ; result <- thing_inside all_pats (mkCheckExpType res_ty)
- ------------
- mk_ctxt :: [ExpPatType] -> TcType -> TidyEnv -> ZonkM (TidyEnv, SDoc)
- mk_ctxt arg_tys res_ty env
- = mkFunTysMsg env herald arg_tys' res_ty arity
- where
- arg_tys' = map prepare_arg_ty (reverse arg_tys)
- prepare_arg_ty (ExpFunPatTy (Scaled u v)) = Anon (Scaled u (checkingExpType "matchExpectedFunTys" v)) visArgTypeLike
- prepare_arg_ty (ExpForAllPatTy tv) = Named (Bndr tv Required)
- -- this is safe b/c we're called from "go"
-
-mkFunTysMsg :: TidyEnv
- -> ExpectedFunTyOrigin
- -> [PiTyBinder] -- only visible quantifiers `t1 -> t2` and `forall (x :: t1) -> t2`
- -> TcType
- -> Arity
- -> ZonkM (TidyEnv, SDoc)
-mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
- = do { (env', fun_ty) <- zonkTidyTcType env $
- mkPiTys arg_tys res_ty
-
- ; let (all_arg_tys, _) =
- -- No invisible quantifiers here (neither `ctx => t` nor `forall x. t`)
- -- because `mkFunTysMsg` never gets those as input in the first place,
- -- so there is no need to filter them out.
- splitPiTys fun_ty
+ ; co <- unifyType Nothing (mkScaledFunTys more_arg_tys res_ty) fun_ty
+ ; return (mkWpCastN co, result) }
+
+new_infer_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled ExpSigmaTypeFRR)
+new_infer_arg_ty herald arg_pos -- position for error messages only
+ = do { mult <- newFlexiTyVarTy multiplicityTy
+ ; inf_hole <- newInferExpTypeFRR (FRRExpectedFunTy herald arg_pos)
+ ; return (mkScaled mult inf_hole) }
+
+new_check_arg_ty :: ExpectedFunTyOrigin -> Int -> TcM (Scaled TcType)
+new_check_arg_ty herald arg_pos -- Position for error messages only
+ = do { mult <- newFlexiTyVarTy multiplicityTy
+ ; arg_ty <- newOpenFlexiFRRTyVarTy (FRRExpectedFunTy herald arg_pos)
+ ; return (mkScaled mult arg_ty) }
+
+mkFunTysMsg :: ExpectedFunTyOrigin
+ -> (Arity, TcType)
+ -> TidyEnv -> ZonkM (TidyEnv, SDoc)
+-- See Note [Reporting application arity errors]
+mkFunTysMsg herald (n_val_args_in_call, fun_ty) env
+ = do { (env', fun_ty) <- zonkTidyTcType env fun_ty
+
+ ; let (pi_ty_bndrs, _) = splitPiTys fun_ty
-- `all_arg_tys` contains visible quantifiers only, so their number matches
-- the number of arguments that the user needs to pass to the function.
- n_fun_args = length all_arg_tys
+ n_fun_args = count isVisiblePiTyBinder pi_ty_bndrs
msg | n_val_args_in_call <= n_fun_args -- Enough args, in the end
= text "In the result of a function call"
| otherwise
= hang (full_herald <> comma)
- 2 (sep [ text "but its type" <+> quotes (pprType fun_ty)
+ 2 (sep [ text "but its type" <+> quotes (pprSigmaType fun_ty)
, if n_fun_args == 0 then text "has none"
else text "has only" <+> speakN n_fun_args])
@@ -522,7 +923,44 @@ mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call
full_herald = pprExpectedFunTyHerald herald
<+> speakNOf n_val_args_in_call (text "value argument")
-----------------------
+
+{- Note [Reporting application arity errors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider f :: Int -> Int -> Int
+and the call foo = f 3 4 5
+We'd like to get an error like:
+
+ • Couldn't match expected type ‘t0 -> t’ with actual type ‘Int’
+ • The function ‘f’ is applied to three value arguments,
+ but its type ‘Int -> Int -> Int’ has only two
+
+That is what `mkFunTysMsg` tries to do. But what is the "type of the function".
+Most obviously, we can report its full, polymorphic type; that is simple and
+explicable. But sometimes a bit odd. Consider
+ f :: Bool -> t Int Int
+ foo = f True 5 10
+We get this error:
+ • Couldn't match type ‘Int’ with ‘t0 -> t’
+ Expected: Int -> t0 -> t
+ Actual: Int -> Int
+ • The function ‘f’ is applied to three value arguments,
+ but its type ‘Bool -> t Int Int’ has only one
+
+That's not /quite/ right beause we can instantiate `t` to an arrow and get
+two arrows (but not three!). With that in mind, one could consider reporting
+the /instantiated/ type, and GHC used to do so. But it's more work, and in
+some ways more confusing, especially when nested quantifiers are concerned, e.g.
+ f :: Bool -> forall t. t Int Int
+
+So we just keep it simple and report the original function type.
+
+
+************************************************************************
+* *
+ Other matchExpected functions
+* *
+********************************************************************* -}
+
matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType)
-- Special case for lists
matchExpectedListTy exp_ty
@@ -902,8 +1340,8 @@ tcSubTypeDS :: HsExpr GhcRn
-- Only one call site, in GHC.Tc.Gen.App.tcApp
tcSubTypeDS rn_expr act_rho res_ty
= case res_ty of
- Check exp_rho -> tc_sub_type_deep (unifyType m_thing) orig
- GenSigCtxt act_rho exp_rho
+ Check exp_rho -> tc_sub_type_ds Deep (unifyType m_thing) orig
+ GenSigCtxt act_rho exp_rho
Infer inf_res -> do { co <- fillInferResult act_rho inf_res
; return (mkWpCastN co) }
@@ -944,9 +1382,9 @@ tcSubTypeAmbiguity :: UserTypeCtxt -- Where did this type arise
-> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- See Note [Ambiguity check and deep subsumption]
tcSubTypeAmbiguity ctxt ty_actual ty_expected
- = tc_sub_type_shallow (unifyType Nothing)
- (AmbiguityCheckOrigin ctxt)
- ctxt ty_actual ty_expected
+ = tc_sub_type_ds Shallow (unifyType Nothing)
+ (AmbiguityCheckOrigin ctxt)
+ ctxt ty_actual ty_expected
---------------
addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a
@@ -1007,13 +1445,12 @@ command. See Note [Implementing :type] in GHC.Tc.Module.
-}
---------------
-tc_sub_type, tc_sub_type_deep, tc_sub_type_shallow
- :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
- -> CtOrigin -- Used when instantiating
- -> UserTypeCtxt -- Used when skolemising
- -> TcSigmaType -- Actual; a sigma-type
- -> TcSigmaType -- Expected; also a sigma-type
- -> TcM HsWrapper
+tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
+ -> CtOrigin -- Used when instantiating
+ -> UserTypeCtxt -- Used when skolemising
+ -> TcSigmaType -- Actual; a sigma-type
+ -> TcSigmaType -- Expected; also a sigma-type
+ -> TcM HsWrapper
-- Checks that actual_ty is more polymorphic than expected_ty
-- If wrap = tc_sub_type t1 t2
-- => wrap :: t1 ~> t2
@@ -1024,16 +1461,19 @@ tc_sub_type, tc_sub_type_deep, tc_sub_type_shallow
----------------------
tc_sub_type unify inst_orig ctxt ty_actual ty_expected
- = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
- ; if deep_subsumption
- then tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
- else tc_sub_type_shallow unify inst_orig ctxt ty_actual ty_expected
- }
+ = do { ds_flag <- getDeepSubsumptionFlag
+ ; tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected }
----------------------
-tc_sub_type_shallow unify inst_orig ctxt ty_actual ty_expected
+tc_sub_type_ds :: DeepSubsumptionFlag
+ -> (TcType -> TcType -> TcM TcCoercionN)
+ -> CtOrigin -> UserTypeCtxt -> TcSigmaType
+ -> TcSigmaType -> TcM HsWrapper
+-- tc_sub_type_ds is the main subsumption worker function
+-- It takes an explicit DeepSubsumptionFlag
+tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected
| definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
- , definitely_mono_shallow ty_actual
+ , definitely_mono ds_flag ty_actual
= do { traceTc "tc_sub_type (drop to equality)" $
vcat [ text "ty_actual =" <+> ppr ty_actual
, text "ty_expected =" <+> ppr ty_expected ]
@@ -1046,46 +1486,24 @@ tc_sub_type_shallow unify inst_orig ctxt ty_actual ty_expected
, text "ty_expected =" <+> ppr ty_expected ]
; (sk_wrap, inner_wrap)
- <- tcTopSkolemise ctxt ty_expected $ \ sk_rho ->
- do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
- ; cow <- unify rho_a sk_rho
- ; return (mkWpCastN cow <.> wrap) }
+ <- case ds_flag of
+ Shallow -> -- Shallow: skolemise, instantiate and unify
+ tcSkolemise Shallow ctxt ty_expected $ \sk_rho ->
+ do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual
+ ; cow <- unify rho_a sk_rho
+ ; return (mkWpCastN cow <.> wrap) }
+ Deep -> -- Deep: we have co/contra work to do
+ tcSkolemise Deep ctxt ty_expected $ \sk_rho ->
+ tc_sub_type_deep unify inst_orig ctxt ty_actual sk_rho
; return (sk_wrap <.> inner_wrap) }
----------------------
-tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
- | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
- , definitely_mono_deep ty_actual
- = do { traceTc "tc_sub_type_deep (drop to equality)" $
- vcat [ text "ty_actual =" <+> ppr ty_actual
- , text "ty_expected =" <+> ppr ty_expected ]
- ; mkWpCastN <$>
- unify ty_actual ty_expected }
-
- | otherwise -- This is the general case
- = do { traceTc "tc_sub_type_deep (general case)" $
- vcat [ text "ty_actual =" <+> ppr ty_actual
- , text "ty_expected =" <+> ppr ty_expected ]
-
- ; (sk_wrap, inner_wrap)
- <- tcDeeplySkolemise ctxt ty_expected $ \ sk_rho ->
- -- See Note [Deep subsumption]
- tc_sub_type_ds unify inst_orig ctxt ty_actual sk_rho
-
- ; return (sk_wrap <.> inner_wrap) }
-
-definitely_mono_shallow :: TcType -> Bool
-definitely_mono_shallow ty = isRhoTy ty
- -- isRhoTy: no top level forall or (=>)
-
-definitely_mono_deep :: TcType -> Bool
-definitely_mono_deep ty
- | not (definitely_mono_shallow ty) = False
- -- isRhoTy: False means top level forall or (=>)
- | Just (_, res) <- tcSplitFunTy_maybe ty = definitely_mono_deep res
- -- Top level (->)
- | otherwise = True
+definitely_mono :: DeepSubsumptionFlag -> TcType -> Bool
+definitely_mono ds_flag ty
+ = case ds_flag of
+ Shallow -> isRhoTy ty -- isRhoTy: no top level forall or (=>)
+ Deep -> isDeepRhoTy ty -- "deep" version: no nested forall or (=>)
definitely_poly :: TcType -> Bool
-- A very conservative test:
@@ -1201,10 +1619,10 @@ prior to the Simplify Subsumption proposal:
The effects are in these main places:
1. In the subsumption check, tcSubType, we must do deep skolemisation:
- see the call to tcDeeplySkolemise in tc_sub_type_deep
+ see the call to tcSkolemise Deep in tc_sub_type_deep
2. In tcPolyExpr we must do deep skolemisation:
- see the call to tcDeeplySkolemise in tcSkolemiseExpType
+ see the call to tcSkolemise in tcSkolemiseExpType
3. for expression type signatures (e :: ty), and functions with type
signatures (e.g. f :: ty; f = e), we must deeply skolemise the type;
@@ -1294,24 +1712,30 @@ where we eta-expanded that (:). But now foldr expects an argument
with ->{Many} and gets an argument with ->{m1} or ->{m2}, and Lint
complains.
-The easiest solution was to use tcEqMult in tc_sub_type_ds, and
+The easiest solution was to use tcEqMult in tc_sub_type_deep, and
insist on equality. This is only in the DeepSubsumption code anyway.
-}
-tc_sub_type_ds :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
- -> CtOrigin -- Used when instantiating
- -> UserTypeCtxt -- Used when skolemising
- -> TcSigmaType -- Actual; a sigma-type
- -> TcRhoType -- Expected; deeply skolemised
- -> TcM HsWrapper
+data DeepSubsumptionFlag = Deep | Shallow
+
+getDeepSubsumptionFlag :: TcM DeepSubsumptionFlag
+getDeepSubsumptionFlag = do { ds <- xoptM LangExt.DeepSubsumption
+ ; if ds then return Deep else return Shallow }
--- If wrap = tc_sub_type_ds t1 t2
+tc_sub_type_deep :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
+ -> CtOrigin -- Used when instantiating
+ -> UserTypeCtxt -- Used when skolemising
+ -> TcSigmaType -- Actual; a sigma-type
+ -> TcRhoType -- Expected; deeply skolemised
+ -> TcM HsWrapper
+
+-- If wrap = tc_sub_type_deep t1 t2
-- => wrap :: t1 ~> t2
-- Here is where the work actually happens!
-- Precondition: ty_expected is deeply skolemised
-tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
- = do { traceTc "tc_sub_type_ds" $
+tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
+ = do { traceTc "tc_sub_type_deep" $
vcat [ text "ty_actual =" <+> ppr ty_actual
, text "ty_expected =" <+> ppr ty_expected ]
; go ty_actual ty_expected }
@@ -1324,9 +1748,9 @@ tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
= do { lookup_res <- isFilledMetaTyVar_maybe tv_a
; case lookup_res of
Just ty_a' ->
- do { traceTc "tc_sub_type_ds following filled meta-tyvar:"
+ do { traceTc "tc_sub_type_deep following filled meta-tyvar:"
(ppr tv_a <+> text "-->" <+> ppr ty_a')
- ; tc_sub_type_ds unify inst_orig ctxt ty_a' ty_e }
+ ; tc_sub_type_deep unify inst_orig ctxt ty_a' ty_e }
Nothing -> just_unify ty_actual ty_expected }
go ty_a@(FunTy { ft_af = af1, ft_mult = act_mult, ft_arg = act_arg, ft_res = act_res })
@@ -1337,9 +1761,9 @@ tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
else
-- This is where we do the co/contra thing, and generate a WpFun, which in turn
-- causes eta-expansion, which we don't like; hence encouraging NoDeepSubsumption
- do { arg_wrap <- tc_sub_type_deep unify given_orig GenSigCtxt exp_arg act_arg
+ do { arg_wrap <- tc_sub_type_ds Deep unify given_orig GenSigCtxt exp_arg act_arg
-- GenSigCtxt: See Note [Setting the argument context]
- ; res_wrap <- tc_sub_type_ds unify inst_orig ctxt act_res exp_res
+ ; res_wrap <- tc_sub_type_deep unify inst_orig ctxt act_res exp_res
; mult_wrap <- tcEqMult inst_orig act_mult exp_mult
-- See Note [Multiplicity in deep subsumption]
; return (mult_wrap <.>
@@ -1353,7 +1777,7 @@ tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
| let (tvs, theta, _) = tcSplitSigmaTy ty_a
, not (null tvs && null theta)
= do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a
- ; body_wrap <- tc_sub_type_ds unify inst_orig ctxt in_rho ty_e
+ ; body_wrap <- tc_sub_type_deep unify inst_orig ctxt in_rho ty_e
; return (body_wrap <.> in_wrap) }
| otherwise -- Revert to unification
@@ -1370,39 +1794,11 @@ tc_sub_type_ds unify inst_orig ctxt ty_actual ty_expected
just_unify ty_a ty_e = do { cow <- unify ty_a ty_e
; return (mkWpCastN cow) }
-tcDeeplySkolemise
- :: UserTypeCtxt -> TcSigmaType
- -> (TcType -> TcM result)
- -> TcM (HsWrapper, result)
- -- ^ The wrapper has type: spec_ty ~> expected_ty
--- Just like tcTopSkolemise, but calls
--- deeplySkolemise instead of topSkolemise
--- See Note [Deep skolemisation]
-tcDeeplySkolemise ctxt expected_ty thing_inside
- | isTauTy expected_ty -- Short cut for common case
- = do { res <- thing_inside expected_ty
- ; return (idHsWrapper, res) }
- | otherwise
- = do { -- This (unpleasant) rec block allows us to pass skol_info to deeplySkolemise;
- -- but skol_info can't be built until we have tv_prs
- rec { (wrap, tv_prs, given, rho_ty) <- deeplySkolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
-
- ; traceTc "tcDeeplySkolemise" (ppr expected_ty $$ ppr rho_ty $$ ppr tv_prs)
-
- ; let skol_tvs = map snd tv_prs
- ; (ev_binds, result)
- <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- thing_inside rho_ty
-
- ; return (wrap <.> mkWpLet ev_binds, result) }
- -- The ev_binds returned by checkConstraints is very
- -- often empty, in which case mkWpLet is a no-op
-
+-----------------------
deeplySkolemise :: SkolemInfo -> TcSigmaType
-> TcM ( HsWrapper
- , [(Name,TyVar)] -- All skolemised variables
- , [EvVar] -- All "given"s
+ , [(Name,TcInvisTVBinder)] -- All skolemised variables
+ , [EvVar] -- All "given"s
, TcRhoType )
-- See Note [Deep skolemisation]
deeplySkolemise skol_info ty
@@ -1411,13 +1807,15 @@ deeplySkolemise skol_info ty
init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
go subst ty
- | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
+ | Just (arg_tys, bndrs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
= do { let arg_tys' = substScaledTys subst arg_tys
- ; ids1 <- newSysLocalIds (fsLit "dk") arg_tys'
- ; (subst', tvs1) <- tcInstSkolTyVarsX skol_info subst tvs
- ; ev_vars1 <- newEvVars (substTheta subst' theta)
+ ; ids1 <- newSysLocalIds (fsLit "dk") arg_tys'
+ ; (subst', bndrs1) <- tcInstSkolTyVarBndrsX skol_info subst bndrs
+ ; ev_vars1 <- newEvVars (substTheta subst' theta)
; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty'
- ; let tv_prs1 = map tyVarName tvs `zip` tvs1
+ ; let tvs = binderVars bndrs
+ tvs1 = binderVars bndrs1
+ tv_prs1 = map tyVarName tvs `zip` bndrs1
; return ( mkWpEta ids1 (mkWpTyLams tvs1
<.> mkWpEvLams ev_vars1
<.> wrap)
@@ -1436,8 +1834,9 @@ deeplyInstantiate orig ty
init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
go subst ty
- | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
- = do { (subst', tvs') <- newMetaTyVarsX subst tvs
+ | Just (arg_tys, bndrs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
+ = do { let tvs = binderVars bndrs
+ ; (subst', tvs') <- newMetaTyVarsX subst tvs
; let arg_tys' = substScaledTys subst' arg_tys
theta' = substTheta subst' theta
; ids1 <- newSysLocalIds (fsLit "di") arg_tys'
@@ -1451,280 +1850,33 @@ deeplyInstantiate orig ty
; return (idHsWrapper, ty') }
tcDeepSplitSigmaTy_maybe
- :: TcSigmaType -> Maybe ([Scaled TcType], [TyVar], ThetaType, TcSigmaType)
+ :: TcSigmaType -> Maybe ([Scaled TcType], [TcInvisTVBinder], ThetaType, TcSigmaType)
-- Looks for a *non-trivial* quantified type, under zero or more function arrows
-- By "non-trivial" we mean either tyvars or constraints are non-empty
-
tcDeepSplitSigmaTy_maybe ty
- | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
- , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty
- = Just (arg_ty:arg_tys, tvs, theta, rho)
-
- | (tvs, theta, rho) <- tcSplitSigmaTy ty
- , not (null tvs && null theta)
- = Just ([], tvs, theta, rho)
-
- | otherwise = Nothing
-
-
-{- *********************************************************************
-* *
- Generalisation
-* *
-********************************************************************* -}
-
-{- Note [Skolemisation]
-~~~~~~~~~~~~~~~~~~~~~~~
-tcTopSkolemise takes "expected type" and strip off quantifiers to expose the
-type underneath, binding the new skolems for the 'thing_inside'
-The returned 'HsWrapper' has type (specific_ty -> expected_ty).
-
-Note that for a nested type like
- forall a. Eq a => forall b. Ord b => blah
-we still only build one implication constraint
- forall a b. (Eq a, Ord b) => <constraints>
-This is just an optimisation, but it's why we use topSkolemise to
-build the pieces from all the layers, before making a single call
-to checkConstraints.
-
-tcSkolemiseScoped is very similar, but differs in two ways:
-
-* It deals specially with just the outer forall, bringing those type
- variables into lexical scope. To my surprise, I found that doing
- this unconditionally in tcTopSkolemise (i.e. doing it even if we don't
- need to bring the variables into lexical scope, which is harmless)
- caused a non-trivial (1%-ish) perf hit on the compiler.
-
-* It handles deep subumption, wheres tcTopSkolemise never looks under
- function arrows.
-
-* It always calls checkConstraints, even if there are no skolem
- variables at all. Reason: there might be nested deferred errors
- that must not be allowed to float to top level.
- See Note [When to build an implication] below.
--}
-
-tcTopSkolemise, tcSkolemiseScoped
- :: UserTypeCtxt -> TcSigmaType
- -> (TcType -> TcM result)
- -> TcM (HsWrapper, result)
- -- ^ The wrapper has type: spec_ty ~> expected_ty
--- See Note [Skolemisation] for the differences between
--- tcSkolemiseScoped and tcTopSkolemise
-
-tcSkolemiseScoped ctxt expected_ty thing_inside
- = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
- ; let skolemise | deep_subsumption = deeplySkolemise
- | otherwise = topSkolemise
- ; -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
- -- in GHC.Tc.Utils.TcType
- rec { (wrap, tv_prs, given, rho_ty) <- skolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
-
- ; let skol_tvs = map snd tv_prs
- ; (ev_binds, res)
- <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- tcExtendNameTyVarEnv tv_prs $
- thing_inside rho_ty
-
- ; return (wrap <.> mkWpLet ev_binds, res) }
-
-tcTopSkolemise ctxt expected_ty thing_inside
- | isRhoTy expected_ty -- Short cut for common case
- = do { res <- thing_inside expected_ty
- ; return (idHsWrapper, res) }
- | otherwise
- = do { -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
- -- in GHC.Tc.Utils.TcType
- rec { (wrap, tv_prs, given, rho_ty) <- topSkolemise skol_info expected_ty
- ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty tv_prs) }
-
- ; let skol_tvs = map snd tv_prs
- ; (ev_binds, result)
- <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
- thing_inside rho_ty
-
- ; return (wrap <.> mkWpLet ev_binds, result) }
- -- The ev_binds returned by checkConstraints is very
- -- often empty, in which case mkWpLet is a no-op
-
--- | Variant of 'tcTopSkolemise' that takes an ExpType
-tcSkolemiseExpType :: UserTypeCtxt -> ExpSigmaType
- -> (ExpRhoType -> TcM result)
- -> TcM (HsWrapper, result)
-tcSkolemiseExpType _ et@(Infer {}) thing_inside
- = (idHsWrapper, ) <$> thing_inside et
-tcSkolemiseExpType ctxt (Check ty) thing_inside
- = do { deep_subsumption <- xoptM LangExt.DeepSubsumption
- ; let skolemise | deep_subsumption = tcDeeplySkolemise
- | otherwise = tcTopSkolemise
- ; skolemise ctxt ty $ \rho_ty ->
- thing_inside (mkCheckExpType rho_ty) }
-
-checkConstraints :: SkolemInfoAnon
- -> [TcTyVar] -- Skolems
- -> [EvVar] -- Given
- -> TcM result
- -> TcM (TcEvBinds, result)
-
-checkConstraints skol_info skol_tvs given thing_inside
- = do { implication_needed <- implicationNeeded skol_info skol_tvs given
-
- ; if implication_needed
- then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
- ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted
- ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs)
- ; emitImplications implics
- ; return (ev_binds, result) }
-
- else -- Fast path. We check every function argument with tcCheckPolyExpr,
- -- which uses tcTopSkolemise and hence checkConstraints.
- -- So this fast path is well-exercised
- do { res <- thing_inside
- ; return (emptyTcEvBinds, res) } }
-
-checkTvConstraints :: SkolemInfo
- -> [TcTyVar] -- Skolem tyvars
- -> TcM result
- -> TcM result
-
-checkTvConstraints skol_info skol_tvs thing_inside
- = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
- ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted
- ; return result }
-
-emitResidualTvConstraint :: SkolemInfo -> [TcTyVar]
- -> TcLevel -> WantedConstraints -> TcM ()
-emitResidualTvConstraint skol_info skol_tvs tclvl wanted
- | not (isEmptyWC wanted) ||
- checkTelescopeSkol skol_info_anon
- = -- checkTelescopeSkol: in this case, /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] in
- -- GHC.Tc.Gen.HsType
- do { implic <- buildTvImplication skol_info_anon skol_tvs tclvl wanted
- ; emitImplication implic }
-
- | otherwise -- Empty 'wanted', emit nothing
- = return ()
+ = go ty
where
- skol_info_anon = getSkolemInfo skol_info
-
-buildTvImplication :: SkolemInfoAnon -> [TcTyVar]
- -> TcLevel -> WantedConstraints -> TcM Implication
-buildTvImplication skol_info skol_tvs tclvl wanted
- = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
- do { ev_binds <- newNoTcEvBinds -- Used for equalities only, so all the constraints
- -- are solved by filling in coercion holes, not
- -- by creating a value-level evidence binding
- ; implic <- newImplication
-
- ; let implic' = implic { ic_tclvl = tclvl
- , ic_skols = skol_tvs
- , ic_given_eqs = NoGivenEqs
- , ic_wanted = wanted
- , ic_binds = ev_binds
- , ic_info = skol_info }
-
- ; checkImplicationInvariants implic'
- ; return implic' }
-
-implicationNeeded :: SkolemInfoAnon -> [TcTyVar] -> [EvVar] -> TcM Bool
--- See Note [When to build an implication]
-implicationNeeded skol_info skol_tvs given
- | null skol_tvs
- , null given
- , not (alwaysBuildImplication skol_info)
- = -- Empty skolems and givens
- do { tc_lvl <- getTcLevel
- ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
- then return False -- already inside an implication
- else
- do { dflags <- getDynFlags -- If any deferral can happen,
- -- we must build an implication
- ; return (gopt Opt_DeferTypeErrors dflags ||
- gopt Opt_DeferTypedHoles dflags ||
- gopt Opt_DeferOutOfScopeVariables dflags) } }
-
- | otherwise -- Non-empty skolems or givens
- = return True -- Definitely need an implication
-
-alwaysBuildImplication :: SkolemInfoAnon -> Bool
--- See Note [When to build an implication]
-alwaysBuildImplication _ = False
-
-{- Commmented out for now while I figure out about error messages.
- See #14185
-
-alwaysBuildImplication (SigSkol ctxt _ _)
- = case ctxt of
- FunSigCtxt {} -> True -- RHS of a binding with a signature
- _ -> False
-alwaysBuildImplication (RuleSkol {}) = True
-alwaysBuildImplication (InstSkol {}) = True
-alwaysBuildImplication (FamInstSkol {}) = True
-alwaysBuildImplication _ = False
--}
-
-buildImplicationFor :: TcLevel -> SkolemInfoAnon -> [TcTyVar]
- -> [EvVar] -> WantedConstraints
- -> TcM (Bag Implication, TcEvBinds)
-buildImplicationFor tclvl skol_info skol_tvs given wanted
- | isEmptyWC wanted && null given
- -- Optimisation : if there are no wanteds, and no givens
- -- don't generate an implication at all.
- -- Reason for the (null given): we don't want to lose
- -- the "inaccessible alternative" error check
- = return (emptyBag, emptyTcEvBinds)
-
- | otherwise
- = assertPpr (all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs) (ppr skol_tvs) $
- -- Why allow TyVarTvs? Because implicitly declared kind variables in
- -- non-CUSK type declarations are TyVarTvs, and we need to bring them
- -- into scope as a skolem in an implication. This is OK, though,
- -- because TyVarTvs will always remain tyvars, even after unification.
- do { ev_binds_var <- newTcEvBinds
- ; implic <- newImplication
- ; let implic' = implic { ic_tclvl = tclvl
- , ic_skols = skol_tvs
- , ic_given = given
- , ic_wanted = wanted
- , ic_binds = ev_binds_var
- , ic_info = skol_info }
- ; checkImplicationInvariants implic'
-
- ; return (unitBag implic', TcEvBinds ev_binds_var) }
-
-{- Note [When to build an implication]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have some 'skolems' and some 'givens', and we are
-considering whether to wrap the constraints in their scope into an
-implication. We must /always/ so if either 'skolems' or 'givens' are
-non-empty. But what if both are empty? You might think we could
-always drop the implication. Other things being equal, the fewer
-implications the better. Less clutter and overhead. But we must
-take care:
-
-* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
- we'll make a /term-level/ evidence binding for 'g = error "blah"'.
- We must have an EvBindsVar those bindings!, otherwise they end up as
- top-level unlifted bindings, which are verboten. This only matters
- at top level, so we check for that
- See also Note [Deferred errors for coercion holes] in GHC.Tc.Errors.
- cf #14149 for an example of what goes wrong.
-
-* If you have
- f :: Int; f = f_blah
- g :: Bool; g = g_blah
- If we don't build an implication for f or g (no tyvars, no givens),
- the constraints for f_blah and g_blah are solved together. And that
- can yield /very/ confusing error messages, because we can get
- [W] C Int b1 -- from f_blah
- [W] C Int b2 -- from g_blan
- and fundpes can yield [W] b1 ~ b2, even though the two functions have
- literally nothing to do with each other. #14185 is an example.
- Building an implication keeps them separate.
--}
+ go ty | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty
+ , Just (arg_tys, tvs, theta, rho) <- go res_ty
+ = Just (arg_ty:arg_tys, tvs, theta, rho)
+
+ | (tvs, theta, rho) <- tcSplitSigmaTyBndrs ty
+ , not (null tvs && null theta)
+ = Just ([], tvs, theta, rho)
+
+ | otherwise = Nothing
+
+isDeepRhoTy :: TcType -> Bool
+-- True if there are no foralls or (=>) at the top, or nested under
+-- arrows to the right. e.g
+-- forall a. a False
+-- Int -> forall a. a False
+-- (forall a. a) -> Int True
+-- Returns True iff tcDeepSplitSigmaTy_maybe returns Nothing
+isDeepRhoTy ty
+ | not (isRhoTy ty) = False -- Foralls or (=>) at top
+ | Just (_, res) <- tcSplitFunTy_maybe ty = isDeepRhoTy res
+ | otherwise = True -- No forall, (=>), or (->) at top
{-
************************************************************************
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index a8826f595fc5bbbabff52c73fae5936ecaf46b8c..2ec448da50b532c8e861970d5e378e8e28ac52d6 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -288,22 +288,12 @@ checkUserTypeError ctxt ty
| TySynCtxt {} <- ctxt -- Do not complain about TypeError on the
= return () -- RHS of type synonyms. See #20181
+ | Just msg <- deepUserTypeError_maybe ty
+ = do { env0 <- liftZonkM tcInitTidyEnv
+ ; let (env1, tidy_msg) = tidyOpenType env0 msg
+ ; failWithTcM (env1, TcRnUserTypeError tidy_msg) }
| otherwise
- = check ty
- where
- check ty
- | Just msg <- userTypeError_maybe ty = fail_with msg
- | Just (_,t1) <- splitForAllTyCoVar_maybe ty = check t1
- | let (_,tys) = splitAppTys ty = mapM_ check tys
- -- splitAppTys keeps type family applications saturated.
- -- This means we don't go looking for user type errors
- -- inside type family arguments (see #20241).
-
- fail_with :: Type -> TcM ()
- fail_with msg = do { env0 <- liftZonkM tcInitTidyEnv
- ; let (env1, tidy_msg) = tidyOpenType env0 msg
- ; failWithTcM (env1, TcRnUserTypeError tidy_msg)
- }
+ = return ()
{- Note [When we don't check for ambiguity]
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index e14d83962ed99808ef080dc37a9561cc8a3a2ca7..e8f37261f99c6319016086ecdd4129c5e4d05ffd 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -7,6 +7,7 @@
{-# LANGUAGE MultiWayIf, PatternSynonyms #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+{-# LANGUAGE DeriveFunctor #-}
-- |
-- #name_types#
@@ -90,7 +91,7 @@ module GHC.Types.Var (
binderVar, binderVars, binderFlag, binderFlags, binderType,
mkForAllTyBinder, mkForAllTyBinders,
mkTyVarBinder, mkTyVarBinders,
- isTyVarBinder,
+ isVisibleForAllTyBinder, isInvisibleForAllTyBinder, isTyVarBinder,
tyVarSpecToBinder, tyVarSpecToBinders, tyVarReqToBinder, tyVarReqToBinders,
mapVarBndr, mapVarBndrs,
@@ -742,6 +743,12 @@ tyVarReqToBinders = map tyVarReqToBinder
tyVarReqToBinder :: VarBndr a () -> VarBndr a ForAllTyFlag
tyVarReqToBinder (Bndr tv _) = Bndr tv Required
+isVisibleForAllTyBinder :: ForAllTyBinder -> Bool
+isVisibleForAllTyBinder (Bndr _ vis) = isVisibleForAllTyFlag vis
+
+isInvisibleForAllTyBinder :: ForAllTyBinder -> Bool
+isInvisibleForAllTyBinder (Bndr _ vis) = isInvisibleForAllTyFlag vis
+
binderVar :: VarBndr tv argf -> tv
binderVar (Bndr v _) = v
diff --git a/testsuite/tests/driver/T2182.stderr b/testsuite/tests/driver/T2182.stderr
index e850b45df6e22c13dbd554591a2b385b22d894a1..54cc10c595b56a236e8417c52096123a786fc66f 100644
--- a/testsuite/tests/driver/T2182.stderr
+++ b/testsuite/tests/driver/T2182.stderr
@@ -1,24 +1,24 @@
T2182.hs:5:5: error: [GHC-39999]
- • No instance for ‘Show (p1 -> p1)’ arising from a use of ‘show’
+ • No instance for ‘Show (t1 -> t1)’ arising from a use of ‘show’
(maybe you haven't applied a function to enough arguments?)
• In the expression: show (\ x -> x)
In an equation for ‘y’: y = show (\ x -> x)
T2182.hs:6:15: error: [GHC-39999]
- • No instance for ‘Eq (p0 -> p0)’ arising from a use of ‘==’
+ • No instance for ‘Eq (t0 -> t0)’ arising from a use of ‘==’
(maybe you haven't applied a function to enough arguments?)
• In the expression: (\ x -> x) == (\ y -> y)
In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
T2182.hs:5:5: error: [GHC-39999]
- • No instance for ‘Show (p1 -> p1)’ arising from a use of ‘show’
+ • No instance for ‘Show (t1 -> t1)’ arising from a use of ‘show’
(maybe you haven't applied a function to enough arguments?)
• In the expression: show (\ x -> x)
In an equation for ‘y’: y = show (\ x -> x)
T2182.hs:6:15: error: [GHC-39999]
- • No instance for ‘Eq (p0 -> p0)’ arising from a use of ‘==’
+ • No instance for ‘Eq (t0 -> t0)’ arising from a use of ‘==’
(maybe you haven't applied a function to enough arguments?)
• In the expression: (\ x -> x) == (\ y -> y)
In an equation for ‘z’: z = (\ x -> x) == (\ y -> y)
diff --git a/testsuite/tests/indexed-types/should_compile/T10806.stderr b/testsuite/tests/indexed-types/should_compile/T10806.stderr
index e718787275a0a5a637111622f715fe4078911ec9..79183d9d478cd611212e3088627f0b66e00dd39c 100644
--- a/testsuite/tests/indexed-types/should_compile/T10806.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T10806.stderr
@@ -3,7 +3,7 @@ T10806.hs:11:32: error: [GHC-83865]
• Couldn't match expected type: Char -> Bool
with actual type: IO ()
• The function ‘print’ is applied to two value arguments,
- but its type ‘Char -> IO ()’ has only one
+ but its type ‘Show a => a -> IO ()’ has only one
In the expression: print 'x' 'y'
In an equation for ‘triggersLoop’:
triggersLoop (Q _ _) (Q _ _) = print 'x' 'y'
diff --git a/testsuite/tests/indexed-types/should_fail/T8518.stderr b/testsuite/tests/indexed-types/should_fail/T8518.stderr
index e2284caa37325c45b80830a63bdec11bacf98dcb..1e79ce4324a5705a9b9e6be9aad49406f2516e77 100644
--- a/testsuite/tests/indexed-types/should_fail/T8518.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T8518.stderr
@@ -3,7 +3,7 @@ T8518.hs:14:18: error: [GHC-83865]
• Couldn't match expected type: Z c -> B c -> t0
with actual type: F c
• The function ‘rpt’ is applied to four value arguments,
- but its type ‘Int -> c -> F c’ has only two
+ but its type ‘t1 -> t2 -> F t2’ has only two
In the expression: rpt (4 :: Int) c z b
In an equation for ‘callCont’:
callCont c z b
diff --git a/testsuite/tests/rep-poly/T23903.stderr b/testsuite/tests/rep-poly/T23903.stderr
index 72743fa1539078ce67659ccf88b248c877b9a181..ec4ba3b21c9245aed3762aa66b80379e11498483 100644
--- a/testsuite/tests/rep-poly/T23903.stderr
+++ b/testsuite/tests/rep-poly/T23903.stderr
@@ -3,8 +3,8 @@ T23903.hs:21:1: error: [GHC-55287]
• The first pattern in the equation for ‘f’
does not have a fixed runtime representation.
Its type is:
- p0 :: TYPE c0
- Cannot unify ‘Rep a’ with the type variable ‘c0’
+ t0 :: TYPE cx0
+ Cannot unify ‘Rep a’ with the type variable ‘cx0’
because the former is not a concrete ‘RuntimeRep’.
• The equation for ‘f’ has one value argument,
but its type ‘a #-> ()’ has none
diff --git a/testsuite/tests/th/T5358.stderr b/testsuite/tests/th/T5358.stderr
index adf00b5195bf85c1b8ea5c3f1db08c1a812d4b53..efca289b75b307c29da4c3d13cc9aae5cda2cb1f 100644
--- a/testsuite/tests/th/T5358.stderr
+++ b/testsuite/tests/th/T5358.stderr
@@ -1,11 +1,11 @@
T5358.hs:7:1: error: [GHC-83865]
- • Couldn't match expected type ‘Int’ with actual type ‘p1 -> p1’
+ • Couldn't match expected type ‘Int’ with actual type ‘t1 -> t1’
• The equation for ‘t1’ has one value argument,
but its type ‘Int’ has none
T5358.hs:8:1: error: [GHC-83865]
- • Couldn't match expected type ‘Int’ with actual type ‘p0 -> p0’
+ • Couldn't match expected type ‘Int’ with actual type ‘t0 -> t0’
• The equation for ‘t2’ has one value argument,
but its type ‘Int’ has none
diff --git a/testsuite/tests/typecheck/should_fail/T10709b.stderr b/testsuite/tests/typecheck/should_fail/T10709b.stderr
index acd824e2491018797db80fa7566177bbf4f4acd8..e4741ddcc188297a82d2afc7616edcd5e4e1db4e 100644
--- a/testsuite/tests/typecheck/should_fail/T10709b.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10709b.stderr
@@ -1,9 +1,9 @@
T10709b.hs:6:22: error: [GHC-91028]
- • Couldn't match type ‘p1’ with ‘forall a. IO a -> IO a’
- Expected: (p1 -> IO ()) -> IO ()
+ • Couldn't match type ‘t2’ with ‘forall a. IO a -> IO a’
+ Expected: (t2 -> IO ()) -> IO ()
Actual: ((forall a. IO a -> IO a) -> IO ()) -> IO ()
- Cannot instantiate unification variable ‘p1’
+ Cannot instantiate unification variable ‘t2’
with a type involving polytypes: forall a. IO a -> IO a
• In the second argument of ‘(.)’, namely ‘mask’
In the expression: (replicateM 2 . mask) (\ _ -> return ())
@@ -11,10 +11,10 @@ T10709b.hs:6:22: error: [GHC-91028]
x4 = (replicateM 2 . mask) (\ _ -> return ())
T10709b.hs:7:22: error: [GHC-91028]
- • Couldn't match type ‘t0’ with ‘forall a1. IO a1 -> IO a1’
- Expected: (t0 -> IO a) -> IO a
+ • Couldn't match type ‘t1’ with ‘forall a1. IO a1 -> IO a1’
+ Expected: (t1 -> IO a) -> IO a
Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
- Cannot instantiate unification variable ‘t0’
+ Cannot instantiate unification variable ‘t1’
with a type involving polytypes: forall a1. IO a1 -> IO a1
• In the second argument of ‘(.)’, namely ‘mask’
In the expression: (replicateM 2 . mask) (\ x -> undefined x)
@@ -22,10 +22,10 @@ T10709b.hs:7:22: error: [GHC-91028]
x5 = (replicateM 2 . mask) (\ x -> undefined x)
T10709b.hs:8:22: error: [GHC-91028]
- • Couldn't match type ‘p0’ with ‘forall a1. IO a1 -> IO a1’
- Expected: (p0 -> IO a) -> IO a
+ • Couldn't match type ‘t0’ with ‘forall a1. IO a1 -> IO a1’
+ Expected: (t0 -> IO a) -> IO a
Actual: ((forall a1. IO a1 -> IO a1) -> IO a) -> IO a
- Cannot instantiate unification variable ‘p0’
+ Cannot instantiate unification variable ‘t0’
with a type involving polytypes: forall a1. IO a1 -> IO a1
• In the second argument of ‘(.)’, namely ‘mask’
In the expression: (replicateM 2 . mask) (id (\ _ -> undefined))
diff --git a/testsuite/tests/typecheck/should_fail/T12947.stderr b/testsuite/tests/typecheck/should_fail/T12947.stderr
index 299c6f95452e64cc8590cb69165fe694d52c9fd9..12b2c9e24bfe2881f01a81ff1bc914db95db117e 100644
--- a/testsuite/tests/typecheck/should_fail/T12947.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12947.stderr
@@ -1,3 +1,3 @@
T12947.hs:15:14: error: [GHC-88464]
- Data constructor not in scope: ContT :: (p0 -> m0 a0) -> P m a
+ Data constructor not in scope: ContT :: (t0 -> m0 a0) -> P m a
diff --git a/testsuite/tests/typecheck/should_fail/T13902.stderr b/testsuite/tests/typecheck/should_fail/T13902.stderr
index 37ec4b401ba405900f7f48dffcee381c9be0a832..9a274da40755fd1abd7bdda4c6f1fee91234dab6 100644
--- a/testsuite/tests/typecheck/should_fail/T13902.stderr
+++ b/testsuite/tests/typecheck/should_fail/T13902.stderr
@@ -2,6 +2,6 @@
T13902.hs:8:5: error: [GHC-83865]
• Couldn't match expected type ‘t0 -> Int’ with actual type ‘Int’
• The function ‘f’ is applied to two value arguments,
- but its type ‘Int -> Int’ has only one
+ but its type ‘a -> a’ has only one
In the expression: f @Int 42 5
In an equation for ‘g’: g = f @Int 42 5
diff --git a/testsuite/tests/typecheck/should_fail/T18398.stderr b/testsuite/tests/typecheck/should_fail/T18398.stderr
index e9824e5b50615c4683f62891794f88cf88a1683d..397a4a664c5dccd6d7808cce0c139d0c3a5d532c 100644
--- a/testsuite/tests/typecheck/should_fail/T18398.stderr
+++ b/testsuite/tests/typecheck/should_fail/T18398.stderr
@@ -1,12 +1,12 @@
T18398.hs:13:34: error: [GHC-39999]
- • No instance for ‘C Ex p0’ arising from a use of ‘meth’
+ • No instance for ‘C Ex t0’ arising from a use of ‘meth’
• In the expression: meth x y
In a case alternative: MkEx _ -> meth x y
In the expression: case x of MkEx _ -> meth x y
T18398.hs:13:70: error: [GHC-39999]
- • No instance for ‘C Ex p0’ arising from a use of ‘meth’
+ • No instance for ‘C Ex t0’ arising from a use of ‘meth’
• In the expression: meth x z
In a case alternative: MkEx _ -> meth x z
In the expression: case x of MkEx _ -> meth x z
diff --git a/testsuite/tests/typecheck/should_fail/T23427.stderr b/testsuite/tests/typecheck/should_fail/T23427.stderr
index 84d92f8dab0164174eb8098f04fcae14cf05ee41..6126854c1f92128633bf376d30d9e0f12aee99b0 100644
--- a/testsuite/tests/typecheck/should_fail/T23427.stderr
+++ b/testsuite/tests/typecheck/should_fail/T23427.stderr
@@ -1,13 +1,13 @@
T23427.hs:10:7: error: [GHC-39999]
- • Could not deduce ‘C a0’
+ • Could not deduce ‘C t0’
arising when matching required constraints
in a group involving ‘doTail’
from the context: C a
bound by the type signature for:
indent :: forall a. C a => a -> a
at T23427.hs:7:1-23
- The type variable ‘a0’ is ambiguous
+ The type variable ‘t0’ is ambiguous
• In an equation for ‘indent’:
indent n
= doText n
diff --git a/testsuite/tests/typecheck/should_fail/T2714.stderr b/testsuite/tests/typecheck/should_fail/T2714.stderr
index fdb328eb1ce319639e50d81f3d1a82accec92408..89a0561d86bed76e177137948ed7678b12525bf5 100644
--- a/testsuite/tests/typecheck/should_fail/T2714.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2714.stderr
@@ -4,8 +4,8 @@ T2714.hs:8:7: error: [GHC-25897]
Expected: c -> a
Actual: f0 (a -> b) -> f0 b
‘c’ is a rigid type variable bound by
- a type expected by the context:
- forall c. c -> a
+ the type signature for:
+ f :: ((a -> b) -> b) -> forall c. c -> a
at T2714.hs:8:1-13
• In the expression: ffmap x
In an equation for ‘f’: f x = ffmap x
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index 3eb958919f95601998ecd48e2a5c73442e2cf006..c4cea94e5199daf04116a47efcc59d295167adcf 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -7,8 +7,8 @@ T8603.hs:33:17: error: [GHC-18872]
Expected: [a2] -> StateT s RV a0
Actual: t0 ((->) [a1]) (StateT s RV a0)
• The function ‘lift’ is applied to two value arguments,
- but its type ‘([a1] -> StateT s RV a0)
- -> t0 ((->) [a1]) (StateT s RV a0)’
+ but its type ‘(Control.Monad.Trans.Class.MonadTrans t, Monad m) =>
+ m a -> t m a’
has only one
In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3]
In the expression:
diff --git a/testsuite/tests/typecheck/should_fail/T9605.stderr b/testsuite/tests/typecheck/should_fail/T9605.stderr
index 359ebc74fda4b48d298f989bd14fefce0997f0ad..9bb8a11b3ad53e4d2f3ca6751f47796cc65bf752 100644
--- a/testsuite/tests/typecheck/should_fail/T9605.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9605.stderr
@@ -3,7 +3,8 @@ T9605.hs:7:6: error: [GHC-83865]
• Couldn't match type ‘Bool’ with ‘m Bool’
Expected: t0 -> m Bool
Actual: t0 -> Bool
- • In the result of a function call
+ • The function ‘f1’ is applied to one value argument,
+ but its type ‘Monad m => m Bool’ has none
In the expression: f1 undefined
In an equation for ‘f2’: f2 = f1 undefined
• Relevant bindings include f2 :: m Bool (bound at T9605.hs:7:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
index 43aade07be41927800ff1d51c7e4a1a290fe2c0c..baad29fe53c5700ab2cc042ead4dab55e4e0b458 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr
@@ -1,6 +1,6 @@
tcfail140.hs:11:7: error: [GHC-83865]
- • Couldn't match expected type ‘t0 -> t’ with actual type ‘Int’
+ • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
• The function ‘f’ is applied to two value arguments,
but its type ‘Int -> Int’ has only one
In the expression: f 3 9
@@ -8,7 +8,7 @@ tcfail140.hs:11:7: error: [GHC-83865]
• Relevant bindings include bar :: t (bound at tcfail140.hs:11:1)
tcfail140.hs:13:10: error: [GHC-83865]
- • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’
+ • Couldn't match expected type ‘t2 -> t’ with actual type ‘Int’
• The function ‘f’ is applied to two value arguments,
but its type ‘Int -> Int’ has only one
In the expression: 3 `f` 4
@@ -33,6 +33,6 @@ tcfail140.hs:17:8: error: [GHC-27346]
In the expression: ((\ Just x -> x) :: Maybe a -> a) (Just 1)
tcfail140.hs:20:1: error: [GHC-83865]
- • Couldn't match expected type ‘Int’ with actual type ‘p0 -> Bool’
+ • Couldn't match expected type ‘Int’ with actual type ‘t0 -> Bool’
• The equation for ‘g’ has two value arguments,
but its type ‘Int -> Int’ has only one
diff --git a/testsuite/tests/typecheck/should_fail/tcfail175.hs b/testsuite/tests/typecheck/should_fail/tcfail175.hs
index 09e7dc3c9bdb5f6223a5494a5b523f0ea6064669..701737e048bd3dc64e810ca29d313ed9d0e4b0ab 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail175.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail175.hs
@@ -1,7 +1,7 @@
-- Crashed GHC 6.6!
-- #1153
-
+
module ShouldFail where
eval :: Int -> String -> String -> String
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr
index 591855176fe711a985c36abc2c927dac05af13b0..6577f85436996388dc36b5586b74b439a56f7655 100644
--- a/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_match.stderr
@@ -2,8 +2,8 @@
T22326_fail_match.hs:7:4: error: [GHC-25897]
• Couldn't match expected type ‘t’ with actual type ‘Maybe a’
‘t’ is a rigid type variable bound by
- a type expected by the context:
- forall t -> t -> ()
+ the type signature for:
+ f :: forall t -> t -> ()
at T22326_fail_match.hs:7:1-25
• In the pattern: type (Maybe a)
In an equation for ‘f’: f (type (Maybe a)) x = ()
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr
index b313b93601b612c0bb0b8c96e0a0a5f02f00e724..32984f57391b3300a947a19d98c3ef4f444b9b44 100644
--- a/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr
@@ -1,9 +1,9 @@
T22326_fail_n_args.hs:6:1: error: [GHC-25897]
- • Couldn't match expected type ‘b’ with actual type ‘p0 -> a0’
+ • Couldn't match expected type ‘b’ with actual type ‘t0 -> t1’
‘b’ is a rigid type variable bound by
- a type expected by the context:
- forall b -> b
+ the type signature for:
+ f :: a -> forall b -> b
at T22326_fail_n_args.hs:6:1-26
• The equation for ‘f’ has three value arguments,
but its type ‘a -> forall b -> b’ has only two
diff --git a/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr b/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr
index 49deefd8211f03f3592fcb1ad55ef95914e85615..4e6f48c3bbcec601880be66a17945bf63ba602e9 100644
--- a/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr
+++ b/testsuite/tests/vdq-rta/should_fail/T22326_fail_pat.stderr
@@ -2,8 +2,8 @@
T22326_fail_pat.hs:9:4: error: [GHC-25897]
• Couldn't match expected type ‘a’ with actual type ‘Int’
‘a’ is a rigid type variable bound by
- a type expected by the context:
- forall a -> ()
+ the type signature for:
+ f :: forall a -> ()
at T22326_fail_pat.hs:9:1-17
• In the pattern: type Int
In an equation for ‘f’: f (type Int) = ()