proof search for a view in array fails

[Chris Double]

With the following code:

fun test {l:agz}(pf: !array_v(int, l, 2)| p: ptr l): void = let
prval (pf_x, pf_xs) = array_v_uncons(pf)
prval (pf_x1, pf_xs1) = array_v_uncons(pf_xs)
val () = !p := 0
val p2 = ptr1_succ<int>(p)
val () = !p2 := 0
prval () = pf_xs := array_v_cons(pf_x1, pf_xs1)
prval () = pf := array_v_cons(pf_x, pf_xs)
in () end

I get an error in the "!p2 := 0" line saying it can't find the proof
search for the assignment to 'p2' failed. Shouldn't that be the 'pf_1'
proof? What am I doing wrong?

--
http://bluishcoder.co.nz

[Artyom Shalkhakov]

While I can't answer your question, this works:

https://glot.io/snippets/ex2t763amv

(I guess you're well aware it would have worked, but I decided to post it nevertheless. This style is clumsy/difficult to follow, but it works.)

 

--
http://bluishcoder.co.nz

[gmhwxi]

I took a look at the source code of the typechecker.
There was a missing case. Now this issue has been fixed.
Changes will go into the next release. Thanks!