[Agda] Polymorphic Unit type with FFI / IO

stvienna wiener stvienna at gmail.com
Wed Nov 9 00:11:07 CET 2016


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161109/9421dff6/attachment.html


More information about the Agda mailing list