Do not bring visible foralls into scope in hsScopedTvs
Previously, hsScopedTvs
(and its cousin hsWcScopedTvs
) pretended
that visible dependent quantification could not possibly happen at
the term level, and cemented that assumption with an ASSERT
:
hsScopedTvs (HsForAllTy { hst_fvf = vis_flag, ... }) =
ASSERT( vis_flag == ForallInvis )
...
It turns out that this assumption is wrong. You can end up tripping
this ASSERT
if you stick it to the man and write a type for a term
that uses visible dependent quantification anyway, like in this
example:
{-# LANGUAGE ScopedTypeVariables #-}
x :: forall a -> a -> a
x = x
That won't typecheck, but that's not the point. Before the
typechecker has a chance to reject this, the renamer will try
to use hsScopedTvs
to bring a
into scope over the body of x
,
since a
is quantified by a forall
. This, in turn, causes the
ASSERT
to fail. Bummer.
Instead of walking on this dangerous ground, this patch makes GHC
adopt a more hardline stance by pattern-matching directly on
ForallInvis
in hsScopedTvs
:
hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ...
Now a
will not be brought over the body of x
at all (which is how
it should be), there's no chance of the ASSERT
failing anymore (as
it's gone), and best of all, the behavior of hsScopedTvs
does not
change. Everyone wins!
Fixes #17687 (closed).