<div dir="ltr">You can also use a type synonym and inline {-# HASKELL #-}. See<div>Agda.Builtin.List (<a href="https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/List.agda">https://github.com/agda/agda/blob/master/src/data/lib/prim/Agda/Builtin/List.agda</a>)</div><div>for an example.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Nov 9, 2016 at 12:52 AM, G. Allais <span dir="ltr">&lt;<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I think that you need to use a different Unit on the Haskell side of<br>
things, one that takes a phantom argument. The following works fine<br>
(I compiled it using `agda --compile --no-main LUnit.agda`):<br>
<br>
--------------- LUnit.hs --------------------<br>
module LUnit where<br>
<br>
data Unit a = Unit<br>
------------------------------<wbr>---------------<br>
<br>
--------------- LUnit.agda ------------------<br>
module LUnit where<br>
<span class=""><br>
record Unit {α} : Set α where<br>
  constructor unit<br>
<br>
</span>{-# IMPORT LUnit                              #-}<br>
{-# COMPILED_DATA Unit LUnit.Unit LUnit.Unit  #-}<br>
------------------------------<wbr>---------------<br>
<br>
Best,<br>
<div><div class="h5"><br>
On 09/11/16 00:11, stvienna wiener wrote:<br>
&gt; Hi,<br>
&gt;<br>
&gt; What is the current solution to get a polymorphic Unit type working with<br>
&gt; FFI / IO?<br>
&gt;<br>
&gt; My Code:<br>
&gt; ------------------------------<wbr>-------------<br>
&gt; record Unit {α} : Set α where<br>
&gt;   constructor unit<br>
&gt;<br>
&gt; {-# COMPILED_DATA Unit () () #-}<br>
&gt;<br>
&gt; This is accepted by Agda but, of course, I get an error while compiling.<br>
&gt; (Error message: Expecting one fewer argument to ‘()’).<br>
&gt;<br>
&gt; Best,<br>
&gt; Stephan<br>
&gt;<br>
&gt;<br>
</div></div>&gt; ______________________________<wbr>_________________<br>
&gt; Agda mailing list<br>
&gt; <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
&gt; <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
&gt;<br>
<br>
<br>______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>