Skip to content

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.

Edited by Krzysztof Gogolewski
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information