Commit d8d73d77 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Notes only: telescopes

This documentation-only patch fixes #17793
parent b157399f
Pipeline #15651 passed with stages
in 658 minutes and 55 seconds
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment