[Git][ghc/ghc][wip/T24676] Comments only...

[Simon Peyton Jones (@simonpj)]

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


Commits:
8f49e3f1 by Simon Peyton Jones at 2024-05-13T09:03:44+01:00
Comments only...

.. relating to deep subsumption and visible (required) foralls.
See #24696

- - - - -


1 changed file:

- compiler/GHC/Tc/Utils/Unify.hs


Changes:

=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1638,8 +1638,17 @@ Consider (1)
 We must skolemise the `forall b` before instantiating the `forall a`.
 See also Note [Deep skolemisation].
 
-Note that we /always/ use shallow subsumption in the ambiguity check.
-See Note [Ambiguity check and deep subsumption].
+Wrinkles:
+
+(DS1) Note that we /always/ use shallow subsumption in the ambiguity check.
+      See Note [Ambiguity check and deep subsumption].
+
+(DS2) Deep subsumption requires deep instantiation too.
+      See Note [The need for deep instantiation]
+
+(DS3) The interaction between deep subsumption and required foralls
+      (forall a -> ty) is a bit subtle.  See #24696 and
+      Note [Deep subsumption and required foralls]
 
 Note [Deep skolemisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1715,6 +1724,70 @@ complains.
 
 The easiest solution was to use tcEqMult in tc_sub_type_deep, and
 insist on equality. This is only in the DeepSubsumption code anyway.
+
+Note [The need for deep instantiation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this, without Quick Look, but with Deep Subsumption:
+   f :: ∀a b c. a b c -> Int
+   g :: Bool -> ∀d. d -> d
+Consider the application (f g).  We need to do the subsumption test
+
+  (Bool -> ∀ d. d->d)   <=   (alpha beta gamma)
+
+where alpha, beta, gamma are the unification variables that instantiate a,b,c,
+respectively.  We must not drop down to unification, or we will reject the call.
+Rather we must deeply instantiate the LHS to get
+
+  (Bool -> delta -> delta)   <=   (alpha beta gamma)
+
+and now we can unify to get
+
+   alpha = (->)
+   beta = Bool
+   gamma = delta -> delta
+
+Hence the call to `deeplyInstantiate` in `tc_sub_type_deep`.
+
+See typecheck/should_compile/T11305 for an example of when this is important.
+
+Note [Deep subsumption and required foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A required forall, (forall a -> ty) behaves like a "rho-type", one with no
+top-level quantification.  In particular, it is neither implicitly instantiated nor
+skolemised.  So
+
+  rid1 :: forall a -> a -> a
+  rid1 = id
+
+  rid2 :: forall a -> a -> a
+  rid2 a = id
+
+Here `rid2` wll typecheck, but `rid1` will not, because we don't implicitly skolemise
+the  type.
+
+This "no implicit subsumption nor skolemisation" applies during subsumption.
+For example
+   (forall a. a->a)  <=  (forall a -> a -> a)  -- NOT!
+does /not/ hold, because that would require implicitly skoleming the (forall a->).
+
+Note also that, in Core, `eqType` distinguishes between
+   (forall a. blah) and forall a -> blah)
+See discussion on #22762 and these Notes in GHC.Core.TyCo.Compare
+  * Note [ForAllTy and type equality]
+  * Note [Comparing visiblity]
+
+So during deep subsumption we simply stop (and drop down to equality) when we encounter
+a (forall a->).  This is a little odd:
+* Deep subsumption looks inside invisible foralls (forall a. ty)
+* Deep subsumption looks inside arrows (t1 -> t2)
+* But it does not look inside required foralls (forall a -> ty)
+
+There is discussion on #24696.  How is this implemented?
+
+* In `tc_sub_type_deep`, the calls to `topInstantiate` and `deeplyInstantiate`
+  instantiate only /invisible/ binders.
+* In `tc_sub_type_ds`, the call to `tcSkolemise` skolemises only /invisible/
+  binders.
 -}
 
 data DeepSubsumptionFlag = Deep | Shallow
@@ -1786,10 +1859,7 @@ tc_sub_type_deep unify inst_orig ctxt ty_actual ty_expected
       | otherwise   -- Revert to unification
       = do { -- It's still possible that ty_actual has nested foralls. Instantiate
              -- these, as there's no way unification will succeed with them in.
-             -- See typecheck/should_compile/T11305 for an example of when this
-             -- is important. The problem is that we're checking something like
-             --  a -> forall b. b -> b     <=   alpha beta gamma
-             -- where we end up with alpha := (->)
+             -- See Note [The need for deep instantiation]
              (inst_wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
            ; unify_wrap         <- just_unify rho_a ty_expected
            ; return (unify_wrap <.> inst_wrap) }



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8f49e3f1ec706f75e28ca79fd419821355e445ce

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/8f49e3f1ec706f75e28ca79fd419821355e445ce
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/20240513/c4996621/attachment-0001.html>