idris2 generates invalid scheme

[kuribas]

Steps to Reproduce

Loading my records library in the repl: https://gist.github.com/kuribas/36291152663166bb1ee4b1eca7d6337f

Then printing my testx record using :exec

:exec print testx

Expected Behavior

It should print the record according to my Show instance.

Observed Behavior

It prints an error in the process buffer:

Exception: attempt to reference unbound identifier pat1C-58-8 at line 615, char 334 of /home/kristof/tmp/build/exec/_tmpchez_app/_tmpchez.ss

The generated code looks wrong:

(define Records-splitRow (lambda (arg-3 arg-4 arg-5) (if (null? arg-3) (cons (vector 0 ) (vector 0 )) (let ((e-2 (car arg-3))) (let ((e-3 (cdr arg-3))) (let ((e-10 (vector-ref arg-5 2))) (let ((e-11 (vector-ref arg-5 3))) (Records-with--splitRow-2826 (pat1C-58-8) 'erased arg-4 e-2 (pat1C-58-3) e-10 (Records-recordView (cons (cons (pat1C-58-8) (pat1C-58-3)) arg-4) e-10) e-3 e-11 arg-3))))))))

pat1C-58-8 is unbound here.

[gallais]

Interesting. Last time we had a similar error (pattern variables remaining at runtime) it was because of a use of rewrite but you don't seem to have any in your file. You do however have with which is using a similar abstraction mechanism so it could be that it comes from there.