[Agda] --without-K option too restrictive?

[Nils Anders Danielsson]

On 2013-05-29 22:52, Andreas Abel wrote:
> The error comes from universe polymorphism: Agda complains about
> Level.zero not being pattern, although Level.zero is only visible in
> the debug printing -v tc.lhs.split.well-formed:20.

The --without-K check reconstructs constructor parameters, but this
information is not propagated to the pretty-printer.

-- 
/NAD