Notes only: telescopes

This documentation-only patch fixes #17793

4 files changed, 18 insertions, 37 deletions

diff --git a/compiler/typecheck/Constraint.hs b/compiler/typecheck/Constraint.hs
index 459b45767f..aa1bfe479f 100644
--- a/compiler/typecheck/Constraint.hs
+++ b/compiler/typecheck/Constraint.hs
@@ -1175,8 +1175,16 @@ like this one:
 
 The kind of 'a' mentions 'k' which is bound after 'a'.  Oops.
 
-Knowing this means that unification etc must have happened, so it's
-convenient to detect it in the constraint solver:
+One approach to doing this would be to bring each of a, k, and b into
+scope, one at a time, creating a separate implication constraint for
+each one, and bumping the TcLevel. This would work, because the kind
+of, say, a would be untouchable when k is in scope (and the constraint
+couldn't float out because k blocks it). However, it leads to terrible
+error messages, complaining about skolem escape. While it is indeed a
+problem of skolem escape, we can do better.
+
+Instead, our approach is to bring the block of variables into scope
+all at once, creating one implication constraint for the lot:
 
 * We make a single implication constraint when kind-checking
   the 'forall' in Foo's kind, something like
@@ -1201,8 +1209,6 @@ convenient to detect it in the constraint solver:
   constraint solver a chance to make that bad-telescope test!  Hence
   the extra guard in emitResidualTvConstraint; see #16247
 
-See also TcHsType Note [Keeping scoped variables in order: Explicit]
-
 Note [Needed evidence variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Th ic_need_evs field holds the free vars of ic_binds, and all the
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 5726fc019d..bbfe6efb5d 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1701,33 +1701,8 @@ addTypeCtxt (L _ ty) thing
 %*                                                                      *
 %************************************************************************
 
-Note [Keeping scoped variables in order: Explicit]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When the user writes `forall a b c. blah`, we bring a, b, and c into
-scope and then check blah. In the process of checking blah, we might
-learn the kinds of a, b, and c, and these kinds might indicate that
-b depends on c, and thus that we should reject the user-written type.
-
-One approach to doing this would be to bring each of a, b, and c into
-scope, one at a time, creating an implication constraint and
-bumping the TcLevel for each one. This would work, because the kind
-of, say, b would be untouchable when c is in scope (and the constraint
-couldn't float out because c blocks it). However, it leads to terrible
-error messages, complaining about skolem escape. While it is indeed
-a problem of skolem escape, we can do better.
-
-Instead, our approach is to bring the block of variables into scope
-all at once, creating one implication constraint for the lot. The
-user-written variables are skolems in the implication constraint. In
-TcSimplify.setImplicationStatus, we check to make sure that the ordering
-is correct, choosing ImplicationStatus IC_BadTelescope if they aren't.
-Then, in TcErrors, we report if there is a bad telescope. This way,
-we can report a suggested ordering to the user if there is a problem.
-
-See also Note [Checking telescopes] in Constraint
-
-Note [Keeping scoped variables in order: Implicit]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Keeping implicitly quantified variables in order]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When the user implicitly quantifies over variables (say, in a type
 signature), we need to come up with some ordering on these variables.
 This is done by bumping the TcLevel, bringing the tyvars into scope,
@@ -1758,10 +1733,10 @@ There may be some surprises in here:
 
 Step 2 is necessary for two reasons: most signatures also bring
 implicitly quantified variables into scope, and solving is necessary
-to get these in the right order (see Note [Keeping scoped variables in
-order: Implicit]). Additionally, solving is necessary in order to
-kind-generalize correctly: otherwise, we do not know which metavariables
-are left unsolved.
+to get these in the right order (see Note [Keeping implicitly
+quantified variables in order]). Additionally, solving is necessary in
+order to kind-generalize correctly: otherwise, we do not know which
+metavariables are left unsolved.
 
 Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to
 kindGeneralize{All,Some,None}. Here, we have to deal with the fact that
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 63a1552932..b22897e720 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1799,7 +1799,7 @@ setImplicationStatus implic@(Implic { ic_status     = status
 
 checkBadTelescope :: Implication -> TcS Bool
 -- True <=> the skolems form a bad telescope
--- See Note [Keeping scoped variables in order: Explicit] in TcHsType
+-- See Note [Checking telescopes] in Constraint
 checkBadTelescope (Implic { ic_telescope  = m_telescope
                           , ic_skols      = skols })
   | isJust m_telescope
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 0321dadcec..ba5216b93a 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -2712,7 +2712,7 @@ datatype declarations.  This checks for
 
 See also
   * Note [Required, Specified, and Inferred for types] in TcTyClsDecls.
-  * Note [Keeping scoped variables in order: Explicit] discusses how
+  * Note [Checking telescopes] in Constraint discusses how
     this check works for `forall x y z.` written in a type.
 
 Note [Ambiguous kind vars]