Commit fb752133 authored by Richard Eisenberg's avatar Richard Eisenberg

Track visibility in TypeEqOrigin

A type equality error can arise from a mismatch between
*invisible* arguments just as easily as from visible arguments.
But we should really prefer printing out errors from visible
arguments over invisible ones. Suppose we have a mismatch between
`Proxy Int` and `Proxy Maybe`. Would you rather get an error
between `Int` and `Maybe`? Or between `*` and `* -> *`? I thought
so, too.

There is a fair amount of plumbing with this one, but I think
it's worth it.

This commit introduces a performance regression in test
perf/compiler/T5631. The cause of the regression is not the
new visibility stuff, directly: it's due to a change from
zipWithM to zipWith3M in TcUnify. To my surprise, zipWithM
is nicely optimized (it fuses away), but zipWith3M is not.
There are other examples of functions that could be made faster,
so I've posted a separate ticket, #14037, to track these
improvements. For now, I've accepted the small (6.6%) regression.
parent c2417b87
......@@ -407,7 +407,8 @@ tcInstBinder _ subst (Anon ty)
| Just (mk, role, k1, k2) <- get_pred_tys_maybe substed_ty
= do { let origin = TypeEqOrigin { uo_actual = k1
, uo_expected = k2
, uo_thing = Nothing }
, uo_thing = Nothing
, uo_visible = True }
; co <- case role of
Nominal -> unifyKind Nothing k1 k2
Representational -> emitWantedEq origin KindLevel role k1 k2
......
......@@ -930,7 +930,10 @@ can_eq_app ev NomEq s1 t1 s2 t2
; stopWith ev "Decomposed [D] AppTy" }
| CtWanted { ctev_dest = dest, ctev_loc = loc } <- ev
= do { co_s <- unifyWanted loc Nominal s1 s2
; co_t <- unifyWanted loc Nominal t1 t2
; let arg_loc
| isNextArgVisible s1 = loc
| otherwise = updateCtLocOrigin loc toInvisibleOrigin
; co_t <- unifyWanted arg_loc Nominal t1 t2
; let co = mkAppCo co_s co_t
; setWantedEq dest co
; stopWith ev "Decomposed [W] AppTy" }
......@@ -1224,13 +1227,16 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-- the following makes a better distinction between "kind" and "type"
-- in error messages
bndrs = tyConBinders tc
kind_loc = toKindLoc loc
is_kinds = map isNamedTyConBinder bndrs
new_locs | Just KindLevel <- ctLocTypeOrKind_maybe loc
= repeat loc
| otherwise
= map (\is_kind -> if is_kind then kind_loc else loc) is_kinds
is_viss = map isVisibleTyConBinder bndrs
kind_xforms = map (\is_kind -> if is_kind then toKindLoc else id) is_kinds
vis_xforms = map (\is_vis -> if is_vis then id
else flip updateCtLocOrigin toInvisibleOrigin)
is_viss
-- zipWith3 (.) composes its first two arguments and applies it to the third
new_locs = zipWith3 (.) kind_xforms vis_xforms (repeat loc)
-- | Call when canonicalizing an equality fails, but if the equality is
-- representational, there is some hope for the future.
......
......@@ -481,8 +481,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
-- type checking to get a Lint error later
report1 = [ ("custom_error", is_user_type_error,True, mkUserTypeErrorReporter)
, given_eq_spec
, ("insoluble2 ty", utterly_wrong_ty, True, mkGroupReporter mkEqErr)
, ("insoluble2_ki", utterly_wrong, True, mkGroupReporter mkEqErr)
, ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr)
, ("skolem eq1", very_wrong, True, mkSkolReporter)
, ("skolem eq2", skolem_eq, True, mkSkolReporter)
, ("non-tv eq", non_tv_eq, True, mkSkolReporter)
......@@ -515,12 +514,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
utterly_wrong _ _ = False
-- Like utterly_wrong, but suppress derived kind equalities
utterly_wrong_ty ct pred
= utterly_wrong ct pred && case ctOrigin ct of
KindEqOrigin {} -> False
_ -> True
-- Things like (a ~N Int)
very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
very_wrong _ _ = False
......@@ -829,17 +822,21 @@ maybeAddDeferredHoleBinding ctxt err ct
tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
-- Use the first reporter in the list whose predicate says True
tryReporters ctxt reporters cts
= do { traceTc "tryReporters {" (ppr cts)
; (ctxt', cts') <- go ctxt reporters cts
= do { let (vis_cts, invis_cts) = partition (isVisibleOrigin . ctOrigin) cts
; traceTc "tryReporters {" (ppr vis_cts $$ ppr invis_cts)
; (ctxt', cts') <- go ctxt reporters vis_cts invis_cts
; traceTc "tryReporters }" (ppr cts')
; return (ctxt', cts') }
where
go ctxt [] cts
= return (ctxt, cts)
go ctxt (r : rs) cts
= do { (ctxt', cts') <- tryReporter ctxt r cts
; go ctxt' rs cts' }
go ctxt [] vis_cts invis_cts
= return (ctxt, vis_cts ++ invis_cts)
go ctxt (r : rs) vis_cts invis_cts
-- always look at *visible* Origins before invisible ones
-- this is the whole point of isVisibleOrigin
= do { (ctxt', vis_cts') <- tryReporter ctxt r vis_cts
; (ctxt'', invis_cts') <- tryReporter ctxt' r invis_cts
; go ctxt'' rs vis_cts' invis_cts' }
-- Carry on with the rest, because we must make
-- deferred bindings for them if we have -fdefer-type-errors
-- But suppress their error messages
......
......@@ -902,8 +902,9 @@ checkExpectedKind hs_ty ty act_kind exp_kind
= do { (ty', act_kind') <- instantiate ty act_kind exp_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
, uo_thing = Just (ppr hs_ty) }
; co_k <- uType origin KindLevel act_kind' exp_kind
, uo_thing = Just (ppr hs_ty)
, uo_visible = True } -- the hs_ty is visible
; co_k <- uType KindLevel origin act_kind' exp_kind
; traceTc "checkExpectedKind" (vcat [ ppr act_kind
, ppr exp_kind
, ppr co_k ])
......
......@@ -95,8 +95,9 @@ module TcRnTypes(
CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
ctLocTypeOrKind_maybe,
ctLocDepth, bumpCtLocDepth,
setCtLocOrigin, setCtLocEnv, setCtLocSpan,
setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
CtOrigin(..), exprCtOrigin, lexprCtOrigin, matchesCtOrigin, grhssCtOrigin,
isVisibleOrigin, toInvisibleOrigin,
TypeOrKind(..), isTypeLevel, isKindLevel,
pprCtOrigin, pprCtLoc,
pushErrCtxt, pushErrCtxtSameOrigin,
......@@ -2969,6 +2970,10 @@ bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDept
setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc
setCtLocOrigin ctl orig = ctl { ctl_origin = orig }
updateCtLocOrigin :: CtLoc -> (CtOrigin -> CtOrigin) -> CtLoc
updateCtLocOrigin ctl@(CtLoc { ctl_origin = orig }) upd
= ctl { ctl_origin = upd orig }
setCtLocEnv :: CtLoc -> TcLclEnv -> CtLoc
setCtLocEnv ctl env = ctl { ctl_env = env }
......@@ -3160,7 +3165,11 @@ data CtOrigin
| TypeEqOrigin { uo_actual :: TcType
, uo_expected :: TcType
, uo_thing :: Maybe SDoc
-- ^ The thing that has type "actual"
-- ^ The thing that has type "actual"
, uo_visible :: Bool
-- ^ Is at least one of the three elements above visible?
-- (Errors from the polymorphic subsumption check are considered
-- visible.) Only used for prioritizing error messages.
}
| KindEqOrigin
......@@ -3252,6 +3261,21 @@ isKindLevel :: TypeOrKind -> Bool
isKindLevel TypeLevel = False
isKindLevel KindLevel = True
-- An origin is visible if the place where the constraint arises is manifest
-- in user code. Currently, all origins are visible except for invisible
-- TypeEqOrigins. This is used when choosing which error of
-- several to report
isVisibleOrigin :: CtOrigin -> Bool
isVisibleOrigin (TypeEqOrigin { uo_visible = vis }) = vis
isVisibleOrigin (KindEqOrigin _ _ sub_orig _) = isVisibleOrigin sub_orig
isVisibleOrigin _ = True
-- Converts a visible origin to an invisible one, if possible. Currently,
-- this works only for TypeEqOrigin
toInvisibleOrigin :: CtOrigin -> CtOrigin
toInvisibleOrigin orig@(TypeEqOrigin {}) = orig { uo_visible = False }
toInvisibleOrigin orig = orig
instance Outputable CtOrigin where
ppr = pprCtOrigin
......@@ -3451,7 +3475,7 @@ 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 (TypeEqOrigin t1 t2 _ _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2]
pprCtO AnnOrigin = text "an annotation"
pprCtO HoleOrigin = text "a use of" <+> quotes (text "_")
pprCtO ListOrigin = text "an overloaded list"
......
......@@ -58,7 +58,7 @@ module TcType (
-- These are important because they do not look through newtypes
getTyVar,
tcSplitForAllTy_maybe,
tcSplitForAllTys, tcSplitPiTys, tcSplitForAllTyVarBndrs,
tcSplitForAllTys, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllTyVarBndrs,
tcSplitPhiTy, tcSplitPredFunTy_maybe,
tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
tcSplitFunTysN,
......@@ -187,7 +187,11 @@ module TcType (
pprTheta, pprParendTheta, pprThetaArrowTy, pprClassPred,
pprTvBndr, pprTvBndrs,
TypeSize, sizeType, sizeTypes, toposortTyVars
TypeSize, sizeType, sizeTypes, toposortTyVars,
---------------------------------
-- argument visibility
tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible
) where
......@@ -220,6 +224,7 @@ import BasicTypes
import Util
import Bag
import Maybes
import ListSetOps ( getNth )
import Outputable
import FastString
import ErrUtils( Validity(..), MsgDoc, isValid )
......@@ -1358,6 +1363,10 @@ variables. It's up to you to make sure this doesn't matter.
tcSplitPiTys :: Type -> ([TyBinder], Type)
tcSplitPiTys = splitPiTys
-- | Splits a type into a TyBinder and a body, if possible. Panics otherwise
tcSplitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
tcSplitPiTy_maybe = splitPiTy_maybe
tcSplitForAllTy_maybe :: Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty'
tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty)
......@@ -2590,3 +2599,28 @@ sizeType = go
sizeTypes :: [Type] -> TypeSize
sizeTypes tys = sum (map sizeType tys)
-----------------------------------------------------------------------------------
-----------------------------------------------------------------------------------
-----------------------
-- | For every arg a tycon can take, the returned list says True if the argument
-- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to
-- allow for oversaturation.
tcTyConVisibilities :: TyCon -> [Bool]
tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True
where
tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc)
tc_return_kind_viss = map isVisibleBinder (fst $ tcSplitPiTys (tyConResKind tc))
-- | If the tycon is applied to the types, is the next argument visible?
isNextTyConArgVisible :: TyCon -> [Type] -> Bool
isNextTyConArgVisible tc tys
= tcTyConVisibilities tc `getNth` length tys
-- | Should this type be applied to a visible argument?
isNextArgVisible :: TcType -> Bool
isNextArgVisible ty
| Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisibleBinder bndr
| otherwise = True
-- this second case might happen if, say, we have an unzonked TauTv.
-- But TauTvs can't range over types that take invisible arguments
This diff is collapsed.
......@@ -444,7 +444,7 @@ test('T5631',
# 2014-04-04: 346389856 (x86 Windows, 64 bit machine)
# 2014-12-01: 390199244 (Windows laptop)
# 2016-04-06: 570137436 (amd64/Linux) many reasons
(wordsize(64), 1037482512, 5)]),
(wordsize(64), 1106015512, 5)]),
# expected value: 774595008 (amd64/Linux):
# expected value: 735486328 (amd64/Linux) 2012/12/12:
# expected value: 690742040 (amd64/Linux) Call Arity improvements
......@@ -459,6 +459,8 @@ test('T5631',
# 2017-02-17: 1517484488 (amd64/Linux) Type-indexed Typeable
# 2017-03-03: 1065147968 (amd64/Linux) Share Typeable KindReps
# 2017-03-31: 1037482512 (amd64/Linux) Fix memory leak in simplifier
# 2017-07-27: 1106015512 (Mac) Regresssion from tracking visibility in TypeEqOrigin
# should be fixed by #14037
only_ways(['normal'])
],
compile,
......
KindVType.hs:8:8: error:
• Couldn't match type ‘*’ with ‘* -> *
• Couldn't match type ‘Int’ with ‘Maybe
Expected type: Proxy Maybe
Actual type: Proxy Int
• In the expression: (Proxy :: Proxy Int)
......
T12373.hs:10:19: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a1 :: *
MVar# RealWorld a0 :: TYPE 'UnliftedRep
Expected type: (# State# RealWorld, a1 #)
Actual type: (# State# RealWorld, MVar# RealWorld a0 #)
• In the expression: newMVar# rw
......
T13530.hs:11:7: error:
• Couldn't match a lifted type with an unlifted type
When matching types
a0 :: *
Int# :: TYPE 'IntRep
Expected type: (# Int#, Int# #)
Actual type: (# Int#, a0 #)
• In the expression: g x
......
T8603.hs:33:17: error:
• Couldn't match type ‘RV a1’ with ‘StateT s RV a0’
• Couldn't match kind ‘* -> *’ with ‘*’
When matching types
t0 :: (* -> *) -> * -> *
(->) :: * -> * -> *
Expected type: [Integer] -> StateT s RV a0
Actual type: t0 ((->) [a1]) (RV a1)
• The function ‘lift’ is applied to two arguments,
......@@ -10,5 +13,3 @@ T8603.hs:33:17: error:
In the expression:
do prize <- lift uniform [1, 2, ....]
return False
• Relevant bindings include
testRVState1 :: RVState s Bool (bound at T8603.hs:32:1)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment