[commit: ghc] master: Expand the Note on let-bound skolems (a744134)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/a74413479cf4bf84fcacf1c5f76da1c1610d208b/ghc

>---------------------------------------------------------------

commit a74413479cf4bf84fcacf1c5f76da1c1610d208b
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Sun Sep 23 15:23:09 2018 +0100

    Expand the Note on let-bound skolems


>---------------------------------------------------------------

a74413479cf4bf84fcacf1c5f76da1c1610d208b
 compiler/typecheck/TcSMonad.hs | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index db29f67..3e50569 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -2215,6 +2215,31 @@ For an example, see Trac #9211.
 See also TcUnify Note [Deeper level on the left] for how we ensure
 that the right variable is on the left of the equality when both are
 tyvars.
+
+You might wonder whether the skokem really needs to be bound "in the
+very same implication" as the equuality constraint.
+(c.f. Trac #15009) Consider this:
+
+  data S a where
+    MkS :: (a ~ Int) => S a
+
+  g :: forall a. S a -> a -> blah
+  g x y = let h = \z. ( z :: Int
+                      , case x of
+                           MkS -> [y,z])
+          in ...
+
+From the type signature for `g`, we get `y::a` .  Then when when we
+encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
+body of the lambda we'll get
+
+  [W] alpha[1] ~ Int                             -- From z::Int
+  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]
+
+Now, suppose we decide to float `alpha ~ a` out of the implication
+and then unify `alpha := a`.  Now we are stuck!  But if treat
+`alpha ~ Int` first, and unify `alpha := Int`, all is fine.
+But we absolutely cannot float that equality or we will get stuck.
 -}
 
 removeInertCts :: [Ct] -> InertCans -> InertCans