Skip to content

Do not bring visible foralls into scope in hsScopedTvs

Ryan Scott requested to merge wip/T17687 into master

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).

Merge request reports