Remove universe levels when compiling?

[GoogleCodeExporter]

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 reported on code.google.com by [email protected] on 12 Nov 2012 at 10:59

[GoogleCodeExporter]

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

Original comment by [email protected] on 13 Nov 2012 at 1:02

[GoogleCodeExporter]

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.

Original comment by nils.anders.danielsson on 13 Nov 2012 at 1:20

• Changed title: Remove universe levels when compiling?
• Changed state: Accepted
• Added labels: Compiler, Priority-Medium, Type-Enhancement

[UlfNorell]

type AgdaIO a b = IO b

At the very least we shouldn't eta expand gratuitously. Changing the definition to

type AgdaIO a = IO

should fix this particular problem.

[UlfNorell]

Turns out it's not that simple... we also create a bunch of type synonyms with too many arguments.

[jespercockx]

Now that we have --level-universe, we have a clear path to make this work (at least when this flag is enabled): we just need to remember the shape of the sort (Set, Prop, LevelUniv, ...) of type variables in the treeless syntax, and then each backend can decide what to do with those arguments (either drop them or compile them to unit). See also #4193.