trans/vector/read-back bug
pnwamk opened this issue · 6 comments
An internal match error is produced by the pie program at the bottom of this message. It produces the following error message:
.../pie/normalize.rkt:458:2: match*: no matching clause for (list (VEC (NEU 'UNIVERSE (N-var 'Y)) (NEU 'NAT (N-iter-Nat (N-var 'n) (THE 'NAT (NEU 'NAT (N-var 'k))) (THE (PI 'n 'NAT (HO-CLOS #<procedure:...ie/normalize.rkt:18:29>)) (LAM 'x (FO-CLOS '() 'x '(add1 x))))))) (VEC:: (NEU (NEU 'UNIVERSE (N-var 'Y...
i.e. it looks like it is trying to read-back a vec:: whose type is (Vec Y blah) where blah is a neutral Nat.
The error is caused by the trans clause in the body of the inductive case in foo.
The error message goes away if trans is not used (i.e. just use the cong since the first equality in the trans is a same), or if the annotation on the first argument to trans is omitted (but I tested separately and the annotation itself seems fine/valid -- so it appears to be is some combination of the two from what I've observed).
Sorry the example isn't smaller. I tried a few but failed to recreate the error and decided to at least post a summary and what I had so far.
#lang pie
(claim succ (-> Nat Nat))
(define succ (λ (x) (add1 x)))
(claim + (-> Nat Nat Nat))
(define + (λ (x y) (iter-Nat x y succ)))
(claim * (-> Nat Nat Nat))
(define * (λ (x y) (iter-Nat x 0 (+ y))))
(claim bar
(Π ([E U]
[n Nat]
[m Nat])
(-> (Vec E n) (Vec E m)
(Vec E (+ n m)))))
(define bar
(λ (E n m xs ys)
(ind-Vec n xs
(λ (z v) (Vec E (+ z m)))
ys
(λ (k h t q)
(vec:: h q)))))
(claim baz
(Π ((A U)
(B U)
[n Nat])
(-> (-> A B)
(Vec A n)
(Vec B n))))
(define baz
(λ (A B n f v)
(ind-Vec n v
(λ (n v) (Vec B n))
vecnil
(λ (? x _ qwerty)
(vec:: (f x) qwerty)))))
(claim foo
(Π ((X U)
(Y U)
(f (-> X Y))
(j Nat)
(k Nat)
(fred (Vec X j))
(wilma (Vec X k)))
(= (Vec Y (+ j k))
(bar Y j k (baz X Y j f fred) (baz X Y k f wilma))
(baz X Y (+ j k) f (bar X j k fred wilma)))))
(define foo
(λ (X Y f j k fred wilma)
(ind-Vec j fred
(λ (j fred) (= (Vec Y (+ j k))
(bar Y j k (baz X Y j f fred) (baz X Y k f wilma))
(baz X Y (+ j k) f (bar X j k fred wilma))))
(same (baz X Y k f wilma))
(λ (n x xs IH)
(trans (the (= (Vec Y (add1 (+ n k)))
(bar Y (add1 n) k (baz X Y (add1 n) f (vec:: x xs)) (baz X Y k f wilma))
(vec:: (f x) (bar Y n k (baz X Y n f xs) (baz X Y k f wilma))))
(same (vec:: (f x) (bar Y n k (baz X Y n f xs) (baz X Y k f wilma)))))
(cong IH (the (-> (Vec Y (+ n k))
(Vec Y (add1 (+ n k))))
(λ (?) (vec:: (f x) ?)))))))))
It looks like this is happening during the cross-stage persistence bit, where the compile-time context is serialized to a first-order value, and then reconstituted. Interesting...
Are the obfuscated variable names here to keep students from cheating on homework?
More or less, yes XD
OK, I figured it out. Fix incoming once I get an appropriate regression test added.
That should do it for you. Thanks for the bug report!