[Git][ghc/ghc][wip/T22194-flags] Respond to Richard's review
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Mar 17 18:00:07 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
5e122c94 by Simon Peyton Jones at 2023-03-17T18:01:10+00:00
Respond to Richard's review
- - - - -
8 changed files:
- compiler/GHC/Data/Bag.hs
- compiler/GHC/Data/Maybe.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/polykinds/T14939.hs
Changes:
=====================================
compiler/GHC/Data/Bag.hs
=====================================
@@ -19,7 +19,7 @@ module GHC.Data.Bag (
isEmptyBag, isSingletonBag, consBag, snocBag, anyBag, allBag,
listToBag, nonEmptyToBag, bagToList, headMaybe, mapAccumBagL,
concatMapBag, concatMapBagPair, mapMaybeBag, unzipBag,
- mapBagM, mapBagM_,
+ mapBagM, mapBagM_, lookupBag,
flatMapBagM, flatMapBagPairM,
mapAndUnzipBagM, mapAccumBagLM,
anyBagM, filterBagM
@@ -38,6 +38,7 @@ import Data.List ( partition, mapAccumL )
import Data.List.NonEmpty ( NonEmpty(..) )
import qualified Data.List.NonEmpty as NE
import qualified Data.Semigroup ( (<>) )
+import Control.Applicative( Alternative( (<|>) ) )
infixr 3 `consBag`
infixl 3 `snocBag`
@@ -115,6 +116,16 @@ filterBagM pred (ListBag vs) = do
sat <- filterM pred (toList vs)
return (listToBag sat)
+lookupBag :: Eq a => a -> Bag (a,b) -> Maybe b
+lookupBag _ EmptyBag = Nothing
+lookupBag k (UnitBag kv) = lookup_one k kv
+lookupBag k (TwoBags b1 b2) = lookupBag k b1 <|> lookupBag k b2
+lookupBag k (ListBag xs) = foldr ((<|>) . lookup_one k) Nothing xs
+
+lookup_one :: Eq a => a -> (a,b) -> Maybe b
+lookup_one k (k',v) | k==k' = Just v
+ | otherwise = Nothing
+
allBag :: (a -> Bool) -> Bag a -> Bool
allBag _ EmptyBag = True
allBag p (UnitBag v) = p v
=====================================
compiler/GHC/Data/Maybe.hs
=====================================
@@ -35,6 +35,7 @@ import Data.Maybe
import Data.Foldable ( foldlM, for_ )
import GHC.Utils.Misc (HasCallStack)
import Data.List.NonEmpty ( NonEmpty )
+import Control.Applicative( Alternative( (<|>) ) )
infixr 4 `orElse`
@@ -47,7 +48,7 @@ infixr 4 `orElse`
-}
firstJust :: Maybe a -> Maybe a -> Maybe a
-firstJust a b = firstJusts [a, b]
+firstJust = (<|>)
-- | Takes a list of @Maybes@ and returns the first @Just@ if there is one, or
-- @Nothing@ otherwise.
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1641,9 +1641,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
What if one side is a TyVarLHS and the other is a TyFamLHS, (a ~ F tys)?
Which to put on the left? Answer:
* Put the tyvar on the left, (a ~ F tys) as this may be our only shot to unify.
-* But if we fail to unify and end up in cantMakeCanonical,
- then flip back to (F tys ~ a) because it's generally better
- to rewrite away function calls. This makes types smaller.
+* But if we fail to unify then flip back to (F tys ~ a) because it's generally
+ better to rewrite away function calls.
It's important to flip back. Consider
[W] F alpha ~ alpha
@@ -1712,9 +1711,11 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
, NomEq <- eq_rel -- See Note [Do not unify representational equalities]
, TyVarLHS tv <- lhs
= do { given_eq_lvl <- getInnermostGivenEqLevel
- ; if not (touchabilityTest given_eq_lvl tv rhs)
+ ; if not (touchabilityAndShapeTest given_eq_lvl tv rhs)
then if | Just can_rhs <- canTyFamEqLHS_maybe rhs
-> swapAndFinish ev eq_rel swapped tv can_rhs
+ -- See Note [Orienting TyVarLHS/TyFamLHS]
+
| otherwise
-> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
else
@@ -1725,14 +1726,25 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
PuFail reason
| Just can_rhs <- canTyFamEqLHS_maybe rhs
-> swapAndFinish ev eq_rel swapped tv can_rhs
+ -- See Note [Orienting TyVarLHS/TyFamLHS]
+
+ -- If we have [W] alpha[2] ~ Maybe b[3]
+ -- we can't unify (skolem-escape); but it /is/ canonical,
+ -- and hence we /can/ use it for rewriting
+ | reason `cterHasOnlyProblem` cteSkolemEscape
+ -> canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
+
| otherwise
-> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
PuOK rhs_redn _ ->
-- Success: we can solve by unification
- do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
- (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
+ do { -- Comment needed!
+ new_ev <- if isReflCo (reductionCoercion rhs_redn)
+ then return ev
+ else rewriteEqEvidence emptyRewriterSet ev swapped
+ (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn
; let tv_ty = mkTyVarTy tv
final_rhs = reductionReducedType rhs_redn
@@ -1769,7 +1781,6 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
---------------------------
-- Unification is off the table
--- Here we never have TyVarLHS ~ TyFamLHS (it is always the other way)
canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
= do { -- Do checkTypeEq to guarantee (TyEq:OC), (TyEq:F)
-- Must do the occurs check even on tyvar/tyvar equalities,
@@ -1791,8 +1802,9 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
-> TcTyVar -> CanEqLHS -- a ~ F tys
-> TcS (StopOrContinue Ct)
--- We have an equality a ~ F tys, and want to flip it to
--- (F tys ~ a), whereupon it is canonical
+-- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
+-- mentions alpha, it would not be a canonical constraint as-is.
+-- We want to flip it to (F tys ~ a), whereupon it is canonical
swapAndFinish ev eq_rel swapped lhs_tv can_rhs
= do { let lhs_ty = mkTyVarTy lhs_tv
; new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
@@ -1807,7 +1819,7 @@ swapAndFinish ev eq_rel swapped lhs_tv can_rhs
tryIrredInstead :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag
-> CanEqLHS -> TcType -> TcS (StopOrContinue Ct)
-- We have a non-canonical equality
--- We still swap it 'swapped' sayso, so that it is oriented
+-- We still swap it if 'swapped' says so, so that it is oriented
-- in the direction that the error message reporting machinery
-- expects it; e.g. (m ~ t m) rather than (t m ~ m)
-- This is not very important, and only affects error reporting.
@@ -1863,8 +1875,9 @@ Wrinkles:
and unifying alpha effectively promotes this wanted to a given. Doing so
means we lose track of the rewriter set associated with the wanted.
- In short: we must not have a co_hole in a Given, and unification
- effectively makes a Given
+ Another way to say it: we must not have a co_hole in a Given, and
+ unification effectively makes a Given. (This is not very well motivated;
+ may need to dig deeper if anything goes wrong.)
On the other hand, w is perfectly suitable for rewriting, because of the
way we carefully track rewriter sets.
@@ -2002,7 +2015,6 @@ The details depend on whether we're working with a Given or a Wanted.
Given
-----
-
We emit a new Given, [G] F a ~ cbv, equating the type family application to
our new cbv. Note its orientation: The type family ends up on the left; see
commentary on canEqTyVarFunEq, which decides how to orient such cases. No
@@ -2059,19 +2071,14 @@ and we turn this into
where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below.
Critically, we emit the two new constraints (the last two above)
-directly instead of calling unifyWanted. (Otherwise, we'd end up unifying cbv1
-and cbv2 immediately, achieving nothing.)
-Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
-unification -- which must be the next step after breaking the cycles --
-happens in the course of normal behavior of top-level
-interactions, later in the solver pipeline. We know this unification will
-indeed happen because breakTyEqCycle_maybe, which decides whether to apply
-this logic, checks to ensure unification will succeed in its final_check.
-(In particular, the LHS must be a touchable tyvar, never a type family. We don't
-yet have an example of where this logic is needed with a type family, and it's
-unclear how to handle this case, so we're skipping for now.) Now, we're
-here (including further context from our original example, from the top of the
-Note):
+directly instead of calling unifyWanted. (Otherwise, we'd end up
+unifying cbv1 and cbv2 immediately, achieving nothing.) Next, we
+unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
+unification happens immediately following a successful call to
+checkTouchableTyVarEq, in canEqCanLHSFinish_try_unification.
+
+Now, we're here (including further context from our original example,
+from the top of the Note):
instance C (a -> b)
[W] Arg (cbv1 -> cbv2) ~ cbv1
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -237,13 +237,15 @@ instance Outputable WorkList where
* *
********************************************************************* -}
-type CycleBreakerVarStack = NonEmpty [(TcTyVar, TcType)]
+type CycleBreakerVarStack = NonEmpty (Bag (TcTyVar, TcType))
-- ^ a stack of (CycleBreakerTv, original family applications) lists
-- first element in the stack corresponds to current implication;
-- later elements correspond to outer implications
-- used to undo the cycle-breaking needed to handle
-- Note [Type equality cycles] in GHC.Tc.Solver.Canonical
-- Why store the outer implications? For the use in mightEqualLater (only)
+ --
+ -- Why NonEmpty? So there is always a top element to add to
data InertSet
= IS { inert_cans :: InertCans
@@ -291,7 +293,7 @@ emptyInertCans
emptyInert :: InertSet
emptyInert
= IS { inert_cans = emptyInertCans
- , inert_cycle_breakers = [] :| []
+ , inert_cycle_breakers = emptyBag :| []
, inert_famapp_cache = emptyFunEqs
, inert_solved_dicts = emptyDictMap }
@@ -722,7 +724,7 @@ applying S(f,_) to t.
-----------------------------------------------------------------------------
Our main invariant:
- the CEqCans in inert_eqs should be a terminating generalised substitution
+ the EqCts in inert_eqs should be a terminating generalised substitution
-----------------------------------------------------------------------------
Note that termination is not the same as idempotence. To apply S to a
@@ -814,7 +816,7 @@ Main Theorem [Stability under extension]
(T3) lhs not in t -- No occurs check in the work item
-- If lhs is a type family application, we require only that
-- lhs is not *rewritable* in t. See Note [Rewritable] and
- -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
+ -- Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
AND, for every (lhs1 -fs-> s) in S:
(K0) not (fw >= fs)
@@ -849,7 +851,7 @@ The idea is that
* T3 is guaranteed by an occurs-check on the work item.
This is done during canonicalisation, in checkTypeEq; invariant
- (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
+ (TyEq:OC) of CEqCan. See also Note [EqCt occurs check] in GHC.Tc.Types.Constraint.
* (K1-3) are the "kick-out" criteria. (As stated, they are really the
"keep" criteria.) If the current inert S contains a triple that does
@@ -1811,7 +1813,7 @@ lookupCycleBreakerVar cbv (IS { inert_cycle_breakers = cbvs_stack })
-- to avoid #20231. This function (and its one usage site) is the only reason
-- that we store a stack instead of just the top environment.
| Just tyfam_app <- assert (isCycleBreakerTyVar cbv) $
- firstJusts (NE.map (lookup cbv) cbvs_stack)
+ firstJusts (NE.map (lookupBag cbv) cbvs_stack)
= tyfam_app
| otherwise
= pprPanic "lookupCycleBreakerVar found an unbound cycle breaker" (ppr cbv $$ ppr cbvs_stack)
@@ -1819,16 +1821,16 @@ lookupCycleBreakerVar cbv (IS { inert_cycle_breakers = cbvs_stack })
-- | Push a fresh environment onto the cycle-breaker var stack. Useful
-- when entering a nested implication.
pushCycleBreakerVarStack :: CycleBreakerVarStack -> CycleBreakerVarStack
-pushCycleBreakerVarStack = ([] <|)
+pushCycleBreakerVarStack = (emptyBag <|)
-- | Add a new cycle-breaker binding to the top environment on the stack.
-addCycleBreakerBindings :: [(TcTyVar, Type)] -- ^ (cbv,expansion) pairs
+addCycleBreakerBindings :: Bag (TcTyVar, Type) -- ^ (cbv,expansion) pairs
-> InertSet -> InertSet
addCycleBreakerBindings prs ics
= assertPpr (all (isCycleBreakerTyVar . fst) prs) (ppr prs) $
ics { inert_cycle_breakers = add_to (inert_cycle_breakers ics) }
where
- add_to (top_env :| rest_envs) = (prs ++ top_env) :| rest_envs
+ add_to (top_env :| rest_envs) = (prs `unionBags` top_env) :| rest_envs
-- | Perform a monadic operation on all pairs in the top environment
-- in the stack.
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -48,7 +48,7 @@ module GHC.Tc.Solver.Monad (
newWanted,
newWantedNC, newWantedEvVarNC,
newBoundEvVarId,
- unifyTyVar, reportUnifications, touchabilityTest,
+ unifyTyVar, reportUnifications, touchabilityAndShapeTest,
setEvBind, setWantedEq,
setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, newGivenEvVars,
@@ -2077,6 +2077,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
-- True <=> type families are ok on the RHS
= do { traceTcS "checkTouchableTyVarEq: simple-check wins" (ppr lhs_tv $$ ppr rhs)
; return (pure (mkReflRedn Nominal rhs)) }
+
| otherwise
= do { traceTcS "checkTouchableTyVarEq {" (ppr lhs_tv $$ ppr rhs)
; check_result <- wrapTcS (check_rhs rhs)
@@ -2125,10 +2126,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
checkTypeEq :: CtEvidence -> EqRel -> CanEqLHS -> TcType
-> TcS (PuResult () Reduction)
-- Used for general CanEqLHSs, ones that do
--- not have a touchable type variable on the LHS
---
--- For Givens, flatten to avoid an occurs-check
--- For Wanteds, don't bother
+-- not have a touchable type variable on the LHS (i.e. not unifying)
checkTypeEq ev eq_rel lhs rhs
| isGiven ev
= do { traceTcS "checkTypeEq {" (vcat [ text "lhs:" <+> ppr lhs
@@ -2137,10 +2135,9 @@ checkTypeEq ev eq_rel lhs rhs
; traceTcS "checkTypeEq }" (ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
- PuOK redn prs -> do { let prs_list = bagToList prs
- ; new_givens <- mapM mk_new_given prs_list
- ; emitWorkNC new_givens
- ; updInertTcS (addCycleBreakerBindings prs_list)
+ PuOK redn prs -> do { new_givens <- mapBagM mk_new_given prs
+ ; emitWorkNC (bagToList new_givens)
+ ; updInertTcS (addCycleBreakerBindings prs)
; return (pure redn) } }
| otherwise -- Wanted
@@ -2163,9 +2160,7 @@ checkTypeEq ev eq_rel lhs rhs
, tef_unifying = NotUnifying
, tef_fam_app = TEFA_Recurse
, tef_occurs = occ_prob }
- -- TEFA_Recurse: no point in TEFA_Break, because we would just make
- -- [W] beta[tau] ~ F ty (beta fresh)
- -- and would then unify beta in the next step. Infinite loop!
+ -- TEFA_Recurse: see Note [Don't cycle-break Wanteds when not unifying]
occ_prob = case eq_rel of
NomEq -> cteInsolubleOccurs
@@ -2207,3 +2202,44 @@ restoreTyVarCycles is
{-# SPECIALISE forAllCycleBreakerBindings_ ::
CycleBreakerVarStack -> (TcTyVar -> TcType -> TcM ()) -> TcM () #-}
+
+{- Note [Don't cycle-break Wanteds when not unifying]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consdier
+ [W] a[2] ~ Maybe (F a[2])
+
+Should we cycle-break this Wanted, thus?
+
+ [W] a[2] ~ Maybe delta[2]
+ [W] delta[2] ~ F a[2]
+
+For a start, this is dodgy because we might just unify delta, thus undoing
+what we have done, and getting an infinite loop in the solver. Even if we
+somehow prevented ourselves from doing so, is there any merit in the split?
+Maybe: perhaps we can use that equality on `a` to unlock other constraints?
+Consider
+ type instance F (Maybe _) = Bool
+
+ [G] g1: a ~ Maybe Bool
+ [W] w1: a ~ Maybe (F a)
+
+If we loop-break w1 to get
+ [W] w1': a ~ Maybe gamma
+ [W] w3: gamma ~ F a
+Now rewrite w3 with w1'
+ [W] w3': gamma ~ F (Maybe gamma)
+Now use the type instance to get
+ gamma := Bool
+Now we are left with
+ [W] w1': a ~ Maybe Bool
+which we can solve from the Given.
+
+BUT in this situation we could have rewritten the
+/original/ Wanted from the Given, like this:
+ [W] w1': Maybe Bool ~ Maybe (F (Maybe Bool))
+and that is readily soluble.
+
+In short: loop-breaking Wanteds, when we aren't unifying,
+seems of no merit. Hence TEFA_Recurse, rather than TEFA_Break,
+in `wanted_flags` in `checkTypeEq`.
+-}
\ No newline at end of file
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -152,7 +152,7 @@ import Data.List ( intersperse )
* *
************************************************************************
-Note [CEqCan occurs check]
+Note [EqCt occurs check]
~~~~~~~~~~~~~~~~~~~~~~~~~~
A CEqCan relates a CanEqLHS (a type variable or type family applications) on
its left to an arbitrary type on its right. It is used for rewriting.
@@ -268,11 +268,9 @@ data Ct
{- Note [Invariants of EqCt]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-An EqCt carries a canonical equality constraint, that satisfies these invariants:
- * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.InertSet
- * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify
+An EqCt is a canonical equality constraint. It satisfies these invariants:
* (TyEq:OC) lhs does not occur in rhs (occurs check)
- Note [CEqCan occurs check]
+ Note [EqCt occurs check]
* (TyEq:F) rhs has no foralls
(this avoids substituting a forall for the tyvar in other types)
* (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant]
@@ -284,6 +282,11 @@ An EqCt carries a canonical equality constraint, that satisfies these invariants
* (TyEq:TV) If rhs (perhaps under a cast) is also CanEqLHS, then it is oriented
to give best chance of unification happening; eg if rhs is touchable then lhs is too
Note [TyVar/TyVar orientation] in GHC.Tc.Utils.Unify
+
+These invariants ensure that the EqCts in inert_eqs constitute a
+terminating generalised substitution. See Note [inert_eqs: the inert equalities]
+in GHC.Tc.Solver.InertSet for what these words mean!
+
-}
data EqCt -- An equality constraint; see Note [Invariants of EqCt]
@@ -502,10 +505,14 @@ cteImpredicative, cteTypeFamily, cteInsolubleOccurs,
cteSkolemEscape :: CheckTyEqProblem
cteImpredicative = CTEP (bit 0) -- Forall or (=>) encountered
cteTypeFamily = CTEP (bit 1) -- Type family encountered
+
cteInsolubleOccurs = CTEP (bit 2) -- Occurs-check
-cteSolubleOccurs = CTEP (bit 3) -- Occurs-check under a type function or in a coercion
- -- must be one bit to the left of cteInsolubleOccurs
- -- See also Note [Insoluble occurs check] in GHC.Tc.Errors
+cteSolubleOccurs = CTEP (bit 3) -- Occurs-check under a type function, or in a coercion,
+ -- or in a representational equality; see
+ -- See Note [Occurs check and representational equality]
+ -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs
+ -- See also Note [Insoluble occurs check] in GHC.Tc.Errors
+
cteCoercionHole = CTEP (bit 4) -- Coercion hole encountered
cteConcrete = CTEP (bit 5) -- Type variable that can't be made concrete
-- e.g. alpha[conc] ~ Maybe beta[tv]
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -21,7 +21,7 @@ module GHC.Tc.Utils.Unify (
-- Various unifications
unifyType, unifyKind, unifyExpectedType,
uType, promoteTcType,
- swapOverTyVars, touchabilityTest,
+ swapOverTyVars, touchabilityAndShapeTest,
--------------------------------
-- Holes
@@ -2072,7 +2072,9 @@ uUnfilledVar2 :: CtOrigin
uUnfilledVar2 origin t_or_k swapped tv1 ty2
= do { cur_lvl <- getTcLevel
-- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
- ; if not (touchabilityTest cur_lvl tv1 ty2)
+ -- Here we don't know about given equalities here; so we treat
+ -- /any/ level outside this one as untouchable. Hence cur_lvl.
+ ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2)
then not_ok_so_defer
else
do { check_result <- uTypeCheckTouchableTyVarEq tv1 ty2
@@ -2260,8 +2262,9 @@ Needless to say, all there are wrinkles:
isTouchableMetaTyVar.
* In the constraint solver, we track where Given equalities occur
- and use that to guard unification in GHC.Tc.Solver.Canonical.touchabilityTest
- More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
+ and use that to guard unification in
+ GHC.Tc.Solver.Canonical.touchabilityAndShapeTest. More details in
+ Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
Historical note: in the olden days (pre 2021) the constraint solver
also used to unify only if l=n. Equalities were "floated" out of the
@@ -2276,8 +2279,8 @@ Note [TyVar/TyVar orientation]
See also Note [Fundeps with instances, and equality orientation]
where the kind equality orientation is important
-Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)?
-This is a surprisingly tricky question! This is invariant (TyEq:TV).
+Given (a ~ b), should we orient the equality as (a~b) or (b~a)?
+This is a surprisingly tricky question!
The question is answered by swapOverTyVars, which is used
- in the eager unifier, in GHC.Tc.Utils.Unify.uUnfilledVar1
@@ -2294,11 +2297,9 @@ So we look for a positive reason to swap, using a three-step test:
* Priority. If the levels are the same, look at what kind of
type variable it is, using 'lhsPriority'.
- Generally speaking we always try to put a MetaTv on the left
- in preference to SkolemTv or RuntimeUnkTv:
- a) Because the MetaTv may be touchable and can be unified
- b) Even if it's not touchable, GHC.Tc.Solver.floatConstraints
- looks for meta tyvars on the left
+ Generally speaking we always try to put a MetaTv on the left in
+ preference to SkolemTv or RuntimeUnkTv, because the MetaTv may be
+ touchable and can be unified.
Tie-breaking rules for MetaTvs:
- CycleBreakerTv: This is essentially a stand-in for another type;
@@ -2527,6 +2528,8 @@ matchExpectedFunKind hs_ty n k = go n k
uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType)
-- The check may expand type synonyms to avoid an occurs check,
-- so we must use the return type
+--
+-- Precondition: rhs is fully zonked
uTypeCheckTouchableTyVarEq lhs_tv rhs
| simpleUnifyCheck False lhs_tv rhs -- Do a fast-path check
-- False <=> See Note [Prevent unification with type families]
@@ -2580,7 +2583,8 @@ simpleUnifyCheck fam_ok lhs_tv rhs
go w && go a && go r
go (TyConApp tc tys)
| lhs_tv_is_concrete, not (isConcreteTyCon tc) = False
- | not fam_ok, isTypeFamilyTyCon tc = False
+ | not (isTauTyCon tc) = False
+ | not fam_ok, not (isFamFreeTyCon tc) = False
| otherwise = all go tys
go (AppTy t1 t2) = go t1 && go t2
go (ForAllTy {}) = False
@@ -2838,6 +2842,7 @@ checkTyEqRhs flags ty
-------------------
checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
+-- See Note [checkCo]
checkCo (TEF { tef_lhs = TyFamLHS {} }) co
= return (PuOK co emptyBag)
@@ -2852,7 +2857,7 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
-- Occurs check (can promote)
| Unifying _ lhs_tv_lvl LC_Promote <- unifying
- = do { reason <- checkFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
+ = do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfCo co)
; if cterHasNoProblem reason
then return (pure co)
else failCheckWith reason }
@@ -2864,6 +2869,66 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
| otherwise
= return (PuOK co emptyBag)
+{- Note [checkCo]
+~~~~~~~~~~~~~~~~~
+We don't often care about the contents of coercions, so checking
+coercions before making an equality constraint may be surprising.
+But there are several cases we need to be wary of:
+
+(1) When we're unifying a variable, we must make sure that the variable
+ appears nowhere on the RHS -- even in a coercion. Otherwise, we'll
+ create a loop.
+
+(2) We must still make sure that no variable in a coercion is at too
+ high a level. But, when unifying, we can promote any variables we encounter.
+
+(3) We do not unify variables with a type with a free coercion hole.
+ See (COERCION-HOLE) in Note [Unification preconditons].
+
+
+Note [Promotion and level-checking]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+"Promotion" happens when we have this:
+
+ [W] w1: alpha[2] ~ Maybe beta[4]
+ [W] w2: alpha[2] ~ Maybe (F gamma beta[4])
+
+In `w1` we must NOT unify alpha := Maybe beta, because beta
+may turn out to stand for a type involving some inner skolem.
+Yikes! Skolem-escape. So instead we /promote/ beta, like this:
+
+ beta[4] := beta'[2]
+ [W] w1: alpha[2] ~ Maybe beta'[2]
+
+Now we can unify alpha := Maybe beta', which might unlock other
+constraints. But if some other constraint wants to unify beta with a
+nested skolem, it'll get stuck with a skolem-escape error.
+
+In `w2`, it may or may not be the case that `beta` is level 2; suppose
+we later discover gamma := Int, and type instance F Int _ = Int.
+So we promote the entire funcion call:
+
+ [W] w2': alpha[2] ~ Maybe gamma[2]
+ [W] w3: gamma[2] ~ F gamma beta[4]
+
+Now we can unify alpha := Maybe gamma, which is a Good Thng.
+
+Wrinkle (W1)
+
+There is an important wrinkle: /all this only applies when unifying/.
+For example, suppose we have
+ [G] a[2] ~ Maybe b[4]
+where 'a' is a skolem. This Given might arise from a GADT match, and
+we can absolutely use it to rewrite locally. In fact we must do so:
+that is how we exploit local knowledge about the outer skolem a[2].
+This applies equally for a Wanted [W] a[2] ~ Maybe b[4]. Using it for
+local rewriting is fine. (It's not clear to me that it is /useful/,
+but it's fine anyway.)
+
+So we only do the level in checkTyVar when /unifying/ not for skolems
+(or untouchable unification variables).
+-}
+
-------------------
checkTyConApp :: TyEqFlags a
-> TcType -> TyCon -> [TcType]
@@ -2947,6 +3012,8 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
---------------------
check_tv NotUnifying lhs_tv
+ -- We need an occurs-check here, but no level check
+ -- See Note [No level-check or promotion when not unifying]
| occursCheckTv lhs_tv occ_tv
= failCheckWith (cteProblem occ_prob)
| otherwise
@@ -2955,7 +3022,13 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
check_tv (Unifying info lvl LC_Promote) lhs_tv
= do { mb_done <- isFilledMetaTyVar_maybe occ_tv
; case mb_done of
- Just {} -> success -- Already promoted; job done
+ Just {} -> success
+ -- Already promoted; job done
+ -- Example alpha[2] ~ Maybe (beta[4], beta[4])
+ -- We promote the first occurrence, and then encounter it
+ -- a second time; we don't want to re-promote it!
+ -- Remember, the entire process started with a fully zonked type
+
Nothing -> check_unif info lvl LC_Promote lhs_tv }
check_tv (Unifying info lvl prom) lhs_tv
= check_unif info lvl prom lhs_tv
@@ -3004,7 +3077,7 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
new_lvl = lhs_tv_lvl `minTcLevel` lvl_occ
-- c[conc,3] ~ p[tau,2]: want to clone p:=p'[conc,2]
-- c[tau,2] ~ p[tau,3]: want to clone p:=p'[tau,2]
- ; reason <- checkFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
+ ; reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl (tyCoVarsOfType (tyVarKind occ_tv))
; if cterHasNoProblem reason -- Successfully promoted
then do { new_tv_ty <- promote_meta_tyvar new_info new_lvl occ_tv
; okCheckRefl new_tv_ty }
@@ -3012,13 +3085,13 @@ checkTyVar (TEF { tef_lhs = lhs, tef_unifying = unifying, tef_occurs = occ_prob
| otherwise = pprPanic "promote" (ppr occ_tv)
-------------------------
-checkFreeVars :: CheckTyEqProblem -- Occurs check problem
- -> TcTyVar -> TcLevel
- -> TyCoVarSet -> TcM CheckTyEqResult
+checkPromoteFreeVars :: CheckTyEqProblem -- What occurs check problem to report
+ -> TcTyVar -> TcLevel
+ -> TyCoVarSet -> TcM CheckTyEqResult
-- Check this set of TyCoVars for
-- (a) occurs check
-- (b) promote if necessary, or report skolem escape
-checkFreeVars occ_prob lhs_tv lhs_tv_lvl vs
+checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl vs
= do { oks <- mapM do_one (nonDetEltsUniqSet vs)
; return (mconcat oks) }
where
@@ -3059,11 +3132,11 @@ promote_meta_tyvar info dest_lvl occ_tv
-------------------------
-touchabilityTest :: TcLevel -> TcTyVar -> TcType -> Bool
+touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
-- This is the key test for untouchability:
-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
-- and Note [Solve by unification] in GHC.Tc.Solver.Interact
-touchabilityTest given_eq_lvl tv rhs
+touchabilityAndShapeTest given_eq_lvl tv rhs
| MetaTv { mtv_info = info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
, checkTopShape info rhs
= tv_lvl `deeperThanOrSame` given_eq_lvl
=====================================
testsuite/tests/polykinds/T14939.hs
=====================================
@@ -12,10 +12,8 @@ newtype Frí (cls::Type -> Constraint) :: (Type -> Alg cls Type) where
Frí :: { with :: forall x. cls x => (a -> x) -> x }
-> Frí cls a
-{-
data AlgCat (cls::Type -> Constraint) :: Cat (Alg cls Type) where
AlgCat :: (cls a, cls b) => (a -> b) -> AlgCat cls a b
leftAdj :: AlgCat cls (Frí cls a) b -> (a -> b)
leftAdj (AlgCat f) a = undefined
--}
\ No newline at end of file
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e122c94f4828f6bd1da7e11b2e3cd4cd61e4965
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5e122c94f4828f6bd1da7e11b2e3cd4cd61e4965
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/20230317/2584cc45/attachment-0001.html>
More information about the ghc-commits
mailing list