[Agda] Polymorphic Unit type with FFI / IO

[Ulf Norell]

You can also use a type synonym and inline {-# HASKELL #-}. See
Agda.Builtin.List (
https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/List.agda
)
for an example.

/ Ulf

On Wed, Nov 9, 2016 at 12:52 AM, G. Allais <guillaume.allais at ens-lyon.org>
wrote:

> Hi,
>
> I think that you need to use a different Unit on the Haskell side of
> things, one that takes a phantom argument. The following works fine
> (I compiled it using `agda --compile --no-main LUnit.agda`):
>
> --------------- LUnit.hs --------------------
> module LUnit where
>
> data Unit a = Unit
> ---------------------------------------------
>
> --------------- LUnit.agda ------------------
> module LUnit where
>
> record Unit {α} : Set α where
>   constructor unit
>
> {-# IMPORT LUnit                              #-}
> {-# COMPILED_DATA Unit LUnit.Unit LUnit.Unit  #-}
> ---------------------------------------------
>
> Best,
>
> On 09/11/16 00:11, stvienna wiener wrote:
> > Hi,
> >
> > What is the current solution to get a polymorphic Unit type working with
> > FFI / IO?
> >
> > My Code:
> > -------------------------------------------
> > record Unit {α} : Set α where
> >   constructor unit
> >
> > {-# COMPILED_DATA Unit () () #-}
> >
> > This is accepted by Agda but, of course, I get an error while compiling.
> > (Error message: Expecting one fewer argument to ‘()’).
> >
> > Best,
> > Stephan
> >
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161109/80e62089/attachment-0001.html