[Agda] Size limit on generated code?

[Nils Anders Danielsson]

On 2014-09-27 04:39, Roly Perera wrote:
> Total compilation time was more than 30 minutes, and obviously these
> files sizes are kind of ridiculous, but at least we don't have an Agda
> bug (as such). I'm guessing there's some kind of quadratic blow up at
> play, though, or at least a nasty constant factor arising from all
> those coercions..

Agda compiles type-checked code, with all implicit arguments filled in.
In this case one or more of those arguments might be very large.

-- 
/NAD