[Agda] Re: Agda FFI bindings

[Nils Anders Danielsson]

On 2010-09-20 14:34, Alan Jeffrey wrote:
> The source of these errors is HaskellTypes.hs -- it looks like there'd
> be an easy fix for universe-monomorphic bindings, which is to add a
> cluase to haskellType, something like:
>
> Lit (LitLevel _ _) -> "()"

This seems wrong, because there is nothing which stops an Agda program
from pattern matching on a level. I hope that we will switch to
parametric universe-polymorphism soon, but this has not happened yet.

--
/NAD