[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