Support generating RankN haskell types (using forall)

[anka-213]

For example, this agda code:

data MyBool : Set where
    MyTrue : MyBool
    MyFalse : MyBool
{-# COMPILE AGDA2HS MyBool #-}

exisitentialUse : (∀ (a : Set) → a → a) → MyBool
exisitentialUse f = f MyBool MyTrue
{-# COMPILE AGDA2HS exisitentialUse #-}

generates the following haskell code, which fails to compile

module Existential where

data MyBool = MyTrue | MyFalse

exisitentialUse :: (a -> a) -> MyBool
exisitentialUse f = f MyTrue

rather than the correct

module Existential where

data MyBool = MyTrue | MyFalse

exisitentialUse :: (forall a. a -> a) -> MyBool
exisitentialUse f = f MyTrue

[jespercockx]

Yes, this seems like a great feature to support and not too difficult to add! We'd just have to keep track of whether we are currently at the top-level or in a nested position when compiling a type, and generate explicit foralls when required.