[Git][ghc/ghc][wip/cfuneqcan-refactor] More reactions to reviews
Richard Eisenberg
gitlab at gitlab.haskell.org
Thu Nov 12 22:14:01 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
0b4d386c by Richard Eisenberg at 2020-11-12T17:13:46-05:00
More reactions to reviews
- - - - -
7 changed files:
- compiler/GHC/Core/Type.hs
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -1344,6 +1344,9 @@ splitTyConApp_maybe = repSplitTyConApp_maybe . coreFullView
-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
-- type before using this function.
--
+-- This does *not* split types headed with (=>), as that's not a TyCon in the
+-- type-checker.
+--
-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
-- Defined here to avoid module loops between Unify and TcType.
=====================================
compiler/GHC/HsToCore/Monad.hs
=====================================
@@ -300,7 +300,11 @@ initTcDsForSolver thing_inside
; let DsGblEnv { ds_mod = mod
, ds_fam_inst_env = fam_inst_env
, ds_gbl_rdr_env = rdr_env } = gbl
- -- this is *the* use of ds_gbl_rdr_env
+ -- This is *the* use of ds_gbl_rdr_env:
+ -- Make sure the solver (used by the pattern-match overlap checker) has
+ -- access to the GlobalRdrEnv and FamInstEnv for the module, so that it
+ -- knows how to reduce type families, and which newtypes it can unwrap.
+
DsLclEnv { dsl_loc = loc } = lcl
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -2050,9 +2050,7 @@ simplifyHoles = mapBagM simpl_hole
where
simpl_hole :: Hole -> TcS Hole
- -- do not simplify an extra-constraints wildcard. These holes
- -- are filled with already-simplified constraints in
- -- chooseInferredQuantifiers (choose_psig_context)
+ -- See Note [Do not simplify ConstraintHoles]
simpl_hole h@(Hole { hole_sort = ConstraintHole }) = return h
-- other wildcards should be simplified for printing
@@ -2102,6 +2100,41 @@ test T12227.
But we don't get to discard all redundant equality superclasses, alas;
see #15205.
+Note [Do not simplify ConstraintHoles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Before printing the inferred value for a type hole (a _ wildcard in
+a partial type signature), we simplify it w.r.t. any Givens. This
+makes for an easier-to-understand diagnostic for the user.
+
+However, we do not wish to do this for extra-constraint holes. Here is
+the example for why (partial-sigs/should_compile/T12844):
+
+ bar :: _ => FooData rngs
+ bar = foo
+
+ data FooData rngs
+
+ class Foo xs where foo :: (Head xs ~ '(r,r')) => FooData xs
+
+ type family Head (xs :: [k]) where Head (x ': xs) = x
+
+GHC correctly infers that the extra-constraints wildcard on `bar`
+should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this constraint
+as a Given on the implication constraint for `bar`. The Hole for
+the _ is stored within the implication's WantedConstraints.
+When simplifyHoles is called, that constraint is already assumed as
+a Given. Simplifying with respect to it turns it into
+('(r, r') ~ '(r, r'), Foo rngs), which is disastrous.
+
+Furthermore, there is no need to simplify here: extra-constraints wildcards
+are filled in with the output of the solver, in chooseInferredQuantifiers
+(choose_psig_context), so they are already simplified. (Contrast to normal
+type holes, which are just bound to a meta-variable.) Avoiding the poor output
+is simple: just don't simplify extra-constraints wildcards.
+
+This is the only reason we need to track ConstraintHole separately
+from TypeHole in HoleSort.
+
Note [Tracking redundant constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
With Opt_WarnRedundantConstraints, GHC can report which
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2312,8 +2312,6 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
-- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K)
-- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqTyVarHomo
- -- this next line checks also for coercion holes; see
- -- Note [Equalities with incompatible kinds]
= do { dflags <- getDynFlags
; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs rewrite_co1 rewrite_co2
@@ -2321,6 +2319,8 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
-- equalities, in case have x ~ (y :: ..x...)
-- #12593
-- guarantees (TyEq:OC), (TyEq:F), and (TyEq:H)
+ -- this next line checks also for coercion holes (TyEq:H); see
+ -- Note [Equalities with incompatible kinds]
; case canEqOK dflags eq_rel lhs rhs of
CanEqOK ->
do { traceTcS "canEqOK" (ppr lhs $$ ppr rhs)
@@ -2692,6 +2692,10 @@ Note that
* We track the cycle-breaker variables in inert_cycle_breakers in InertSet
* We eventually fill in the cycle-breakers, with `cbv := F a`.
No one else fills in cycle-breakers!
+* In inert_cycle_breakers, we remember the (cbv, F a) pair; that is, we
+ remember the /original/ type. The [G] F a ~ cbv constraint may be rewritten
+ by other givens (eg if we have another [G] a ~ (b,c), but at the end we
+ still fill in with cbv := F a
* This fill-in is done when solving is complete, by restoreTyVarCycles
in nestImplicTcS and runTcSWithEvBinds.
* The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is
@@ -2738,6 +2742,8 @@ Details:
(2) Our goal here is to avoid loops in rewriting. We can thus skip looking
in coercions, as we don't rewrite in coercions.
+ (There is no worry about unifying a meta-variable here: this Note is
+ only about Givens.)
(3) As we're substituting, we can build ill-kinded
types. For example, if we have Proxy (F a) b, where (b :: F a), then
@@ -2820,6 +2826,10 @@ Details:
we only want to break cycles for user-written loopy Givens, and
a CycleBreakerTv certainly isn't user-written.
+NB: This same situation (an equality like b ~ Maybe (F b)) can arise with
+Wanteds, but we have no concrete case incentivising special treatment. It
+would just be a CIrredCan.
+
-}
{-
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -273,7 +273,8 @@ data HoleSort = ExprHole Id
| ConstraintHole
-- ^ A hole in a constraint, like @f :: (_, Eq a) => ...
-- Differentiated from TypeHole because a ConstraintHole
- -- is simplified differently. See GHC.Tc.Solver.simplifyHoles.
+ -- is simplified differently. See
+ -- Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.
instance Outputable Hole where
ppr (Hole { hole_sort = ExprHole id
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -857,6 +857,10 @@ any_rewritable :: Bool -- Ignore casts and coercions
-- ORing the results of the predicates above together
-- Do not look inside casts and coercions if 'ignore_cos' is True
-- See Note [anyRewritableTyVar must be role-aware]
+--
+-- This looks like it should use foldTyCo, but that function is
+-- role-agnostic, and this one must be role-aware. We could make
+-- foldTyCon role-aware, but that may slow down more common usages.
{-# INLINE any_rewritable #-} -- this allows specialization of predicates
any_rewritable ignore_cos role tv_pred tc_pred should_expand
= go role emptyVarSet
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1989,6 +1989,11 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType
-- inside the kinds of variables it mentions. For (d) we look deeply
-- in coercions when the LHS is a tyvar (but skip coercions for type family
-- LHSs), and for (e) see Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
+--
+-- checkTypeEq is called from
+-- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
+-- case-analysis on 'lhs'
+-- * checkEqCanLHSFinish, which does not know the form of 'lhs'
checkTypeEq dflags ty_fam_ok lhs ty
= go ty
where
@@ -2047,14 +2052,15 @@ checkTypeEq dflags ty_fam_ok lhs ty
-- this slightly peculiar way of defining this means
-- we don't have to evaluate this `case` at every tyconapp
go_tc = case lhs of
- TyVarLHS {} -> \ tc tys -> if good_tc tc
- then mapM go tys >> ok
- else MTVU_Bad
+ TyVarLHS {} -> \ tc tys ->
+ if | good_tc tc -> mapM go tys >> ok
+ | otherwise -> MTVU_Bad
TyFamLHS fam_tc fam_args -> \ tc tys ->
if | tcEqTyConApps fam_tc fam_args tc tys -> MTVU_Occurs
| good_tc tc -> mapM go tys >> ok
| otherwise -> MTVU_Bad
+
-- no bother about impredicativity in coercions, as they're
-- inferred
go_co co | not (gopt Opt_DeferTypeErrors dflags)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0b4d386cc779db18e9fdb266cf76bff341fb126a
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/0b4d386cc779db18e9fdb266cf76bff341fb126a
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201112/672cb78c/attachment-0001.html>
More information about the ghc-commits
mailing list