On 2010-10-27 15:01, Alan Jeffrey wrote: > a) Support for FFI bindings for dependent types (in particular > level-polymorphic types) -- I submitted a patch for this. Available here: http://code.google.com/p/agda/issues/detail?id=324 -- /NAD