support for scoped type variables

[jwiegley]

The following definition compiles in Agda (please ignore the lack of correctness for now):

{-# TERMINATING #-}
survey : {a : Set} → (Zipper a -> Zipper a) -> List a -> List a
survey {a} f = maybe [] go ∘ fromList
  where
    go : Zipper a → List a
    go z = let z' = f z in maybe (unzipper z') go (right z')
{-# COMPILE AGDA2HS survey #-}

But the resulting Haskell will not compile because of mismatched type variables:

survey :: (Zipper a -> Zipper a) -> [a] -> [a]
survey f = maybe [] go . fromList
  where
    go :: Zipper a -> [a]
    go z = maybe (unzipper (f z)) go (right (f z))

It should of course be, with ScopedTypeVariables enabled:

survey :: forall a. (Zipper a -> Zipper a) -> [a] -> [a]
survey f = maybe [] go . fromList
  where
    go :: Zipper a -> [a]
    go z = maybe (unzipper (f z)) go (right (f z))