[Git][ghc/ghc][wip/T24676] Add more Notes
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Wed May 15 21:34:00 UTC 2024
Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC
Commits:
2eaed087 by Simon Peyton Jones at 2024-05-15T22:33:26+01:00
Add more Notes
- - - - -
3 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -729,7 +729,7 @@ tcInstFun do_ql inst_final fun_ctxt tc_fun fun_sigma rn_args
-- Fill in kappa := nu_1 -> .. -> nu_n -> res_nu
-- NB: kappa is uninstantiated ('go' already checked that)
; kind_co <- unifyKind Nothing liftedTypeKind (tyVarKind kappa)
- -- unifyKind: see (UQL1) in Note [Actual unification during QuickLook]
+ -- unifyKind: see (UQL3) in Note [Actual unification during QuickLook]
; liftZonkM (writeMetaTyVar kappa (mkCastTy fun_ty' kind_co))
; let co_wrap = mkWpCastN (mkGReflLeftCo Nominal fun_ty' kind_co)
@@ -1790,9 +1790,11 @@ which has no free instantiation variables, so we can QL-unify
---------------------
qlUnify :: Delta -> TcType -> TcType -> TcM ()
--- Unify ty1 with ty2, unifying only instantiation variables in delta
--- (it never unifies ordinary unification variables)
+-- Unify ty1 with ty2, unifying /only/ instantiation variables in delta
+-- (it /never/ unifies ordinary unification variables)
-- It never produces errors, even for mis-matched types
+-- It may return without having made the types equal, of course;
+-- it just makes best efforts.
qlUnify delta ty1 ty2
= assertPpr (not (isEmptyVarSet delta)) (ppr delta $$ ppr ty1 $$ ppr ty2) $
-- Only called with a non-empty delta
@@ -1872,7 +1874,7 @@ qlUnify delta ty1 ty2
----------------
go_flexi (_,bvs2) kappa ty2 -- ty2 is zonked
- | -- See Note [Actual unification during QuickLook]
+ | -- See Note [Actual unification during QuickLook] (UQL1)
let ty2_tvs = shallowTyCoVarsOfType ty2
, not (ty2_tvs `intersectsVarSet` bvs2)
-- Can't instantiate a delta-var to a forall-bound variable
@@ -1883,7 +1885,8 @@ qlUnify delta ty1 ty2
= do { let kappa_kind = tyVarKind kappa
ty2_kind = typeKind ty2
; kinds_ok <- go_kinds kappa_kind ty2_kind
- ; when kinds_ok $
+ ; when kinds_ok $ -- If kinds_ok is False, we simply no-op
+ -- See Note [Actual unification during QuickLook] (UQL2)
do { traceTc "qlUnify:update" $
hang (ppr kappa <+> dcolon <+> ppr kappa_kind)
2 (text ":=" <+> ppr ty2 <+> dcolon <+> ppr ty2_kind)
@@ -1893,6 +1896,7 @@ qlUnify delta ty1 ty2
= return () -- Occurs-check or forall-bound variable
go_kinds :: TcKind -> TcKind -> TcM Bool
+ -- See Note [Actual unification during QuickLook] (UQL2)
go_kinds kind1 kind2
| kind1 `tcEqType` kind2 = return True
| otherwise = do { qlUnify delta kind1 kind2
@@ -1907,44 +1911,57 @@ qlUnify delta ty1 ty2
In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
That is the entire point of qlUnify! Wrinkles:
-* We must not unify with anything bound by an enclosing forall; e.g.
- (forall a. kappa -> Int) ~ forall a. a -> Int)
- That's tracked by the 'bvs' arg of 'go'.
-
-* We must not make an occurs-check; we use occCheckExpand for that.
-
-* checkTypeEq also checks for various other things, including
- - foralls, and predicate types (which we want to allow here)
- - type families (relates to a very specific and exotic performance
- question, that is unlikely to bite here)
- - blocking coercion holes
- After some thought we believe that none of these are relevant
- here
-
-* What if kappa and ty have different kinds? We solve that problem by
- calling unifyKind, producing a coercion perhaps emitting some deferred
- equality constraints. That is /different/ from the approach we use in
- the main constraint solver for heterogeneous equalities; see Note
- [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
-
- Why different? Because:
- - We can't use qlUnify to solve the kind constraint because qlUnify
- won't unify ordinary (non-instantiation) unification variables.
- (It would have to worry about lots of things like untouchability
- if it did.)
- - qlUnify can't give up if the kinds look un-equal because that would
- mean that it might succeed some times (when the eager unifier
- has already unified those kinds) but not others -- order
- dependence.
- - We can't use the ordinary unifier/constraint solver instead,
- because it doesn't unify polykinds, and has all kinds of other
- magic. qlUnify is very focused.
-
-Wrinkles
-(UQL1) .. todo ...
-
- TL;DR Calling unifyKind seems like the lesser evil.
- -}
+(UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
+ the usual unification conditions: see `GHC.Tc.Utils.Unify.simpleUnifyCheck`
+ In particular:
+ * We must not unify with anything bound by an enclosing forall; e.g.
+ (forall a. kappa -> Int) ~ forall a. a -> Int)
+ That's tracked by the 'bvs' arg of 'go'.
+
+ * We must not make an occurs-check; we use occCheckExpand for that.
+
+ * We must not unify a concrete type variable with a non-concrete type.
+
+ `simpleUnifyCheck` also checks for various other things, including
+ - foralls; but we specifically *want* to unify foralls here!
+ - level mis-match; but instantiation variables are at the innermoest
+ level anyway, so this would always succeed
+ - type families; relates to a very specific and exotic performance
+ question, that is unlikely to bite here
+
+(UQL2) What if kappa and ty have different kinds? So we:
+ * Check to see if the kinds are already the same
+ * If not, use qlUnify to unify them, and
+ * Then check again for equality
+ We insist on actual equality, without any casts. The whole point of
+ qlUnify is to impredicatively unify (kappa := forall a. blah). It is
+ no good to unify (kappa := (forall a.blah) |> co) because we can't
+ use that casted polytype.
+
+ There is a small worry that we might have
+ qlUnify( (kappa :: alpha), (forall a. a->a :: Type) )
+ where `alpha` is a regular unification variable, not an instantiation
+ variable; so qlUnify won't unify it, and hence won't unify `kappa`.
+ But maybe `alpha` turns out to be Type anyway, so it'd be fine. But
+ we are very wary about unifying non-instantiation variables here; see
+ wrinkle (UQL3). So there is a remote danger of order dependence; whether
+ Quick Look succeeds depends on when `alpha` gets unified.
+
+(UQL3) qlUnify (and Quick Look generally) is very careful only to unify
+ instantiation variables, not regular unification variables. Why?
+ Because instantiation variables don't really have a settled level yet;
+ see Note [Quick Look at value arguments] wrinkle (QLA6). So we should be
+ worried that we might unify
+ alpha[1] := Maybe kappa[??]
+ and later this kappa turns out to be a level-2 variable, and we have committed
+ a skolem-escape error. Boo!
+
+ Solution: Quick Look only unifies instantiation variables.
+
+ Small exception: In the IVAR rule we want (tyVarKind kappa ~ liftedTypeKind),
+ and that cannot possibly cause skolem escape, so do allow regular unification
+ for this case, via the call to `unifyKind`.
+-}
{- *********************************************************************
* *
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -50,7 +50,7 @@ module GHC.Tc.Solver.Monad (
newWanted,
newWantedNC, newWantedEvVarNC,
newBoundEvVarId,
- unifyTyVar, reportUnifications, touchabilityAndShapeTest,
+ unifyTyVar, reportUnifications,
setEvBind, setWantedEq,
setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, emitNewGivens,
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -3524,8 +3524,9 @@ touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
-- True <=> touchability and shape are OK
touchabilityAndShapeTest given_eq_lvl tv rhs
| MetaTv { mtv_info = info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
+ , tv_lvl `deeperThanOrSame` given_eq_lvl
, checkTopShape info rhs
- = tv_lvl `deeperThanOrSame` given_eq_lvl
+ = True
| otherwise
= False
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2eaed0877cb0a3d746489f0ea59aebd603240aa8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2eaed0877cb0a3d746489f0ea59aebd603240aa8
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/20240515/878138be/attachment-0001.html>
More information about the ghc-commits
mailing list