From 7730713b747e66c93b4fe45478981a6e2ebfc7e2 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Mon, 15 Feb 2021 22:36:16 +0000
Subject: [PATCH] Unify result type earlier to improve error messages
Ticket #19364 helpfully points out that we do not currently take
advantage of pushing the result type of an application into the
arguments. This makes error messages notably less good.
The fix is rather easy: move the result-type unification step earlier.
It's even a bit more efficient; in the the checking case we now
do one less zonk.
See Note [Unify with expected type before typechecking arguments]
in GHC.Tc.Gen.App
This change generally improves error messages, but it made one worse:
typecheck/should_fail/T16204c. That led me to the realisation that
a good error can be replaced by a less-good one, which provoked
me to change GHC.Tc.Solver.Interact.inertsCanDischarge. It's
explained in the new Note [Combining equalities]
One other refactoring: I discovered that KindEqOrigin didn't need a
Maybe in its type -- a nice simplification.
---
compiler/GHC/Tc/Errors.hs | 17 +-
compiler/GHC/Tc/Gen/App.hs | 164 +++++++++++-------
compiler/GHC/Tc/Gen/Head.hs | 30 ++--
compiler/GHC/Tc/Solver/Interact.hs | 103 ++++++++---
compiler/GHC/Tc/Types/Constraint.hs | 9 +-
compiler/GHC/Tc/Types/Origin.hs | 16 +-
compiler/GHC/Tc/Utils/TcMType.hs | 13 +-
compiler/GHC/Tc/Utils/Unify.hs | 19 +-
testsuite/tests/gadt/T3169.stderr | 13 +-
testsuite/tests/gadt/rw.stderr | 10 +-
.../tests/ghci.debugger/scripts/T14628.stderr | 10 +-
testsuite/tests/ghci/scripts/T10508.stderr | 15 +-
.../should_compile/T12538.stderr | 8 +-
.../indexed-types/should_fail/T15870.stderr | 3 +
.../indexed-types/should_fail/T2544.stderr | 23 ++-
.../indexed-types/should_fail/T2664.stderr | 30 ++--
.../indexed-types/should_fail/T4272.stderr | 13 +-
.../indexed-types/should_fail/T5439.stderr | 3 +-
.../indexed-types/should_fail/T9662.stderr | 2 +-
.../should_fail/Forall1Bad.stderr | 5 +-
.../NamedWildcardExplicitForall.stderr | 8 +-
.../partial-sigs/should_fail/PatBind3.stderr | 9 +-
.../tests/patsyn/should_fail/T15695.stderr | 9 +-
testsuite/tests/th/T10945.stderr | 23 ++-
.../tests/typecheck/should_compile/FD2.stderr | 8 +-
.../typecheck/should_compile/T15368.stderr | 9 +-
.../typecheck/should_compile/T15370.stderr | 15 +-
.../typecheck/should_compile/T2494.stderr | 2 +-
.../tests/typecheck/should_fail/T12648.stderr | 12 +-
.../tests/typecheck/should_fail/T1899.stderr | 12 +-
.../tests/typecheck/should_fail/T19364.hs | 12 ++
.../tests/typecheck/should_fail/T19364.stderr | 8 +
.../tests/typecheck/should_fail/T2688.stderr | 7 +-
.../tests/typecheck/should_fail/T3613.stderr | 9 +-
.../tests/typecheck/should_fail/T3950.stderr | 9 +-
.../should_fail/T6018failclosed2.stderr | 11 +-
.../tests/typecheck/should_fail/T8450.stderr | 10 +-
.../tests/typecheck/should_fail/T9260.stderr | 11 +-
.../tests/typecheck/should_fail/T9774.stderr | 6 +-
testsuite/tests/typecheck/should_fail/all.T | 1 +
.../typecheck/should_fail/tcfail065.stderr | 10 +-
.../typecheck/should_fail/tcfail068.stderr | 19 +-
.../typecheck/should_fail/tcfail103.stderr | 14 +-
.../typecheck/should_fail/tcfail131.stderr | 7 +-
.../typecheck/should_fail/tcfail153.stderr | 9 +-
.../typecheck/should_fail/tcfail179.stderr | 10 +-
.../typecheck/should_fail/tcfail201.stderr | 10 +-
.../should_fail/CaretDiagnostics1.stderr | 43 ++---
48 files changed, 445 insertions(+), 374 deletions(-)
create mode 100644 testsuite/tests/typecheck/should_fail/T19364.hs
create mode 100644 testsuite/tests/typecheck/should_fail/T19364.stderr
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 0e687040e028..82dbd65848eb 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -1901,7 +1901,7 @@ tk_eq_msg ctxt ct ty1 ty2 orig@(TypeEqOrigin { uo_actual = act
count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
tk_eq_msg ctxt ct ty1 ty2
- (KindEqOrigin cty1 mb_cty2 sub_o mb_sub_t_or_k)
+ (KindEqOrigin cty1 cty2 sub_o mb_sub_t_or_k)
= vcat [ headline_eq_msg False ct ty1 ty2
, supplementary_msg ]
where
@@ -1911,17 +1911,15 @@ tk_eq_msg ctxt ct ty1 ty2
supplementary_msg
= sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions ->
- case mb_cty2 of
- Just cty2
- | printExplicitCoercions
- || not (cty1 `pickyEqType` cty2)
- -> vcat [ hang (text "When matching" <+> sub_whats)
- 2 (vcat [ ppr cty1 <+> dcolon <+>
+ if printExplicitCoercions
+ || not (cty1 `pickyEqType` cty2)
+ then vcat [ hang (text "When matching" <+> sub_whats)
+ 2 (vcat [ ppr cty1 <+> dcolon <+>
ppr (tcTypeKind cty1)
, ppr cty2 <+> dcolon <+>
ppr (tcTypeKind cty2) ])
, mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o ]
- _ -> text "When matching the kind of" <+> quotes (ppr cty1)
+ else text "When matching the kind of" <+> quotes (ppr cty1)
tk_eq_msg _ _ _ _ _ = panic "typeeq_mismatch_msg"
@@ -2873,8 +2871,7 @@ relevantBindings want_filtering ctxt ct
-- For *kind* errors, report the relevant bindings of the
-- enclosing *type* equality, because that's more useful for the programmer
; let extra_tvs = case tidy_orig of
- KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
- t1 : maybeToList m_t2
+ KindEqOrigin t1 t2 _ _ -> tyCoVarsOfTypes [t1,t2]
_ -> emptyVarSet
ct_fvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index 29dc16ab077b..cc1411ba901d 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -244,9 +244,13 @@ tcApp works like this:
when in checking mode. This is the shaded part of APP-Downarrow
in Fig 5.
-5. Use tcValArgs to typecheck the value arguments
+5. Use unifyResultType to match up the result type of the call
+ with that expected by the context. See Note [Unify with
+ expected type before typechecking arguments]
-6. After a gruesome special case for tagToEnum, rebuild the result.
+6. Use tcValArgs to typecheck the value arguments
+
+7. After a gruesome special case for tagToEnum, rebuild the result.
Some cases that /won't/ work:
@@ -274,6 +278,34 @@ particular Ids:
the renamer (Note [Handling overloaded and rebindable constructs] in
GHC.Rename.Expr), and we want them to be instantiated impredicatively
so that (f `op`), say, will work OK even if `f` is higher rank.
+
+Note [Unify with expected type before typechecking arguments]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this (#19364)
+ data Pair a b = Pair a b
+ baz :: MkPair Int Bool
+ baz = MkPair "yes" "no"
+
+We instantiate MkPair with `alpha`, `beta`, and push its argument
+types (`alpha` and `beta`) into the arguments ("yes" and "no").
+But if we first unify the result type (Pair alpha beta) with the expected
+type (Pair Int Bool) we will push the much more informative types
+`Int` and `Bool` into the arguments. This makes a difference:
+
+Unify result type /after/ typechecking the args
+ • Couldn't match type ‘[Char]’ with ‘Bool’
+ Expected type: Pair Foo Bar
+ Actual type: Pair [Char] [Char]
+ • In the expression: Pair "yes" "no"
+
+Unify result type /before/ typechecking the args
+ • Couldn't match type ‘[Char]’ with ‘Bool’
+ Expected: Foo
+ Actual: String
+ • In the first argument of ‘Pair’, namely ‘"yes"’
+
+The latter is much better. That is why we call unifyExpectedType
+before tcValArgs.
-}
tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
@@ -288,7 +320,26 @@ tcApp rn_expr exp_res_ty
; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args
-- Quick look at result
- ; quickLookResultType do_ql delta app_res_rho exp_res_ty
+ ; app_res_rho <- if do_ql
+ then quickLookResultType delta app_res_rho exp_res_ty
+ else return app_res_rho
+
+ -- Unify with expected type from the context
+ -- See Note [Unify with expected type before typechecking arguments]
+ --
+ -- perhaps_add_res_ty_ctxt: Inside an expansion, the addFunResCtxt stuff is
+ -- more confusing than helpful because the function at the head isn't in
+ -- the source program; it was added by the renamer. See
+ -- Note [Handling overloaded and rebindable constructs] in GHC.Rename.Expr
+ ; let perhaps_add_res_ty_ctxt thing_inside
+ | insideExpansion fun_ctxt
+ = thing_inside
+ | otherwise
+ = addFunResCtxt rn_fun rn_args app_res_rho exp_res_ty $
+ thing_inside
+
+ ; res_co <- perhaps_add_res_ty_ctxt $
+ unifyExpectedType rn_expr app_res_rho exp_res_ty
; whenDOptM Opt_D_dump_tc_trace $
do { inst_args <- mapM zonkArg inst_args -- Only when tracing
@@ -304,35 +355,13 @@ tcApp rn_expr exp_res_ty
-- Typecheck the value arguments
; tc_args <- tcValArgs do_ql inst_args
- -- Zonk the result type, to ensure that we substitute out
- -- any filled-in instantiation variable before calling tcWrapResultMono
- -- In the Check case, this isn't really necessary, because tcWrapResultMono
- -- just drops to tcUnify; but in the Infer case a filled-in instantiation
- -- variable might perhaps escape into the constraint generator. The safe
- -- thing to do is to any instantaition variables away.
- -- See Note [Instantiation variables are short lived]
- ; app_res_rho <- zonkQuickLook do_ql app_res_rho
-
- -- Special case for tagToEnum#
- ; if isTagToEnum rn_fun
- then tcTagToEnum rn_expr tc_fun fun_ctxt tc_args app_res_rho exp_res_ty
- else
-
- do { -- Reconstruct
- ; let tc_expr = rebuildHsApps tc_fun fun_ctxt tc_args
-
- -- Set a context for the helpful
- -- "Probably cause: f applied to too many args"
- -- But not in generated code, where we don't want
- -- to mention internal (rebindable syntax) function names
- set_res_ctxt thing_inside
- | insideExpansion tc_args
- = thing_inside
- | otherwise
- = addFunResCtxt tc_fun tc_args app_res_rho exp_res_ty thing_inside
+ -- Reconstruct, with special case for tagToEnum#
+ ; tc_expr <- if isTagToEnum rn_fun
+ then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho
+ else return (rebuildHsApps tc_fun fun_ctxt tc_args)
-- Wrap the result
- ; set_res_ctxt $ tcWrapResultMono rn_expr tc_expr app_res_rho exp_res_ty } }
+ ; return (mkHsWrapCo res_co tc_expr) }
--------------------
wantQuickLook :: HsExpr GhcRn -> TcM Bool
@@ -869,18 +898,28 @@ skipQuickLook :: Delta -> LHsExpr GhcRn -> TcM (Delta, EValArg 'TcpInst)
skipQuickLook delta larg = return (delta, ValArg larg)
----------------
-quickLookResultType :: Bool -> Delta -> TcRhoType -> ExpRhoType -> TcM ()
+quickLookResultType :: Delta -> TcRhoType -> ExpRhoType -> TcM TcRhoType
-- This function implements the shaded bit of rule APP-Downarrow in
-- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).
-
-quickLookResultType do_ql delta app_res_rho exp_res_ty
- | do_ql
- , not (isEmptyVarSet delta) -- Optimisation only
- , Just exp_rho <- checkingExpType_maybe exp_res_ty
- -- In checking mode only
- = qlUnify delta app_res_rho exp_rho
- | otherwise
- = return ()
+-- It returns its second argument, but with any variables in Delta
+-- substituted out, so no variables in Delta escape
+
+quickLookResultType delta app_res_rho (Check exp_rho)
+ = -- In checking mode only, do qlUnify with the expected result type
+ do { unless (isEmptyVarSet delta) $ -- Optimisation only
+ qlUnify delta app_res_rho exp_rho
+ ; return app_res_rho }
+
+quickLookResultType _ app_res_rho (Infer {})
+ = zonkTcType app_res_rho
+ -- Zonk the result type, to ensure that we substitute out any
+ -- filled-in instantiation variable before calling
+ -- unifyExpectedType. In the Check case, this isn't necessary,
+ -- because unifyExpectedType just drops to tcUnify; but in the
+ -- Infer case a filled-in instantiation variable (filled in by
+ -- tcInstFun) might perhaps escape into the constraint
+ -- generator. The safe thing to do is to zonk any instantiation
+ -- variables away. See Note [Instantiation variables are short lived]
---------------------
qlUnify :: Delta -> TcType -> TcType -> TcM ()
@@ -1080,8 +1119,7 @@ findNoQuantVars fun_ty args
{- Note [tagToEnum#]
~~~~~~~~~~~~~~~~~~~~
Nasty check to ensure that tagToEnum# is applied to a type that is an
-enumeration TyCon. Unification may refine the type later, but this
-check won't see that, alas. It's crude, because it relies on our
+enumeration TyCon. It's crude, because it relies on our
knowing *now* that the type is ok, which in turn relies on the
eager-unification part of the type checker pushing enough information
here. In theory the Right Thing to do is to have a new form of
@@ -1109,54 +1147,48 @@ isTagToEnum :: HsExpr GhcRn -> Bool
isTagToEnum (HsVar _ (L _ fun_id)) = fun_id `hasKey` tagToEnumKey
isTagToEnum _ = False
-tcTagToEnum :: HsExpr GhcRn
- -> HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
- -> TcRhoType -> ExpRhoType
+tcTagToEnum :: HsExpr GhcTc -> AppCtxt -> [HsExprArg 'TcpTc]
+ -> TcRhoType
-> TcM (HsExpr GhcTc)
-- tagToEnum# :: forall a. Int# -> a
-- See Note [tagToEnum#] Urgh!
-tcTagToEnum expr fun fun_ctxt args app_res_ty res_ty
- | null val_args
- = failWithTc (text "tagToEnum# must appear applied to one argument")
-
- | otherwise
- = do { res_ty <- readExpType res_ty
- ; ty' <- zonkTcType res_ty
+tcTagToEnum tc_fun fun_ctxt tc_args res_ty
+ | [val_arg] <- dropWhile (not . isHsValArg) tc_args
+ = do { res_ty <- zonkTcType res_ty
-- Check that the type is algebraic
- ; case tcSplitTyConApp_maybe ty' of {
- Nothing -> do { addErrTc (mk_error ty' doc1)
+ ; case tcSplitTyConApp_maybe res_ty of {
+ Nothing -> do { addErrTc (mk_error res_ty doc1)
; vanilla_result } ;
Just (tc, tc_args) ->
do { -- Look through any type family
; fam_envs <- tcGetFamInstEnvs
; case tcLookupDataFamInst_maybe fam_envs tc tc_args of {
- Nothing -> do { check_enumeration ty' tc
+ Nothing -> do { check_enumeration res_ty tc
; vanilla_result } ;
Just (rep_tc, rep_args, coi) ->
do { -- coi :: tc tc_args ~R rep_tc rep_args
- check_enumeration ty' rep_tc
+ check_enumeration res_ty rep_tc
; let rep_ty = mkTyConApp rep_tc rep_args
- fun' = mkHsWrap (WpTyApp rep_ty) fun
- expr' = rebuildHsApps fun' fun_ctxt val_args
+ tc_fun' = mkHsWrap (WpTyApp rep_ty) tc_fun
+ tc_expr = rebuildHsApps tc_fun' fun_ctxt [val_arg]
df_wrap = mkWpCastR (mkTcSymCo coi)
- ; return (mkHsWrap df_wrap expr') }}}}}
+ ; return (mkHsWrap df_wrap tc_expr) }}}}}
- where
- val_args = dropWhile (not . isHsValArg) args
+ | otherwise
+ = failWithTc (text "tagToEnum# must appear applied to one value argument")
- vanilla_result
- = do { let expr' = rebuildHsApps fun fun_ctxt args
- ; tcWrapResultMono expr expr' app_res_ty res_ty }
+ where
+ vanilla_result = return (rebuildHsApps tc_fun fun_ctxt tc_args)
check_enumeration ty' tc
| isEnumerationTyCon tc = return ()
| otherwise = addErrTc (mk_error ty' doc2)
doc1 = vcat [ text "Specify the type by giving a type signature"
- , text "e.g. (tagToEnum# x) :: Bool" ]
+ , text "e.g. (tagToEnum# x) :: Bool" ]
doc2 = text "Result type must be an enumeration type"
mk_error :: TcType -> SDoc -> SDoc
@@ -1174,5 +1206,3 @@ tcTagToEnum expr fun fun_ctxt args app_res_ty res_ty
tcExprPrag :: HsPragE GhcRn -> HsPragE GhcTc
tcExprPrag (HsPragSCC x1 src ann) = HsPragSCC x1 src ann
-
-
diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs
index faf5e0f2f2af..5b57f397ce3f 100644
--- a/compiler/GHC/Tc/Gen/Head.hs
+++ b/compiler/GHC/Tc/Gen/Head.hs
@@ -16,9 +16,10 @@
-}
module GHC.Tc.Gen.Head
- ( HsExprArg(..), EValArg(..), TcPass(..), AppCtxt(..), appCtxtLoc
+ ( HsExprArg(..), EValArg(..), TcPass(..)
+ , AppCtxt(..), appCtxtLoc, insideExpansion
, splitHsApps, rebuildHsApps
- , addArgWrap, isHsValArg, insideExpansion
+ , addArgWrap, isHsValArg
, countLeadingValArgs, isVisibleArg, pprHsExprArgTc
, tcInferAppHead, tcInferAppHead_maybe
@@ -204,6 +205,10 @@ appCtxtLoc :: AppCtxt -> SrcSpan
appCtxtLoc (VAExpansion _ l) = l
appCtxtLoc (VACall _ _ l) = l
+insideExpansion :: AppCtxt -> Bool
+insideExpansion (VAExpansion {}) = True
+insideExpansion (VACall {}) = False
+
instance Outputable AppCtxt where
ppr (VAExpansion e _) = text "VAExpansion" <+> ppr e
ppr (VACall f n _) = text "VACall" <+> int n <+> ppr f
@@ -317,12 +322,6 @@ isVisibleArg (EValArg {}) = True
isVisibleArg (ETypeArg {}) = True
isVisibleArg _ = False
-insideExpansion :: [HsExprArg p] -> Bool
-insideExpansion args = any is_expansion args
- where
- is_expansion (EWrap (EExpand {})) = True
- is_expansion _ = False
-
instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where
ppr (EValArg { eva_arg = arg }) = text "EValArg" <+> ppr arg
ppr (EPrag _ p) = text "EPrag" <+> ppr p
@@ -850,9 +849,10 @@ tcCheckId :: Name -> ExpRhoType -> TcM (HsExpr GhcTc)
tcCheckId name res_ty
= do { (expr, actual_res_ty) <- tcInferId name
; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty])
- ; addFunResCtxt expr [] actual_res_ty res_ty $
- tcWrapResultO (OccurrenceOf name) (HsVar noExtField (noLoc name)) expr
- actual_res_ty res_ty }
+ ; addFunResCtxt rn_fun [] actual_res_ty res_ty $
+ tcWrapResultO (OccurrenceOf name) rn_fun expr actual_res_ty res_ty }
+ where
+ rn_fun = HsVar noExtField (noLoc name)
------------------------
tcInferId :: Name -> TcM (HsExpr GhcTc, TcSigmaType)
@@ -1157,13 +1157,15 @@ naughtiness in both branches. c.f. TcTyClsBindings.mkAuxBinds.
* *
********************************************************************* -}
-addFunResCtxt :: HsExpr GhcTc -> [HsExprArg 'TcpTc]
+addFunResCtxt :: HsExpr GhcRn -> [HsExprArg 'TcpRn]
-> TcType -> ExpRhoType
-> TcM a -> TcM a
-- When we have a mis-match in the return type of a function
-- try to give a helpful message about too many/few arguments
-addFunResCtxt fun args fun_res_ty env_ty
- = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg)
+-- But not in generated code, where we don't want
+-- to mention internal (rebindable syntax) function names
+addFunResCtxt fun args fun_res_ty env_ty thing_inside
+ = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg) thing_inside
-- NB: use a landmark error context, so that an empty context
-- doesn't suppress some more useful context
where
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index b8df1fbae673..8474ca7007fa 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -465,11 +465,12 @@ both. (They probably started as [WD] and got split; this is relatively
rare and it doesn't seem worth trying to put them back together again.)
-}
-solveOneFromTheOther :: CtEvidence -- Inert
- -> CtEvidence -- WorkItem
+solveOneFromTheOther :: CtEvidence -- Inert (Dict or Irred)
+ -> CtEvidence -- WorkItem (same predicate as inert)
-> TcS InteractResult
-- Precondition:
-- * inert and work item represent evidence for the /same/ predicate
+-- * Both are CDictCan or CIrredCan
--
-- We can always solve one from the other: even if both are wanted,
-- although we don't rewrite wanteds with wanteds, we can combine
@@ -499,8 +500,8 @@ solveOneFromTheOther ev_i ev_w
-- Inert is Given or Wanted
= case ev_i of
CtWanted { ctev_nosh = WOnly }
- | WDeriv <- nosh_w -> return KeepWork
- _ -> return KeepInert
+ | WDeriv <- nosh_w -> return KeepWork
+ _ -> return KeepInert
-- Consider work item [WD] C ty1 ty2
-- inert item [W] C ty1 ty2
-- Then we must keep the work item. But if the
@@ -511,7 +512,7 @@ solveOneFromTheOther ev_i ev_w
-- From here on the work-item is Given
| CtWanted { ctev_loc = loc_i } <- ev_i
- , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
+ , prohibitedSuperClassSolve loc_w loc_i
= do { traceTcS "prohibitedClassSolve2" (ppr ev_i $$ ppr ev_w)
; return KeepInert } -- Just discard the un-usable Given
-- This never actually happens because
@@ -1439,49 +1440,107 @@ solving.
**********************************************************************
-}
-inertsCanDischarge :: InertCans -> CanEqLHS -> TcType -> CtFlavourRole
+{- Note [Combining equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+ Inert: g1 :: a ~ t
+ Work item: g2 :: a ~ t
+
+Then we can simply solve g2 from g1, thus g2 := g1. Easy!
+But it's not so simple:
+
+* If t is a type variable, the equalties might be oriented differently:
+ e.g. (g1 :: a~b) and (g2 :: b~a)
+ So we look both ways round. Hence the SwapFlag result to
+ inertsCanDischarge.
+
+* We can only do g2 := g1 if g1 can discharge g2; that depends on
+ (a) the role and (b) the flavour. E.g. a representational equality
+ cannot discharge a nominal one; a Wanted cannot discharge a Given.
+ The predicate is eqCanDischargeFR.
+
+* If the inert is [W] and the work-item is [WD] we don't want to
+ forget the [D] part; hence the Bool result of inertsCanDischarge.
+
+* Visibility. Suppose S :: forall k. k -> Type, and consider unifying
+ S @Type (a::Type) ~ S @(Type->Type) (b::Type->Type)
+ From the first argument we get (Type ~ Type->Type); from the second
+ argument we get (a ~ b) which in turn gives (Type ~ Type->Type).
+ See typecheck/should_fail/T16204c.
+
+ That first argument is invisible in the source program (aside from
+ visible type application), so we'd much prefer to get the error from
+ the second. We track visiblity in the uo_visible field of a TypeEqOrigin.
+ We use this to prioritise visible errors (see GHC.Tc.Errors.tryReporters,
+ the partition on isVisibleOrigin).
+
+ So when combining two otherwise-identical equalites, we want to
+ keep the visible one, and discharge the invisible one. Hence the
+ call to strictly_more_visible.
+-}
+
+inertsCanDischarge :: InertCans -> Ct
-> Maybe ( CtEvidence -- The evidence for the inert
, SwapFlag -- Whether we need mkSymCo
, Bool) -- True <=> keep a [D] version
-- of the [WD] constraint
-inertsCanDischarge inerts lhs rhs fr
+inertsCanDischarge inerts (CEqCan { cc_lhs = lhs_w, cc_rhs = rhs_w
+ , cc_ev = ev_w, cc_eq_rel = eq_rel })
| (ev_i : _) <- [ ev_i | CEqCan { cc_ev = ev_i, cc_rhs = rhs_i
, cc_eq_rel = eq_rel }
- <- findEq inerts lhs
- , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
- , rhs_i `tcEqType` rhs ]
+ <- findEq inerts lhs_w
+ , rhs_i `tcEqType` rhs_w
+ , inert_beats_wanted ev_i eq_rel ]
= -- Inert: a ~ ty
-- Work item: a ~ ty
Just (ev_i, NotSwapped, keep_deriv ev_i)
- | Just rhs_lhs <- canEqLHS_maybe rhs
+ | Just rhs_lhs <- canEqLHS_maybe rhs_w
, (ev_i : _) <- [ ev_i | CEqCan { cc_ev = ev_i, cc_rhs = rhs_i
, cc_eq_rel = eq_rel }
<- findEq inerts rhs_lhs
- , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
- , rhs_i `tcEqType` canEqLHSType lhs ]
+ , rhs_i `tcEqType` canEqLHSType lhs_w
+ , inert_beats_wanted ev_i eq_rel ]
= -- Inert: a ~ b
-- Work item: b ~ a
Just (ev_i, IsSwapped, keep_deriv ev_i)
- | otherwise
- = Nothing
-
where
+ loc_w = ctEvLoc ev_w
+ flav_w = ctEvFlavour ev_w
+ fr_w = (flav_w, eq_rel)
+
+ inert_beats_wanted ev_i eq_rel
+ = -- eqCanDischargeFR: see second bullet of Note [Combining equalities]
+ -- strictly_more_visible: see last bullet of Note [Combining equalities]
+ fr_i`eqCanDischargeFR` fr_w
+ && not ((loc_w `strictly_more_visible` ctEvLoc ev_i)
+ && (fr_w `eqCanDischargeFR` fr_i))
+ where
+ fr_i = (ctEvFlavour ev_i, eq_rel)
+
+ -- See Note [Combining equalities], third bullet
keep_deriv ev_i
| Wanted WOnly <- ctEvFlavour ev_i -- inert is [W]
- , (Wanted WDeriv, _) <- fr -- work item is [WD]
+ , Wanted WDeriv <- flav_w -- work item is [WD]
= True -- Keep a derived version of the work item
| otherwise
= False -- Work item is fully discharged
+ -- See Note [Combining equalities], final bullet
+ strictly_more_visible loc1 loc2
+ = not (isVisibleOrigin (ctLocOrigin loc2)) &&
+ isVisibleOrigin (ctLocOrigin loc1)
+
+inertsCanDischarge _ _ = Nothing
+
+
interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
interactEq inerts workItem@(CEqCan { cc_lhs = lhs
- , cc_rhs = rhs
- , cc_ev = ev
- , cc_eq_rel = eq_rel })
- | Just (ev_i, swapped, keep_deriv)
- <- inertsCanDischarge inerts lhs rhs (ctEvFlavour ev, eq_rel)
+ , cc_rhs = rhs
+ , cc_ev = ev
+ , cc_eq_rel = eq_rel })
+ | Just (ev_i, swapped, keep_deriv) <- inertsCanDischarge inerts workItem
= do { setEvBindIfWanted ev $
evCoercion (maybeTcSymCo swapped $
tcDowngradeRole (eqRelRole eq_rel)
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 3862d842b0d9..29344b17d73e 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -1559,10 +1559,9 @@ instance Outputable TcEvDest where
instance Outputable CtEvidence where
ppr ev = ppr (ctEvFlavour ev)
- <+> pp_ev
- <+> braces (ppr (ctl_depth (ctEvLoc ev))) <> dcolon
- -- Show the sub-goal depth too
- <+> ppr (ctEvPred ev)
+ <+> pp_ev <+> braces (ppr (ctl_depth (ctEvLoc ev)))
+ -- Show the sub-goal depth too
+ <> dcolon <+> ppr (ctEvPred ev)
where
pp_ev = case ev of
CtGiven { ctev_evar = v } -> ppr v
@@ -1860,7 +1859,7 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin
mkKindLoc :: TcType -> TcType -- original *types* being compared
-> CtLoc -> CtLoc
mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
- (KindEqOrigin s1 (Just s2) (ctLocOrigin loc)
+ (KindEqOrigin s1 s2 (ctLocOrigin loc)
(ctLocTypeOrKind_maybe loc))
-- | Take a CtLoc and moves it to the kind level
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b0d970bb37d4..648bf5ce12f4 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -361,7 +361,7 @@ data CtOrigin
}
| KindEqOrigin
- TcType (Maybe TcType) -- A kind equality arising from unifying these two types
+ TcType TcType -- A kind equality arising from unifying these two types
CtOrigin -- originally arising from this
(Maybe TypeOrKind) -- the level of the eq this arises from
@@ -559,16 +559,15 @@ pprCtOrigin (FunDepOrigin2 pred1 orig1 pred2 loc2)
, hang (text "instance" <+> quotes (ppr pred2))
2 (text "at" <+> ppr loc2) ])
-pprCtOrigin (KindEqOrigin t1 (Just t2) _ _)
- = hang (ctoHerald <+> text "a kind equality arising from")
- 2 (sep [ppr t1, char '~', ppr t2])
-
pprCtOrigin AssocFamPatOrigin
= text "when matching a family LHS with its class instance head"
-pprCtOrigin (KindEqOrigin t1 Nothing _ _)
- = hang (ctoHerald <+> text "a kind equality when matching")
- 2 (ppr t1)
+pprCtOrigin (TypeEqOrigin { uo_actual = t1, uo_expected = t2, uo_visible = vis })
+ = text "a type equality" <> brackets (ppr vis) <+> sep [ppr t1, char '~', ppr t2]
+
+pprCtOrigin (KindEqOrigin t1 t2 _ _)
+ = hang (ctoHerald <+> text "a kind equality arising from")
+ 2 (sep [ppr t1, char '~', ppr t2])
pprCtOrigin (DerivOriginDC dc n _)
= hang (ctoHerald <+> text "the" <+> speakNth n
@@ -641,7 +640,6 @@ pprCtO DefaultOrigin = text "a 'default' declaration"
pprCtO DoOrigin = text "a do statement"
pprCtO MCompOrigin = text "a statement in a monad comprehension"
pprCtO ProcOrigin = text "a proc expression"
-pprCtO (TypeEqOrigin t1 t2 _ _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2]
pprCtO AnnOrigin = text "an annotation"
pprCtO (ExprHoleOrigin occ) = text "a use of" <+> quotes (ppr occ)
pprCtO (TypeHoleOrigin occ) = text "a use of wildcard" <+> quotes (ppr occ)
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index ed9ee9cc4461..1e82be0f0e99 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -137,7 +137,6 @@ import GHC.Types.Basic ( TypeOrKind(..) )
import Control.Monad
import GHC.Data.Maybe
-import Control.Arrow ( second )
import qualified Data.Semigroup as Semi
{-
@@ -2516,13 +2515,11 @@ zonkTidyOrigin env orig@(TypeEqOrigin { uo_actual = act
; (env2, exp') <- zonkTidyTcType env1 exp
; return ( env2, orig { uo_actual = act'
, uo_expected = exp' }) }
-zonkTidyOrigin env (KindEqOrigin ty1 m_ty2 orig t_or_k)
- = do { (env1, ty1') <- zonkTidyTcType env ty1
- ; (env2, m_ty2') <- case m_ty2 of
- Just ty2 -> second Just <$> zonkTidyTcType env1 ty2
- Nothing -> return (env1, Nothing)
- ; (env3, orig') <- zonkTidyOrigin env2 orig
- ; return (env3, KindEqOrigin ty1' m_ty2' orig' t_or_k) }
+zonkTidyOrigin env (KindEqOrigin ty1 ty2 orig t_or_k)
+ = do { (env1, ty1') <- zonkTidyTcType env ty1
+ ; (env2, ty2') <- zonkTidyTcType env1 ty2
+ ; (env3, orig') <- zonkTidyOrigin env2 orig
+ ; return (env3, KindEqOrigin ty1' ty2' orig' t_or_k) }
zonkTidyOrigin env (FunDepOrigin1 p1 o1 l1 p2 o2 l2)
= do { (env1, p1') <- zonkTidyTcType env p1
; (env2, p2') <- zonkTidyTcType env1 p2
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 121ebfbe7e39..eee4e1844ccd 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -22,7 +22,7 @@ module GHC.Tc.Utils.Unify (
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
-- Various unifications
- unifyType, unifyKind,
+ unifyType, unifyKind, unifyExpectedType,
uType, promoteTcType,
swapOverTyVars, canSolveByUnification,
@@ -543,11 +543,18 @@ tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc
-- It means we don't need to pass in a CtOrigin
tcWrapResultMono rn_expr expr act_ty res_ty
= ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr )
- do { co <- case res_ty of
- Infer inf_res -> fillInferResult act_ty inf_res
- Check exp_ty -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
+ do { co <- unifyExpectedType rn_expr act_ty res_ty
; return (mkHsWrapCo co expr) }
+unifyExpectedType :: HsExpr GhcRn
+ -> TcRhoType -- Actual -- a rho-type not a sigma-type
+ -> ExpRhoType -- Expected
+ -> TcM TcCoercionN
+unifyExpectedType rn_expr act_ty exp_ty
+ = case exp_ty of
+ Infer inf_res -> fillInferResult act_ty inf_res
+ Check exp_ty -> unifyType (Just (ppr rn_expr)) act_ty exp_ty
+
------------------------
tcSubTypePat :: CtOrigin -> UserTypeCtxt
-> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
@@ -1249,7 +1256,7 @@ uType t_or_k origin orig_ty1 orig_ty2
= do { let ty1 = coercionType co1
ty2 = coercionType co2
; kco <- uType KindLevel
- (KindEqOrigin orig_ty1 (Just orig_ty2) origin
+ (KindEqOrigin orig_ty1 orig_ty2 origin
(Just t_or_k))
ty1 ty2
; return $ mkProofIrrelCo Nominal kco co1 co2 }
@@ -1463,7 +1470,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
; defer }
ty1 = mkTyVarTy tv1
- kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k)
+ kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2
diff --git a/testsuite/tests/gadt/T3169.stderr b/testsuite/tests/gadt/T3169.stderr
index 3a5fc99fb337..5770e03c7072 100644
--- a/testsuite/tests/gadt/T3169.stderr
+++ b/testsuite/tests/gadt/T3169.stderr
@@ -1,20 +1,17 @@
-T3169.hs:13:13: error:
+T3169.hs:13:22: error:
• Couldn't match type ‘elt’ with ‘Map b elt’
- Expected: Maybe (Map b elt)
- Actual: Maybe elt
+ Expected: Map a (Map b elt)
+ Actual: Map (a, b) elt
‘elt’ is a rigid type variable bound by
the type signature for:
lookup :: forall elt. (a, b) -> Map (a, b) elt -> Maybe elt
at T3169.hs:12:3-8
- • In the expression: lookup a m :: Maybe (Map b elt)
+ • In the second argument of ‘lookup’, namely ‘m’
+ In the expression: lookup a m :: Maybe (Map b elt)
In the expression:
case lookup a m :: Maybe (Map b elt) of {
Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
- In an equation for ‘lookup’:
- lookup (a, b) (m :: Map (a, b) elt)
- = case lookup a m :: Maybe (Map b elt) of {
- Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt }
• Relevant bindings include
m :: Map (a, b) elt (bound at T3169.hs:12:17)
b :: b (bound at T3169.hs:12:13)
diff --git a/testsuite/tests/gadt/rw.stderr b/testsuite/tests/gadt/rw.stderr
index fe6ba1edee22..c4221368fdba 100644
--- a/testsuite/tests/gadt/rw.stderr
+++ b/testsuite/tests/gadt/rw.stderr
@@ -13,17 +13,17 @@ rw.hs:14:47: error:
v :: T a (bound at rw.hs:13:10)
writeInt :: T a -> IORef a -> IO () (bound at rw.hs:13:1)
-rw.hs:19:43: error:
+rw.hs:19:51: error:
• Couldn't match type ‘a’ with ‘Bool’
- Expected: a -> IO ()
- Actual: Bool -> IO ()
+ Expected: a -> Bool
+ Actual: Bool -> Bool
‘a’ is a rigid type variable bound by
the type signature for:
readBool :: forall a. T a -> IORef a -> IO ()
at rw.hs:16:1-34
- • In the second argument of ‘(>>=)’, namely ‘(print . not)’
+ • In the second argument of ‘(.)’, namely ‘not’
+ In the second argument of ‘(>>=)’, namely ‘(print . not)’
In the expression: readIORef ref >>= (print . not)
- In a case alternative: ~(Lb x) -> readIORef ref >>= (print . not)
• Relevant bindings include
ref :: IORef a (bound at rw.hs:17:12)
v :: T a (bound at rw.hs:17:10)
diff --git a/testsuite/tests/ghci.debugger/scripts/T14628.stderr b/testsuite/tests/ghci.debugger/scripts/T14628.stderr
index fbce771874cc..0eb90fde1f05 100644
--- a/testsuite/tests/ghci.debugger/scripts/T14628.stderr
+++ b/testsuite/tests/ghci.debugger/scripts/T14628.stderr
@@ -1,9 +1,9 @@
-<interactive>:4:7: error:
+<interactive>:4:17: error:
• Couldn't match type ‘m’ with ‘(,) a0’
- Expected: (a0, ((), Int))
- Actual: m ((), Int)
+ Expected: StateT Int ((,) a0) ()
+ Actual: StateT Int m ()
‘m’ is an interactive-debugger skolem
- • In the second argument of ‘($)’, namely ‘runStateT _result 0’
+ • In the first argument of ‘runStateT’, namely ‘_result’
+ In the second argument of ‘($)’, namely ‘runStateT _result 0’
In the expression: snd $ runStateT _result 0
- In an equation for ‘it’: it = snd $ runStateT _result 0
diff --git a/testsuite/tests/ghci/scripts/T10508.stderr b/testsuite/tests/ghci/scripts/T10508.stderr
index f7931e48e2e8..8cbcb2936d63 100644
--- a/testsuite/tests/ghci/scripts/T10508.stderr
+++ b/testsuite/tests/ghci/scripts/T10508.stderr
@@ -1,13 +1,10 @@
-<interactive>:1:8: error:
+<interactive>:1:15: error:
• Couldn't match type: a0 -> a0
with: [Char]
- Expected: IO Prelude.String
- Actual: IO (a0 -> a0)
- • In the expression: return id
+ Expected: Prelude.String
+ Actual: a0 -> a0
+ • Probable cause: ‘id’ is applied to too few arguments
+ In the first argument of ‘return’, namely ‘id’
+ In the expression: return id
In the second argument of ‘(.)’, namely ‘(\ _ -> return id)’
- In the expression:
- (.)
- (GHC.GHCi.ghciStepIO :: IO Prelude.String -> IO Prelude.String)
- (\ _ -> return id) ::
- Prelude.String -> IO Prelude.String
diff --git a/testsuite/tests/indexed-types/should_compile/T12538.stderr b/testsuite/tests/indexed-types/should_compile/T12538.stderr
index 7a26b9c483c0..7de8f787af0a 100644
--- a/testsuite/tests/indexed-types/should_compile/T12538.stderr
+++ b/testsuite/tests/indexed-types/should_compile/T12538.stderr
@@ -3,12 +3,12 @@ T12538.hs:37:8: error:
• Could not deduce: a' ~ Tagged Int a
from the context: (TagImpl a a', b ~ DF a')
bound by the instance declaration at T12538.hs:36:10-46
- Expected: a -> b
- Actual: a -> DF (Tagged Int a)
+ Expected: Tagged Int a -> b
+ Actual: Tagged Int a -> DF (Tagged Int a)
‘a'’ is a rigid type variable bound by
the instance declaration
at T12538.hs:36:10-46
- • In the expression: DF . tag
+ • In the first argument of ‘(.)’, namely ‘DF’
+ In the expression: DF . tag
In an equation for ‘df’: df = DF . tag
- In the instance declaration for ‘ToDF a b’
• Relevant bindings include df :: a -> b (bound at T12538.hs:37:3)
diff --git a/testsuite/tests/indexed-types/should_fail/T15870.stderr b/testsuite/tests/indexed-types/should_fail/T15870.stderr
index ce087941ea07..7968dc3ddaf5 100644
--- a/testsuite/tests/indexed-types/should_fail/T15870.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T15870.stderr
@@ -1,6 +1,9 @@
T15870.hs:32:34: error:
• Couldn't match kind ‘k’ with ‘*’
+ When matching kinds
+ b :: *
+ a :: k
Expected kind ‘Optic a’, but ‘g2’ has kind ‘Optic b’
‘k’ is a rigid type variable bound by
a family instance declaration
diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 721267e75d64..be58f59e05b1 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,13 +1,26 @@
-T2544.hs:19:12: error:
+T2544.hs:19:18: error:
+ • Couldn't match type: IxMap i0
+ with: IxMap l
+ Expected: IxMap l [Int]
+ Actual: IxMap i0 [Int]
+ NB: ‘IxMap’ is a non-injective type family
+ The type variable ‘i0’ is ambiguous
+ • In the first argument of ‘BiApp’, namely ‘empty’
+ In the expression: BiApp empty empty
+ In an equation for ‘empty’: empty = BiApp empty empty
+ • Relevant bindings include
+ empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
+
+T2544.hs:19:24: error:
• Couldn't match type: IxMap i1
with: IxMap r
- Expected: IxMap (l :|: r) [Int]
- Actual: BiApp (IxMap i0) (IxMap i1) [Int]
+ Expected: IxMap r [Int]
+ Actual: IxMap i1 [Int]
NB: ‘IxMap’ is a non-injective type family
The type variable ‘i1’ is ambiguous
- • In the expression: BiApp empty empty
+ • In the second argument of ‘BiApp’, namely ‘empty’
+ In the expression: BiApp empty empty
In an equation for ‘empty’: empty = BiApp empty empty
- In the instance declaration for ‘Ix (l :|: r)’
• Relevant bindings include
empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:19:4)
diff --git a/testsuite/tests/indexed-types/should_fail/T2664.stderr b/testsuite/tests/indexed-types/should_fail/T2664.stderr
index 64fa85125852..deaffc82ddc9 100644
--- a/testsuite/tests/indexed-types/should_fail/T2664.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2664.stderr
@@ -1,30 +1,22 @@
-T2664.hs:31:9: error:
- • Could not deduce: Dual a ~ Dual b
+T2664.hs:31:52: error:
+ • Could not deduce: b ~ a arising from a use of ‘newPChan’
from the context: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b))
bound by the type signature for:
newPChan :: forall c.
((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
IO (PChan (a :*: b), PChan c)
at T2664.hs:23:5-12
- Expected: IO (PChan (a :*: b), PChan c)
- Actual: IO (PChan (a :*: b), PChan (Dual b :+: Dual a))
- NB: ‘Dual’ is a non-injective type family
- • In a stmt of a 'do' block:
- return
- (O $ takeMVar v,
- E (pchoose Right v newPChan) (pchoose Left v newPChan))
+ ‘b’ is a rigid type variable bound by
+ the instance declaration
+ at T2664.hs:22:10-52
+ ‘a’ is a rigid type variable bound by
+ the instance declaration
+ at T2664.hs:22:10-52
+ • In the third argument of ‘pchoose’, namely ‘newPChan’
+ In the first argument of ‘E’, namely ‘(pchoose Right v newPChan)’
In the expression:
- do v <- newEmptyMVar
- return
- (O $ takeMVar v,
- E (pchoose Right v newPChan) (pchoose Left v newPChan))
- In an equation for ‘newPChan’:
- newPChan
- = do v <- newEmptyMVar
- return
- (O $ takeMVar v,
- E (pchoose Right v newPChan) (pchoose Left v newPChan))
+ E (pchoose Right v newPChan) (pchoose Left v newPChan)
• Relevant bindings include
v :: MVar (Either (PChan a) (PChan b)) (bound at T2664.hs:24:9)
newPChan :: IO (PChan (a :*: b), PChan c) (bound at T2664.hs:23:5)
diff --git a/testsuite/tests/indexed-types/should_fail/T4272.stderr b/testsuite/tests/indexed-types/should_fail/T4272.stderr
index c921445d2e61..69df514c0f1f 100644
--- a/testsuite/tests/indexed-types/should_fail/T4272.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4272.stderr
@@ -1,16 +1,17 @@
-T4272.hs:15:19: error:
- • Couldn't match expected type ‘TermFamily a a’
- with actual type ‘a’
+T4272.hs:15:26: error:
+ • Couldn't match type ‘a’ with ‘TermFamily a a’
+ Expected: TermFamily a (TermFamily a a)
+ Actual: TermFamily a a
‘a’ is a rigid type variable bound by
the type signature for:
laws :: forall a b. TermLike a => TermFamily a a -> b
at T4272.hs:14:1-53
- • In the second argument of ‘prune’, namely
+ • In the first argument of ‘terms’, namely
+ ‘(undefined :: TermFamily a a)’
+ In the second argument of ‘prune’, namely
‘(terms (undefined :: TermFamily a a))’
In the expression: prune t (terms (undefined :: TermFamily a a))
- In an equation for ‘laws’:
- laws t = prune t (terms (undefined :: TermFamily a a))
• Relevant bindings include
t :: TermFamily a a (bound at T4272.hs:15:6)
laws :: TermFamily a a -> b (bound at T4272.hs:15:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index 5dcce91edbd5..c7f230654e80 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -3,7 +3,8 @@ T5439.hs:82:33: error:
• Couldn't match expected type: Attempt (HElemOf rs)
with actual type: Attempt (HHead (HDrop n0 l0))
-> Attempt (HElemOf l0)
- • In the second argument of ‘($)’, namely
+ • Probable cause: ‘($)’ is applied to too few arguments
+ In the second argument of ‘($)’, namely
‘inj $ Failure (e :: SomeException)’
In a stmt of a 'do' block:
c <- complete ev $ inj $ Failure (e :: SomeException)
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 04acdc653d1b..e2f7597b93a8 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -2,7 +2,7 @@
T9662.hs:49:8: error:
• Couldn't match type ‘n’ with ‘Int’
Expected: Exp (((sh :. k) :. m) :. n)
- -> Exp (((sh :. k) :. m) :. n)
+ -> Exp (((sh :. m) :. n) :. k)
Actual: Exp
(Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-> Exp
diff --git a/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr b/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
index 26c895ef3c34..4a2d1673272f 100644
--- a/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/Forall1Bad.stderr
@@ -1,5 +1,6 @@
-Forall1Bad.hs:9:8: error:
+Forall1Bad.hs:9:13: error:
• Couldn't match expected type ‘Char’ with actual type ‘Bool’
- • In the expression: fall True
+ • In the first argument of ‘fall’, namely ‘True’
+ In the expression: fall True
In an equation for ‘test’: test = fall True
diff --git a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
index e366651f7d4f..17ffbc1595b3 100644
--- a/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/NamedWildcardExplicitForall.stderr
@@ -22,14 +22,14 @@ NamedWildcardExplicitForall.hs:13:26: error:
To use the inferred type, enable PartialTypeSignatures
• In the type signature: baz :: forall _a. _a -> _b -> (_a, _b)
-NamedWildcardExplicitForall.hs:14:16: error:
- • Couldn't match expected type ‘Bool’ with actual type ‘_a’
+NamedWildcardExplicitForall.hs:14:12: error:
+ • Couldn't match expected type ‘_a’ with actual type ‘Bool’
‘_a’ is a rigid type variable bound by
the inferred type of baz :: _a -> Bool -> (_a, Bool)
at NamedWildcardExplicitForall.hs:13:15-16
- • In the first argument of ‘not’, namely ‘x’
- In the expression: not x
+ • In the expression: not x
In the expression: (not x, not y)
+ In an equation for ‘baz’: baz x y = (not x, not y)
• Relevant bindings include
x :: _a (bound at NamedWildcardExplicitForall.hs:14:5)
baz :: _a -> Bool -> (_a, Bool)
diff --git a/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr b/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
index e4c368c6e195..a1a1295b123e 100644
--- a/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
+++ b/testsuite/tests/partial-sigs/should_fail/PatBind3.stderr
@@ -1,9 +1,10 @@
-PatBind3.hs:6:12: error:
+PatBind3.hs:6:17: error:
• Couldn't match type ‘(Bool, w)’ with ‘Char’
- Expected: Maybe ((Bool, w) -> Char)
- Actual: Maybe ((Bool, w) -> (Bool, w))
- • In the expression: Just id
+ Expected: (Bool, w) -> Char
+ Actual: (Bool, w) -> (Bool, w)
+ • In the first argument of ‘Just’, namely ‘id’
+ In the expression: Just id
In a pattern binding: Just foo = Just id
• Relevant bindings include
foo :: (Bool, w) -> Char (bound at PatBind3.hs:6:6)
diff --git a/testsuite/tests/patsyn/should_fail/T15695.stderr b/testsuite/tests/patsyn/should_fail/T15695.stderr
index 82398e15a7cf..9418f15a713f 100644
--- a/testsuite/tests/patsyn/should_fail/T15695.stderr
+++ b/testsuite/tests/patsyn/should_fail/T15695.stderr
@@ -33,12 +33,13 @@ T15695.hs:39:14: warning: [-Wdeferred-type-errors (in -Wdefault)]
from' :: ApplyT (* -> * -> *) Either ctx -> NS (NP NA) '[ '[ 'VO]]
(bound at T15695.hs:39:1)
-T15695.hs:40:26: warning: [-Wdeferred-type-errors (in -Wdefault)]
+T15695.hs:40:33: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type: a0 : as0
with: '[]
- Expected: NS (NP NA) '[ '[ 'VO]]
- Actual: NS (NP NA) ('[ 'VO] : a0 : as0)
- • In the expression: There (Here undefined)
+ Expected: NS (NP NA) '[]
+ Actual: NS (NP NA) (a0 : as0)
+ • In the first argument of ‘There’, namely ‘(Here undefined)’
+ In the expression: There (Here undefined)
In an equation for ‘from'’:
from' (ASSO (Right b)) = There (Here undefined)
• Relevant bindings include
diff --git a/testsuite/tests/th/T10945.stderr b/testsuite/tests/th/T10945.stderr
index 1c7a0f238d35..fe71a2f50c56 100644
--- a/testsuite/tests/th/T10945.stderr
+++ b/testsuite/tests/th/T10945.stderr
@@ -1,10 +1,17 @@
-T10945.hs:7:4: error:
+T10945.hs:7:11: error:
• Couldn't match type: [Dec]
with: Q [Dec]
- Expected: Code Q DecsQ
- Actual: Code Q [Dec]
- • In the expression:
+ Expected: DecsQ
+ Actual: [Dec]
+ • In the first argument of ‘return’, namely
+ ‘[SigD
+ (mkName "m")
+ (ForallT
+ [PlainTV (mkName "a") SpecifiedSpec] []
+ (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
+ FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]’
+ In the expression:
return
[SigD
(mkName "m")
@@ -20,11 +27,3 @@ T10945.hs:7:4: error:
[PlainTV (mkName "a") SpecifiedSpec] []
(AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]])
- In the expression:
- $$(return
- [SigD
- (mkName "m")
- (ForallT
- [PlainTV (mkName "a") SpecifiedSpec] []
- (AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
- FunD (mkName "m") [Clause ... (NormalB (VarE (mkName "x"))) []]])
diff --git a/testsuite/tests/typecheck/should_compile/FD2.stderr b/testsuite/tests/typecheck/should_compile/FD2.stderr
index 323d10f06d4b..a5462aa94ee5 100644
--- a/testsuite/tests/typecheck/should_compile/FD2.stderr
+++ b/testsuite/tests/typecheck/should_compile/FD2.stderr
@@ -1,6 +1,6 @@
-FD2.hs:26:36: error:
- • Couldn't match expected type ‘e’ with actual type ‘e1’
+FD2.hs:26:34: error:
+ • Couldn't match expected type ‘e1’ with actual type ‘e’
‘e1’ is a rigid type variable bound by
the type signature for:
mf :: forall e1. Elem a e1 => e1 -> Maybe e1 -> Maybe e1
@@ -9,9 +9,9 @@ FD2.hs:26:36: error:
the type signature for:
foldr1 :: forall e. Elem a e => (e -> e -> e) -> a -> e
at FD2.hs:21:13-47
- • In the first argument of ‘f’, namely ‘x’
- In the first argument of ‘Just’, namely ‘(f x y)’
+ • In the first argument of ‘Just’, namely ‘(f x y)’
In the expression: Just (f x y)
+ In an equation for ‘mf’: mf x (Just y) = Just (f x y)
• Relevant bindings include
y :: e1 (bound at FD2.hs:26:23)
x :: e1 (bound at FD2.hs:26:15)
diff --git a/testsuite/tests/typecheck/should_compile/T15368.stderr b/testsuite/tests/typecheck/should_compile/T15368.stderr
index 33b0407730c0..5760692c755f 100644
--- a/testsuite/tests/typecheck/should_compile/T15368.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15368.stderr
@@ -14,14 +14,15 @@ T15368.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
• Relevant bindings include
trigger :: a -> b -> (F a b, F b a) (bound at T15368.hs:11:1)
-T15368.hs:11:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
+T15368.hs:11:30: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type: F b0 a0
with: F b a
- Expected: (F a b, F b a)
- Actual: (F a b, F b0 a0)
+ Expected: (F a0 b0, F b a)
+ Actual: (F a0 b0, F b0 a0)
NB: ‘F’ is a non-injective type family
The type variables ‘b0’, ‘a0’ are ambiguous
- • In the expression: _ `transitive` trigger _ _
+ • In the second argument of ‘transitive’, namely ‘trigger _ _’
+ In the expression: _ `transitive` trigger _ _
In an equation for ‘trigger’:
trigger _ _ = _ `transitive` trigger _ _
• Relevant bindings include
diff --git a/testsuite/tests/typecheck/should_compile/T15370.stderr b/testsuite/tests/typecheck/should_compile/T15370.stderr
index f359155dbd02..798cfc9f8a88 100644
--- a/testsuite/tests/typecheck/should_compile/T15370.stderr
+++ b/testsuite/tests/typecheck/should_compile/T15370.stderr
@@ -20,19 +20,15 @@ T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
• Couldn't match type ‘S r’ with ‘()’
Expected: ()
Actual: S r
- • In the expression: no + _
+ • In the first argument of ‘(+)’, namely ‘no’
+ In the expression: no + _
In a case alternative: Refl -> no + _
- In the expression: case mkRefl @x @y of { Refl -> no + _ }
• Relevant bindings include
no :: S r (bound at T15370.hs:18:7)
right :: S r -> () (bound at T15370.hs:18:1)
T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
- • Found hole: _ :: S r
- Where: ‘r’, ‘y’, ‘x’ are rigid type variables bound by
- the type signature for:
- right :: forall x y (r :: Either x y). S r -> ()
- at T15370.hs:(16,1)-(17,18)
+ • Found hole: _ :: ()
• In the second argument of ‘(+)’, namely ‘_’
In the expression: no + _
In a case alternative: Refl -> no + _
@@ -40,3 +36,8 @@ T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
no :: S r (bound at T15370.hs:18:7)
right :: S r -> () (bound at T15370.hs:18:1)
Constraints include y ~ x (from T15370.hs:20:5-8)
+ Valid hole fits include
+ () :: ()
+ mempty :: forall a. Monoid a => a
+ maxBound :: forall a. Bounded a => a
+ minBound :: forall a. Bounded a => a
diff --git a/testsuite/tests/typecheck/should_compile/T2494.stderr b/testsuite/tests/typecheck/should_compile/T2494.stderr
index 8e427c5ac86c..d7c96aeeaab6 100644
--- a/testsuite/tests/typecheck/should_compile/T2494.stderr
+++ b/testsuite/tests/typecheck/should_compile/T2494.stderr
@@ -21,7 +21,7 @@ T2494.hs:15:14: error:
T2494.hs:15:30: error:
• Couldn't match type ‘b’ with ‘a’
- Expected: Maybe (m b) -> Maybe (m a)
+ Expected: Maybe (m a) -> Maybe (m a)
Actual: Maybe (m b) -> Maybe (m b)
‘b’ is a rigid type variable bound by
the RULE "foo/foo"
diff --git a/testsuite/tests/typecheck/should_fail/T12648.stderr b/testsuite/tests/typecheck/should_fail/T12648.stderr
index f13b6c1cd013..6f12341c062a 100644
--- a/testsuite/tests/typecheck/should_fail/T12648.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12648.stderr
@@ -1,17 +1,13 @@
-T12648.hs:76:2: error:
- • Couldn't match type ‘a’ with ‘()’
- Expected: m a
- Actual: m ()
+T12648.hs:76:9: error:
+ • Couldn't match expected type ‘a’ with actual type ‘()’
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall (m :: * -> *) a. MonadBaseUnlift m IO => m a
at T12648.hs:71:1-34
- • In a stmt of a 'do' block: return ()
+ • In the first argument of ‘return’, namely ‘()’
+ In a stmt of a 'do' block: return ()
In the expression:
do _ <- askUnliftBase
return ()
- In an equation for ‘f’:
- f = do _ <- askUnliftBase
- return ()
• Relevant bindings include f :: m a (bound at T12648.hs:72:1)
diff --git a/testsuite/tests/typecheck/should_fail/T1899.stderr b/testsuite/tests/typecheck/should_fail/T1899.stderr
index bd4aceed9ee6..ceb5f69c66cf 100644
--- a/testsuite/tests/typecheck/should_fail/T1899.stderr
+++ b/testsuite/tests/typecheck/should_fail/T1899.stderr
@@ -1,15 +1,15 @@
-T1899.hs:15:36: error:
- • Couldn't match type ‘a’ with ‘Proposition a0’
- Expected: [Proposition a0]
- Actual: [a]
+T1899.hs:15:26: error:
+ • Couldn't match expected type ‘a’
+ with actual type ‘Proposition a0’
‘a’ is a rigid type variable bound by
the type signature for:
transRHS :: forall a. [a] -> Int -> Constraint a
at T1899.hs:9:2-39
- • In the first argument of ‘Auxiliary’, namely ‘varSet’
- In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
+ • In the first argument of ‘Prop’, namely ‘(Auxiliary varSet)’
In the expression: Prop (Auxiliary varSet)
+ In the expression:
+ [Prop (Auxiliary varSet), Prop (Auxiliary varSet)]
• Relevant bindings include
varSet :: [a] (bound at T1899.hs:10:11)
transRHS :: [a] -> Int -> Constraint a (bound at T1899.hs:10:2)
diff --git a/testsuite/tests/typecheck/should_fail/T19364.hs b/testsuite/tests/typecheck/should_fail/T19364.hs
new file mode 100644
index 000000000000..6b7259c6ee06
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19364.hs
@@ -0,0 +1,12 @@
+module T19364 where
+
+type Foo = Bool
+type Bar = String
+
+data Pair a b = Pair a b
+
+baz :: Pair Foo Bar
+baz = Pair "yes" "no"
+
+-- The whole point about this test is the quality
+-- of the error message in baz: see #19364
diff --git a/testsuite/tests/typecheck/should_fail/T19364.stderr b/testsuite/tests/typecheck/should_fail/T19364.stderr
new file mode 100644
index 000000000000..ffd5ad2bf7a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19364.stderr
@@ -0,0 +1,8 @@
+
+T19364.hs:9:12: error:
+ • Couldn't match type ‘[Char]’ with ‘Bool’
+ Expected: Foo
+ Actual: String
+ • In the first argument of ‘Pair’, namely ‘"yes"’
+ In the expression: Pair "yes" "no"
+ In an equation for ‘baz’: baz = Pair "yes" "no"
diff --git a/testsuite/tests/typecheck/should_fail/T2688.stderr b/testsuite/tests/typecheck/should_fail/T2688.stderr
index f7980d273439..748ec505f373 100644
--- a/testsuite/tests/typecheck/should_fail/T2688.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2688.stderr
@@ -1,5 +1,5 @@
-T2688.hs:8:14: error:
+T2688.hs:8:22: error:
• Couldn't match expected type ‘v’ with actual type ‘s’
‘s’ is a rigid type variable bound by
the class declaration for ‘VectorSpace’
@@ -7,8 +7,9 @@ T2688.hs:8:14: error:
‘v’ is a rigid type variable bound by
the class declaration for ‘VectorSpace’
at T2688.hs:5:19
- • In the expression: v *^ (1 / s)
- In an equation for ‘^/’: v ^/ s = v *^ (1 / s)
+ • In the second argument of ‘(/)’, namely ‘s’
+ In the second argument of ‘(*^)’, namely ‘(1 / s)’
+ In the expression: v *^ (1 / s)
• Relevant bindings include
s :: s (bound at T2688.hs:8:10)
v :: v (bound at T2688.hs:8:5)
diff --git a/testsuite/tests/typecheck/should_fail/T3613.stderr b/testsuite/tests/typecheck/should_fail/T3613.stderr
index 8183ff981e8d..cff3344597df 100644
--- a/testsuite/tests/typecheck/should_fail/T3613.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3613.stderr
@@ -1,12 +1,11 @@
T3613.hs:14:20: error:
• Couldn't match type ‘IO’ with ‘Maybe’
- Expected: Maybe b
- Actual: IO b
- • In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
+ Expected: Maybe ()
+ Actual: IO ()
+ • In the first argument of ‘(>>)’, namely ‘bar’
+ In the first argument of ‘fooThen’, namely ‘(bar >> undefined)’
In the expression: fooThen (bar >> undefined)
- In the expression:
- let fooThen m = foo >> m in fooThen (bar >> undefined)
T3613.hs:17:24: error:
• Couldn't match type ‘IO’ with ‘Maybe’
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index f71fd5d50161..69ff2764797b 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,12 +1,13 @@
-T3950.hs:15:8: error:
+T3950.hs:15:13: error:
• Couldn't match kind ‘*’ with ‘* -> *’
When matching types
w :: (* -> * -> *) -> *
Sealed :: (* -> *) -> *
- Expected: Maybe (w (Id p))
- Actual: Maybe (Sealed (Id p0 x0))
- • In the expression: Just rp'
+ Expected: w (Id p)
+ Actual: Sealed (Id p0 x0)
+ • In the first argument of ‘Just’, namely ‘rp'’
+ In the expression: Just rp'
In an equation for ‘rp’:
rp _
= Just rp'
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
index 3b203968f07d..52d57c01e669 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed2.stderr
@@ -1,7 +1,6 @@
-T6018failclosed2.hs:17:14:
- Couldn't match expected type ‘Bar a0’ with actual type ‘Char’
- The type variable ‘a0’ is ambiguous
- In the first argument of ‘bar’, namely ‘'c'’
- In the expression: bar 'c'
- In an equation for ‘barapp’: barapp = bar 'c'
+T6018failclosed2.hs:17:10: error:
+ • Couldn't match expected type ‘Char’ with actual type ‘Bar a0’
+ The type variable ‘a0’ is ambiguous
+ • In the expression: bar 'c'
+ In an equation for ‘barapp’: barapp = bar 'c'
diff --git a/testsuite/tests/typecheck/should_fail/T8450.stderr b/testsuite/tests/typecheck/should_fail/T8450.stderr
index 9ac0d63643a2..8ba84a76f15a 100644
--- a/testsuite/tests/typecheck/should_fail/T8450.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8450.stderr
@@ -1,15 +1,11 @@
-T8450.hs:8:19: error:
- • Couldn't match type ‘a’ with ‘Bool’
- Expected: Either Bool ()
- Actual: Either a ()
+T8450.hs:8:7: error:
+ • Couldn't match expected type ‘a’ with actual type ‘()’
‘a’ is a rigid type variable bound by
the type signature for:
run :: forall a. a
at T8450.hs:7:1-18
- • In the second argument of ‘($)’, namely
- ‘(undefined :: Either a ())’
- In the expression: runEffect $ (undefined :: Either a ())
+ • In the expression: runEffect $ (undefined :: Either a ())
In an equation for ‘run’:
run = runEffect $ (undefined :: Either a ())
• Relevant bindings include run :: a (bound at T8450.hs:8:1)
diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr
index b3752e427930..2a6c0ac16c67 100644
--- a/testsuite/tests/typecheck/should_fail/T9260.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9260.stderr
@@ -1,7 +1,8 @@
-T9260.hs:12:8: error:
- • Couldn't match type ‘2’ with ‘1’
- Expected: Fin 1
- Actual: Fin ((0 + 1) + 1)
- • In the expression: Fsucc Fzero
+T9260.hs:12:14: error:
+ • Couldn't match type ‘1’ with ‘0’
+ Expected: Fin 0
+ Actual: Fin (0 + 1)
+ • In the first argument of ‘Fsucc’, namely ‘Fzero’
+ In the expression: Fsucc Fzero
In an equation for ‘test’: test = Fsucc Fzero
diff --git a/testsuite/tests/typecheck/should_fail/T9774.stderr b/testsuite/tests/typecheck/should_fail/T9774.stderr
index da75c339b85d..2381e3ce75bc 100644
--- a/testsuite/tests/typecheck/should_fail/T9774.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9774.stderr
@@ -1,8 +1,8 @@
-T9774.hs:5:17: error:
+T9774.hs:5:29: error:
• Couldn't match type ‘Char’ with ‘[Char]’
Expected: String
Actual: Char
- • In the first argument of ‘putStrLn’, namely ‘(assert True 'a')’
+ • In the second argument of ‘assert’, namely ‘'a'’
+ In the first argument of ‘putStrLn’, namely ‘(assert True 'a')’
In the expression: putStrLn (assert True 'a')
- In an equation for ‘foo’: foo = putStrLn (assert True 'a')
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 07eafc65b5b7..4768b19263ae 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -616,3 +616,4 @@ test('T12178a', normal, compile_fail, [''])
test('T18869', normal, compile_fail, [''])
test('T19142', normal, compile_fail, [''])
test('T19346', normal, compile_fail, ['-fprint-typechecker-elaboration'])
+test('T19364', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail065.stderr b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
index 9be21918cb42..81746cd2001c 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail065.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail065.stderr
@@ -1,8 +1,6 @@
-tcfail065.hs:29:18: error:
- • Couldn't match type ‘x1’ with ‘x’
- Expected: X x
- Actual: X x1
+tcfail065.hs:29:20: error:
+ • Couldn't match expected type ‘x’ with actual type ‘x1’
‘x1’ is a rigid type variable bound by
the type signature for:
setX :: forall x1. x1 -> X x -> X x
@@ -10,9 +8,9 @@ tcfail065.hs:29:18: error:
‘x’ is a rigid type variable bound by
the instance declaration
at tcfail065.hs:28:10-19
- • In the expression: X x
+ • In the first argument of ‘X’, namely ‘x’
+ In the expression: X x
In an equation for ‘setX’: setX x (X _) = X x
- In the instance declaration for ‘HasX (X x)’
• Relevant bindings include
x :: x1 (bound at tcfail065.hs:29:8)
setX :: x1 -> X x -> X x (bound at tcfail065.hs:29:3)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail068.stderr b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
index c7b7630e049b..7266e7682338 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail068.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail068.stderr
@@ -22,10 +22,10 @@ tcfail068.hs:14:9: error:
itgen :: (Int, Int) -> a -> IndTree s a
(bound at tcfail068.hs:12:1)
-tcfail068.hs:19:9: error:
+tcfail068.hs:19:21: error:
• Couldn't match type ‘s1’ with ‘s’
- Expected: GHC.ST.ST s1 (IndTree s a)
- Actual: GHC.ST.ST s (IndTree s a)
+ Expected: STArray s1 (Int, Int) a
+ Actual: IndTree s a
‘s1’ is a rigid type variable bound by
a type expected by the context:
forall s1. GHC.ST.ST s1 (IndTree s a)
@@ -36,18 +36,11 @@ tcfail068.hs:19:9: error:
Constructed a =>
(Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
at tcfail068.hs:16:1-75
- • In the first argument of ‘runST’, namely
+ • In the first argument of ‘readSTArray’, namely ‘arr’
+ In the first argument of ‘(>>=)’, namely ‘readSTArray arr i’
+ In the first argument of ‘runST’, namely
‘(readSTArray arr i
>>= \ val -> writeSTArray arr i (f val) >> return arr)’
- In the expression:
- runST
- (readSTArray arr i
- >>= \ val -> writeSTArray arr i (f val) >> return arr)
- In an equation for ‘itiap’:
- itiap i f arr
- = runST
- (readSTArray arr i
- >>= \ val -> writeSTArray arr i (f val) >> return arr)
• Relevant bindings include
arr :: IndTree s a (bound at tcfail068.hs:17:11)
itiap :: (Int, Int) -> (a -> a) -> IndTree s a -> IndTree s a
diff --git a/testsuite/tests/typecheck/should_fail/tcfail103.stderr b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
index 84c9c8b0b664..0a7a386f9e4f 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail103.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail103.stderr
@@ -1,8 +1,8 @@
-tcfail103.hs:15:13: error:
+tcfail103.hs:15:23: error:
• Couldn't match type ‘s’ with ‘t’
- Expected: ST s Int
- Actual: ST t Int
+ Expected: STRef s Int
+ Actual: STRef t Int
‘s’ is a rigid type variable bound by
the type signature for:
g :: forall s. ST s Int
@@ -11,13 +11,9 @@ tcfail103.hs:15:13: error:
the type signature for:
f :: forall t. ST t Int
at tcfail103.hs:10:1-12
- • In the expression: readSTRef v
+ • In the first argument of ‘readSTRef’, namely ‘v’
+ In the expression: readSTRef v
In an equation for ‘g’: g = readSTRef v
- In the expression:
- do v <- newSTRef 5
- let g :: ST s Int
- g = readSTRef v
- g
• Relevant bindings include
g :: ST s Int (bound at tcfail103.hs:15:9)
v :: STRef t Int (bound at tcfail103.hs:12:5)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail131.stderr b/testsuite/tests/typecheck/should_fail/tcfail131.stderr
index 04fa00020477..25f3f427eda9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail131.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail131.stderr
@@ -1,12 +1,11 @@
-tcfail131.hs:7:11: error:
- • Couldn't match expected type ‘Integer’ with actual type ‘b’
+tcfail131.hs:7:9: error:
+ • Couldn't match expected type ‘b’ with actual type ‘Integer’
‘b’ is a rigid type variable bound by
the type signature for:
g :: forall b. Num b => b -> b
at tcfail131.hs:6:3-22
- • In the first argument of ‘f’, namely ‘x’
- In the expression: f x x
+ • In the expression: f x x
In an equation for ‘g’: g x = f x x
• Relevant bindings include
x :: b (bound at tcfail131.hs:7:5)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail153.stderr b/testsuite/tests/typecheck/should_fail/tcfail153.stderr
index 4faca8f037ee..0d38db4385c3 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail153.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail153.stderr
@@ -1,12 +1,13 @@
-tcfail153.hs:6:9: error:
- • Couldn't match expected type ‘Bool’ with actual type ‘a’
+tcfail153.hs:6:7: error:
+ • Couldn't match type ‘a’ with ‘Bool’
+ Expected: [a]
+ Actual: [Bool]
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a. a -> [a]
at tcfail153.hs:5:1-13
- • In the first argument of ‘g’, namely ‘x’
- In the expression: g x
+ • In the expression: g x
In an equation for ‘f’:
f x
= g x
diff --git a/testsuite/tests/typecheck/should_fail/tcfail179.stderr b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
index a0c124590f38..963ab0ba7869 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail179.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail179.stderr
@@ -1,8 +1,6 @@
-tcfail179.hs:14:41: error:
- • Couldn't match type ‘x’ with ‘s’
- Expected: x -> s
- Actual: x -> x
+tcfail179.hs:14:39: error:
+ • Couldn't match expected type ‘s’ with actual type ‘x’
‘x’ is a rigid type variable bound by
a pattern with constructor:
T :: forall s x. (s -> (x -> s) -> (x, s, Int)) -> T s,
@@ -12,11 +10,11 @@ tcfail179.hs:14:41: error:
the type signature for:
run :: forall s. T s -> Int
at tcfail179.hs:12:1-17
- • In the second argument of ‘g’, namely ‘id’
+ • In the first argument of ‘g’, namely ‘x’
In the expression: g x id
In a pattern binding: (x, _, b) = g x id
• Relevant bindings include
- x :: s (bound at tcfail179.hs:14:26)
+ x :: x (bound at tcfail179.hs:14:26)
g :: s -> (x -> s) -> (x, s, Int) (bound at tcfail179.hs:14:16)
ts :: T s (bound at tcfail179.hs:13:5)
run :: T s -> Int (bound at tcfail179.hs:13:1)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index dd1385fc9052..023772c775d9 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,17 +1,15 @@
-tcfail201.hs:17:56: error:
- • Couldn't match type ‘a’ with ‘HsDoc id0’
- Expected: c a
- Actual: c (HsDoc id0)
+tcfail201.hs:17:58: error:
+ • Couldn't match expected type ‘a’ with actual type ‘HsDoc id0’
‘a’ is a rigid type variable bound by
the type signature for:
gfoldl' :: forall (c :: * -> *) a.
(forall a1 b. c (a1 -> b) -> a1 -> c b)
-> (forall g. g -> c g) -> a -> c a
at tcfail201.hs:15:1-85
- • In the expression: z DocEmpty
+ • In the first argument of ‘z’, namely ‘DocEmpty’
+ In the expression: z DocEmpty
In a case alternative: DocEmpty -> z DocEmpty
- In the expression: case hsDoc of { DocEmpty -> z DocEmpty }
• Relevant bindings include
hsDoc :: a (bound at tcfail201.hs:16:13)
gfoldl' :: (forall a1 b. c (a1 -> b) -> a1 -> c b)
diff --git a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
index c2ff69c9ef15..a4b6cc0b7498 100644
--- a/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
+++ b/testsuite/tests/warnings/should_fail/CaretDiagnostics1.stderr
@@ -1,50 +1,27 @@
-CaretDiagnostics1.hs:(5,3)-(7,16): error:
+CaretDiagnostics1.hs:7:8-15: error:
• Couldn't match expected type ‘IO a0’ with actual type ‘Int’
- • In a stmt of a 'do' block:
+ • In the second argument of ‘(+)’, namely ‘(3 :: Int)’
+ In a stmt of a 'do' block:
10000000000000000000000000000000000000 + 2 + (3 :: Int)
In the expression:
do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
pure ("this is not an IO" + ())
- In an equation for ‘main’:
- main
- = do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
- pure ("this is not an IO" + ())
- where
- _ = case id of { "γηξ" -> () '0' }
|
-5 | 10000000000000000000000000000000000000 +
- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^...
+7 | (3 :: Int)
+ | ^^^^^^^^
-CaretDiagnostics1.hs:8:3-45: error:
+CaretDiagnostics1.hs:8:9-27: error:
• Couldn't match type ‘[Char]’ with ‘()’
- Expected: IO ()
- Actual: IO String
- • In a stmt of a 'do' block: pure ("this is not an IO" + ())
- In the expression:
- do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
- pure ("this is not an IO" + ())
- In an equation for ‘main’:
- main
- = do 10000000000000000000000000000000000000 + 2 + (3 :: Int)
- pure ("this is not an IO" + ())
- where
- _ = case id of { "γηξ" -> () '0' }
- |
-8 | pure ("this is not an IO" + ( ))
- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
-
-CaretDiagnostics1.hs:8:31-44: error:
- • Couldn't match type ‘()’ with ‘[Char]’
- Expected: String
- Actual: ()
- • In the second argument of ‘(+)’, namely ‘()’
+ Expected: ()
+ Actual: String
+ • In the first argument of ‘(+)’, namely ‘"this is not an IO"’
In the first argument of ‘pure’, namely
‘("this is not an IO" + ())’
In a stmt of a 'do' block: pure ("this is not an IO" + ())
|
8 | pure ("this is not an IO" + ( ))
- | ^^^^^^^^^^^^^^
+ | ^^^^^^^^^^^^^^^^^^^
CaretDiagnostics1.hs:13:7-11: error:
• Couldn't match type: a1 -> a1
--
GitLab