Avoid unrepresentable ForallVis/Inferred state in HsForAllTy
Currently, HsForAllTy looks like this:
data HsType pass
= HsForAllTy -- See Note [HsType binders]
{ hst_xforall :: XForAllTy pass
, hst_fvf :: ForallVisFlag -- Is this `forall a -> {...}` or
-- `forall a. {...}`?
, hst_bndrs :: [LHsTyVarBndr Specificity pass]
-- Explicit, user-supplied 'forall a {b} c'
-- see Note [Specificity in HsForAllTy]
, hst_body :: LHsType pass -- body type
}
| ...
This allows for different combinations of ForallVisFlag and Specificity. Two combinations are ForallInvis/Specified (i.e., forall a.) and ForallInvis/Inferred (i.e., forall {a}.). When ForallVis is used, however, the meaning of Specificity is less clear. What does Specified/Inferred mean in the context of visible foralls anyway? Note [Specificity in HsForAllTy] has this to say:
{- Note [Specificity in HsForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
All type variables in a `HsForAllTy` type are annotated with their
`Specificity`. The meaning of this `Specificity` depends on the visibility of
the binder `hst_fvf`:
* In an invisible forall type, the `Specificity` denotes whether type variables
are `Specified` (`forall a. ...`) or `Inferred` (`forall {a}. ...`). For more
information, see Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]
in GHC.Core.TyCo.Rep.
* In a visible forall type, the `Specificity` has no particular meaning. We
uphold the convention that all visible forall types use `Specified` binders.
-}
In practice, GHC adopts the convention that all HsForAllTys that use ForallVis will also use Specified. In other words, ForallVis/Inferred is an unrepresentable state. (You can try writing forall {a} -> in the source code, but it will be swiftly rejected.)
Unfortunately, there are many places in GHC that have to awkwardly dance around this unrepresentable state. Here is a one such place:
argf_to_spec :: ArgFlag -> Specificity
argf_to_spec Required = SpecifiedSpec
-- see Note [Specificity in HsForAllTy] in GHC.Hs.Type
argf_to_spec (Invisible s) = s
go_tv :: TyVarBinder -> LHsTyVarBndr Specificity GhcPs
go_tv (Bndr tv argf) = noLoc $ KindedTyVar noExtField
(argf_to_spec argf)
(noLoc (getRdrName tv))
(go (tyVarKind tv))
go_tv must work over TyVarBinders, which can come from either visible or invisible foralls. Because HsForAllTy uses Specificity in its LHsTyVarBndrs, however, go_tv must convert an ArgFlag to a Specificity, arbitrarily choosing to map Required to SpecifiedSpec. Eek. Search for "Note [Specificity in HsForAllTy]" to see all such places like this.
Fortunately, we don't have to live with this unrepresentable state. We can quite easily eliminate it from the AST with a little bit of refactoring. First, we introduce a HsForAllTelescope type that replaces the existing ForAllVis type:
data HsForAllTelescope pass
= HsForAllVis -- ^ A visible @forall@ (e.g., @forall a -> {...}@).
-- These do not have any notion of specificity, so we use
-- '()' as a placeholder value.
{ hsf_xvis :: XHsForAllVis pass
, hsf_vis_bndrs :: [LHsTyVarBndr () pass]
}
| HsForAllInvis -- ^ An invisible @forall@ (e.g., @forall a {b} c -> {...}@),
-- where each binder has a 'Specificity'.
{ hsf_xinvis :: XHsForAllInvis pass
, hsf_invis_bndrs :: [LHsTyVarBndr Specificity pass]
}
| XHsForAllTelescope !(XXHsForAllTelescope pass)
The key insight here is to use LHsTyVarBndr () for visible foralls (where specificity is meaningless) and to use LHsTyVarBndr Specificity for invisible foralls. Once we have HsForAllTelescope, HsForAllTy becomes:
data HsType pass
= HsForAllTy -- See Note [HsType binders]
{ hst_xforall :: XForAllTy pass
, hst_tele :: LHsForAllTelescope pass
, hst_body :: LHsType pass -- body type
}
| ...
Aside from changing the rest of GHC to accomodate this new code, that's about it. Patch incoming.