Skip to content
  • Ryan Scott's avatar
    Do not bring visible foralls into scope in hsScopedTvs · 0940b59a
    Ryan Scott authored
    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`:
    
    ```hs
        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:
    
    ```hs
    {-# 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`:
    
    ```hs
        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.
    0940b59a