[Git][ghc/ghc][wip/T24676] Respond to RAE

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T24676 at Glasgow Haskell Compiler / GHC


Commits:
6de7178f by Simon Peyton Jones at 2024-06-10T17:13:48+01:00
Respond to RAE

- - - - -


2 changed files:

- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Utils/Instantiate.hs


Changes:

=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -1900,10 +1900,8 @@ qlUnify ty1 ty2
        -> TcM ()
     go (TyVarTy tv) ty2
       | isMetaTyVar tv = go_kappa tv ty2
-        -- Only unify QL instantiation variables
-        -- See (UQL3) in Note [QuickLook unification]
     go ty1 (TyVarTy tv)
-      | isQLInstTyVar tv = go_kappa tv ty1
+      | isMetaTyVar tv = go_kappa tv ty1
 
     go (CastTy ty1 _) ty2 = go ty1 ty2
     go ty1 (CastTy ty2 _) = go ty1 ty2
@@ -1929,7 +1927,7 @@ qlUnify ty1 ty2
     -- We look at the multiplicity too, although the chances of getting
     -- impredicative instantiation info from there seems...remote.
     go (FunTy { ft_af = af1, ft_arg = arg1, ft_res = res1, ft_mult = mult1 })
-        (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
+       (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2, ft_mult = mult2 })
       | af1 == af2 -- Match the arrow TyCon
       = do { when (isVisibleFunArg af1) (go arg1 arg2)
            ; when (isFUNArg af1)        (go mult1 mult2)
@@ -1947,7 +1945,7 @@ qlUnify ty1 ty2
       = do { go t1a t2a; go t1b t2b }
 
     go _ _ = return ()
-
+       -- Don't look under foralls; see (UQL4) of Note [QuickLook unification]
 
     ----------------
     go_kappa kappa ty2
@@ -1991,11 +1989,11 @@ In qlUnify, if we find (kappa ~ ty), we are going to update kappa := ty.
 That is the entire point of qlUnify!   Wrinkles:
 
 (UQL1) Before unifying an instantiation variable in `go_flexi`, we must check
-  the usual unification conditions, by calling `GHC.Tc.Utils.Unify.simpleUnifyCheck`
-  In particular:
-  * 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.
-  * Level mis-match
+  the usual unification conditions, by calling `GHC.Tc.Utils.Unify.simpleUnifyCheck`.
+  For example that checks for
+    * An occurs-check
+    * Level mis-match
+    * An attempt to unify a concrete type variable with a non-concrete type.
 
 (UQL2) What if kappa and ty have different kinds?  We simply call the
   ordinary unifier and use the coercion to connect the two.
@@ -2020,6 +2018,27 @@ That is the entire point of qlUnify!   Wrinkles:
   But happily this can't happen: QL instantiation variables have level infinity,
   and we never unify a variable with a type from a deeper level.
 
+(UQL4) Should we look under foralls in qlUnify? The use-case would be
+     (forall a.  beta[qlinst] -> a)  ~  (forall a. (forall b. b->b) -> a)
+  where we might hope for
+     beta := forall b. b
+
+  But in fact we don't attempt this:
+
+  * The normal on-the-fly unifier doesn't look under foralls, so why
+    should qlUnify?
+
+  * Looking under foralls means we'd have to track the bound variables on both
+    sides.  Tiresome but not a show stopper.
+
+  * We might call the *regular* unifier (via unifyKind) under foralls, and that
+    doesn't know about those bound variables (it controls scope through level
+    numbers) so it might go totally wrong.  At least we'd have to instantaite
+    the forall-types with skolems (with level numbers).  Maybe more.
+
+  It's just not worth the trouble, we think (for now at least).
+
+
 Sadly discarded design alternative
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It is very tempting to use `unifyType` rather than `qlUnify`, killing off the


=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -431,7 +431,7 @@ right here. But note
 
 * There is little point in trying to optimise for
    - (s ~# t), because this has kind Constraint#, not Constraint, and so will not be
-               in the theta instantiated in instCalll
+               in the theta instantiated in instCall
    - (s ~~ t), becaues heterogeneous equality is rare, and more complicated.
 
 Anyway, for now we don't take advantage of these potential effects.



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6de7178f4e820ca15e70e7a15585bb923de705cf

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6de7178f4e820ca15e70e7a15585bb923de705cf
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/20240610/7fdf3c3f/attachment-0001.html>