[Git][ghc/ghc][wip/cfuneqcan-refactor] Try removing (2b). Let's see what the testsuite says
Richard Eisenberg
gitlab at gitlab.haskell.org
Thu Nov 12 21:24:56 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
fa4f1058 by Richard Eisenberg at 2020-11-12T16:24:38-05:00
Try removing (2b). Let's see what the testsuite says
- - - - -
4 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -122,7 +122,7 @@ module GHC.Core.Coercion (
simplifyArgsWorker,
- badCoercionHole, badCoercionHoleCo,
+ hasCoercionHoleTy, hasCoercionHoleCo,
HoleSet, coercionHolesOfType, coercionHolesOfCo
) where
@@ -3050,9 +3050,9 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
%************************************************************************
-}
-bad_co_hole_ty :: Type -> Monoid.Any
-bad_co_hole_co :: Coercion -> Monoid.Any
-(bad_co_hole_ty, _, bad_co_hole_co, _)
+has_co_hole_ty :: Type -> Monoid.Any
+has_co_hole_co :: Coercion -> Monoid.Any
+(has_co_hole_ty, _, has_co_hole_co, _)
= foldTyCo folder ()
where
folder = TyCoFolder { tcf_view = const Nothing
@@ -3065,15 +3065,13 @@ bad_co_hole_co :: Coercion -> Monoid.Any
const2 :: a -> b -> c -> a
const2 x _ _ = x
--- | Is there a blocking coercion hole in this type? See
--- "GHC.Tc.Solver.Canonical" Note [Equalities with incompatible kinds]
-badCoercionHole :: Type -> Bool
-badCoercionHole = Monoid.getAny . bad_co_hole_ty
+-- | Is there a coercion hole in this type?
+hasCoercionHoleTy :: Type -> Bool
+hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
--- | Is there a blocking coercion hole in this coercion? See
--- GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
-badCoercionHoleCo :: Coercion -> Bool
-badCoercionHoleCo = Monoid.getAny . bad_co_hole_co
+-- | Is there a coercion hole in this coercion?
+hasCoercionHoleCo :: Coercion -> Bool
+hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
-- | A set of 'CoercionHole's
type HoleSet = UniqSet CoercionHole
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -154,7 +154,7 @@ data TypeMapX a
-- Note that there is no tyconapp case; see Note [Equality on AppTys] in GHC.Core.Type
-- | Squeeze out any synonyms, and change TyConApps to nested AppTys. Why the
--- last one? See Note [Equality on AppTys] in "GHC.Core.Type"
+-- last one? See Note [Equality on AppTys] in GHC.Core.Type
--
-- Note, however, that we keep Constraint and Type apart here, despite the fact
-- that they are both synonyms of TYPE 'LiftedRep (see #11715).
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -43,7 +43,6 @@ import GHC.Builtin.Types ( anyTypeOfKind )
import GHC.Driver.Session( DynFlags )
import GHC.Types.Name.Set
import GHC.Types.Name.Reader
-import GHC.Types.Unique.Set
import GHC.Hs.Type( HsIPName(..) )
import GHC.Data.Pair
@@ -109,7 +108,7 @@ canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
= canForAll ev pend_sc
canonicalize (CIrredCan { cc_ev = ev, cc_status = status })
- | BlockedCIS holes <- status
+{- "RAE" | BlockedCIS holes <- status
, isEmptyUniqSet holes
-- this would be a CEqCan if it weren't for the blocking hole, but that
-- block has been removed. Warp straight to canEqCanLHSHomo.
@@ -128,7 +127,7 @@ canonicalize (CIrredCan { cc_ev = ev, cc_status = status })
_ -> canIrred status ev }
-- NB: The Irred is /not/ insoluble, so the special case below
-- for insolubles (the direct call to canEqNC) does not apply.
-
+-}
| EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev)
= -- For insolubles (all of which are equalities), do /not/ flatten the arguments
-- In #14350 doing so led entire-unnecessary and ridiculously large
@@ -1034,7 +1033,7 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
-- NB: we have expanded type synonyms already
can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
| Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
- , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2 --
+ , Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
-- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
-- error messages; hence no direct match on TyConApp
, not (isTypeFamilyTyCon tc1)
@@ -2506,8 +2505,17 @@ where
noDerived G = G
noDerived _ = W
-For Wanted/Derived, the [X] constraint is "blocked" (not CEqCan, is CIrred)
-until the k1~k2 constraint solved: Wrinkle (2).
+For reasons described in Wrinkle (2) below, we want the [X] constraint to be "blocked";
+that is, it should be put aside, and not used to rewrite any other constraint,
+until the kind-equality on which it depends (namely 'co' above) is solved.
+To achieve this
+* The [X] constraint is a CIrredCan
+* With a cc_status of BlockedCIS bchs
+* Where 'bchs' is the set of "blocking coercion holes". The blocking coercion
+ holes are the free coercion holes of [X]'s type
+* When all the blocking coercion holes in the CIrredCan are filled (solved),
+ we convert [X] to a CNonCanonical and put it in the work list.
+All this is described in more detail in Wrinkle (2).
Wrinkles:
@@ -2527,8 +2535,8 @@ Wrinkles:
So, we have an invariant on CEqCan (TyEq:H) that the RHS does not have
any coercion holes. This is checked in checkTypeEq. Any equalities that
- have such an RHS are turned in CIrredCans with a BlockedCIS status. We also
- must be sure to kick out any constraints that mention coercion holes
+ have such an RHS are turned into CIrredCans with a BlockedCIS status. We also
+ must be sure to kick out any such CIrredCan constraints that mention coercion holes
when those holes get filled in, so that the unification step can now proceed.
(2a) We must now absolutely make sure to kick out any constraints that
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2058,13 +2058,19 @@ checkTypeEq dflags ty_fam_ok lhs ty
-- no bother about impredicativity in coercions, as they're
-- inferred
go_co co | not (gopt Opt_DeferTypeErrors dflags)
- , badCoercionHoleCo co = MTVU_HoleBlocker
- -- Wrinkle (4b) in "GHC.Tc.Solver.Canonical" Note [Equalities with incompatible kinds]
+ , hasCoercionHoleCo co
+ = MTVU_HoleBlocker -- Wrinkle (2) in GHC.Tc.Solver.Canonical
+ -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
+ -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for
+ -- deferred type errors.
| TyVarLHS tv <- lhs
- , tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
+ , tv `elemVarSet` tyCoVarsOfCo co
+ = MTVU_Occurs
+
-- Don't check coercions for type families; see commentary at top of function
- | otherwise = ok
+ | otherwise
+ = ok
good_tc :: TyCon -> Bool
good_tc
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fa4f10587c630b2afe51a026b81c44d2b064f719
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fa4f10587c630b2afe51a026b81c44d2b064f719
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/89d2dead/attachment-0001.html>
More information about the ghc-commits
mailing list