[Git][ghc/ghc][wip/sand-witch/lazy-skol] Typos

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC


Commits:
b629cc6a by Simon Peyton Jones at 2024-01-12T15:51:34+00:00
Typos

Thanks @sheaf

- - - - -


1 changed file:

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


Changes:

=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -275,7 +275,7 @@ need to be careful:
 * Another similar situation arises with
     g :: forall a b. rho
     g @p @q x y = ....
-  Here again when skolemiseing `a` and `b` we must be careful to match them up
+  Here again when skolemising `a` and `b` we must be careful to match them up
   with `p` and `q`.
 
 * Note that this only matters for /checking/. We don't do inference for
@@ -325,7 +325,7 @@ Both ultimately handled by matchExpectedFunTys.
   harm to do so in both cases, but I found that (to my surprise) doing
   so caused a non-trivial (1%-ish) perf hit on the compiler.
 
-* `tcFunBindMatches` and `tcLambdaMatches` both use `matchExpectedFunTys`, and the
+* `tcFunBindMatches` and `tcLambdaMatches` both use `matchExpectedFunTys`, which
   ensures that any trailing invisible binders are skolemised; and does so deeply
   if DeepSubsumption is on.
 
@@ -348,35 +348,36 @@ Some wrinkles
 
 Some examples:
 
-*   f :: forall a b. blah
-    f @p x = rhs
-  `tcPolyCheck` calls `tcSkolmiseCompleteSig` to skolemise the signature, and then calls
-  `tcFunBindMatches` passing in [a_sk, b_sk], the skolemsed variables. The latter ultimately
-  calls `tcMatches`, and thence `tcMatchPats`.  The latter matches up the `a_sk` with `@p`,
-  and discareds the `b_sk`.
-
-*   f :: forall (a::Type) (b::a). blah
-    f @(p::b) x = rhs
-  The `tcSkolemiseCompleteSig` brings `a` and `b` into scope, bound to `a_sk` and `b_sk` resp.
-  When we `tcMatchPats` typecheckes the pattern `@(p::b)` it'll find that `b` is in scope,
-  which is a bit strange.  But it'll then unify  the kinds `Type ~ b`, which will fail as it
-  should.
-
-*   f :: Int -> forall (a::Type) (b::a). blah
-    f x  @p = rhs
+*     f :: forall a b. blah
+      f @p x = rhs
+  `tcPolyCheck` calls `tcSkolemiseCompleteSig` to skolemise the signature, and
+  then calls `tcFunBindMatches` passing in [a_sk, b_sk], the skolemsed
+  variables. The latter ultimately calls `tcMatches`, and thence `tcMatchPats`.
+  The latter matches up the `a_sk` with `@p`, and discards the `b_sk`.
+
+*     f :: forall (a::Type) (b::a). blah
+      f @(p::b) x = rhs
+  `tcSkolemiseCompleteSig` brings `a` and `b` into scope, bound to `a_sk` and `b_sk` resp.
+  When `tcMatchPats` typechecks the pattern `@(p::b)` it'll find that `b` is in
+  scope (as a result of tcSkolemiseCompleteSig) which is a bit strange.  But
+  it'll then unify the kinds `Type ~ b`, which will fail as it should.
+
+*     f :: Int -> forall (a::Type) (b::a). blah
+      f x  @p = rhs
   `matchExpectedFunTys` does shallow skolemisation eagerly, so we'll skolemise the
   forall a b.  Then `tcMatchPats` will bind [p :-> a_sk], and discard `b_sk`.
 
 * Suppose DeepSubsumption is on
     f :: forall a. a -> forall b. b -> b -> forall z. z
     f @p x @q y = rhs
-  The `tcSkolemiseCompleteSig` uses shallow skolemisation, so it only skolemises and brings
-  into scope [a :-> a_sk]. Then `matchExpectedFunTys` skolemises the forall b, because it
-  needs to expose two value arguments.  Finally `matchExpectedFunTys` concludes with deeply
-  skolemising the remaining type.
-
-  So we end up with `[p :-> a_sk, q :-> b_sk]`.  Notice that we must not deeply-skolemise
-  /first/ or we'd ge the tyvars [a_sk, b_sk, c_sk] which would not line up with the patterns.
+  The `tcSkolemiseCompleteSig` uses shallow skolemisation, so it only skolemises
+  and brings into scope [a :-> a_sk]. Then `matchExpectedFunTys` skolemises the
+  forall b, because it needs to expose two value arguments.  Finally
+  `matchExpectedFunTys` concludes with deeply skolemising the remaining type.
+
+  So we end up with `[p :-> a_sk, q :-> b_sk]`.  Notice that we must not
+  deeply-skolemise /first/ or we'd get the tyvars [a_sk, b_sk, c_sk] which would
+  not line up with the patterns [@p, x, @q, y]
 -}
 
 tcSkolemiseGeneral
@@ -560,7 +561,7 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have some 'skolems' and some 'givens', and we are
 considering whether to wrap the constraints in their scope into an
-implication.  We must /always/ so if either 'skolems' or 'givens' are
+implication.  We must /always/ do so if either 'skolems' or 'givens' are
 non-empty.  But what if both are empty?  You might think we could
 always drop the implication.  Other things being equal, the fewer
 implications the better.  Less clutter and overhead.  But we must



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

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b629cc6af7b5d3f5d569c5816c7a1cb74846d096
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/20240112/34c74bd7/attachment-0001.html>