do-ap error in normalize.rkt

[pnwamk]

The following program in DrRacket v6.11

#lang pie

(claim inc (-> Nat Nat))
(define inc (λ (n) (add1 n)))
(claim plus (-> Nat Nat Nat))
(define plus (λ (n j) (iter-Nat n j inc)))

(check-same Nat (plus zero zero) zero)
(check-same Nat (plus 1 2) 3)
(check-same Nat (plus 40 2) 42)

(claim mult (-> Nat (-> Nat Nat)))
(define mult (λ (n) (iter-Nat n
                      (the (-> Nat Nat) (λ (m) zero))
                      (λ (times-n-1)
                        (λ (m) (plus m (times-n-1 m)))))))

(check-same Nat (mult zero zero) zero)
(check-same Nat (mult 1 0) 0)
(check-same Nat (mult 40 2) 80)

produces the error:

Repos/plt/6.11/add-on/6.11/pkgs/pie/normalize.rkt:23:2: match: no matching clause for (NEU 'NAT (N-var 'times-n-1))

which points here.

Don't have time to look into it today -- tomorrow I'll give it a look if no one has tackled it yet.

[david-christiansen]

Thanks for the report! The bug was in the evaluator for iter-Nat. When it made neutral versions, it put the step type as (Pi ((x Nat)) B), where B is the type of the base. This is the rule for which-Nat, not iter-Nat, which should be picking (Pi ((x B)) B) as its step type. This has been fixed, and a test added.