[Agda] Polymorphic Unit type with FFI / IO

[G. Allais]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 801 bytes
Desc: OpenPGP digital signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20161109/3af1858f/signature.bin