summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/GHC/Tc/Errors.hs17
-rw-r--r--compiler/GHC/Tc/Gen/App.hs164
-rw-r--r--compiler/GHC/Tc/Gen/Head.hs30
-rw-r--r--compiler/GHC/Tc/Solver/Interact.hs103
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs9
-rw-r--r--compiler/GHC/Tc/Types/Origin.hs16
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs13
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs19
8 files changed, 230 insertions, 141 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 0e687040e0..82dbd65848 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 29dc16ab07..cc1411ba90 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 faf5e0f2f2..5b57f397ce 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 b8df1fbae6..8474ca7007 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 3862d842b0..29344b17d7 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 b0d970bb37..648bf5ce12 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 ed9ee9cc44..1e82be0f0e 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 121ebfbe7e..eee4e1844c 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
View Lorry Controller Status