Relax restrictions on required foralls
We now support RequiredTypeArguments
, forall a -> ty
.
The arrow forall a -> ty
was created as a modification of forall a. ty
. However, it has a lot of common with other types such as the normal function arrow, a -> ty
. Required foralls don't have implicit instantiation or generalization, a lot of complexity around implicit arguments disappears.
I think that forall a -> ty
should be treated as a tau-type rather than a sigma-type in GHC.
For example, given
myId :: forall a -> a -> a
myId = myId
single x = [x]
l = single myId
We want l :: [forall a -> a -> a]
. Currently, typechecking l
requires ImpredicativeTypes
. But there should be no need for Quick Look inference. Contrast this with single id
, where the type argument is implicit: it can be typed either as forall a. [a -> a]
or [forall a. a -> a]
.
Likewise, in Template Haskell we currently don't allow quantification, as this variant of T11452 shows:
{-# LANGUAGE RankNTypes, TemplateHaskell, RequiredTypeArguments, ExplicitNamespaces #-}
module T11452a where
impred :: forall a -> a -> a
impred = $$( [|| (\(type _) x -> x) :: (forall a -> a -> a) ||] )
But I think this should just work.
[Added later] One more example that I think should work:
f :: (forall a -> a) -> ()
f x = undefined x
g :: (forall a -> a) -> ()
g (undefined -> ()) = ()
f
works only when ImpredicativeTypes
are on; g
doesn't work even with this flag.