On 2013-04-17 11:29, Станислав Черничкин wrote: > And I wondering, probably Agda compiler is already able to extract > type information from Haskell somehow? No. (Except that generated code is type-checked by GHC, so Agda gets information about whether GHC accepts the code or not.) -- /NAD