Remove universe levels when compiling?

[UlfNorell]

From edg...@gmail.com on November 12, 2012 23:59:27

Suppose you wanted to write bindings for a Haskell monad transformer:

postulate FooT : (Set → Set) → Set → Set

{-# COMPILED_TYPE FooT <...> #-}

Now, you can't bind 'return' and '>>=' for any transformer or any monad (polymorphically), but at least one should be able to write specific instances, say 'FooT IO':

postulate return : ∀ {a} → a → FooT IO a

{-# COMPILED return (_ -> return) #-}

But the stdlib's IO binds to AgdaIO, which is a type synonym:

type AgdaIO a b = IO b

Unfortunately this results in a partially-applied type synonym in return's type, namely a -> FooT (AgdaIO ()) a, and GHC bails out with an error.

LiberalTypeSynonyms doesn't save us here, while a newtype complicates things quite a bit. Perhaps COMPILED_TYPE should be extended to allow us to drop level arguments? The obvious workaround is to give up IO polymorphism completely like it used to be, but I suppose this should be fixed properly.

I encountered this issue while helping Tim Dysinger in #agda with some bindings he was writing.

Original issue: http://code.google.com/p/agda/issues/detail?id=753

[UlfNorell]

From dysin...@gmail.com on November 12, 2012 17:02:45

The code that didn't work over the weekend was this https://github.com/dysinger/mayhem/blob/develop/src/Foreign/Haskell/Control/Monad/Trans/Resource.agda

[UlfNorell]

From nils.anders.danielsson on November 13, 2012 05:20:14

I read this as a feature request.

I'm not sure if we can remove universe levels, but if we can't, then maybe we should change Agda so that we can.

Summary: Remove universe levels when compiling?
Status: Accepted
Labels: Type-Enhancement Priority-Medium Compiler