Open GoogleCodeExporter opened 9 years ago
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 dysin...@gmail.com
on 13 Nov 2012 at 1:02
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
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.
Turns out it's not that simple... we also create a bunch of type synonyms with too many arguments.
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.
Suppose you wanted to write bindings for a Haskell monad transformer:
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, sayFooT IO
:But the stdlib's IO binds to AgdaIO, which is a type synonym:
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
edg...@gmail.com
on 12 Nov 2012 at 10:59