@rossberg @DCupello1 While trying to produce a well-typed animated IL output, I came to the realisation that with the current typechecker, because term-level equality information in premises is not kept track of during TC, "valid" programs can fail to be typed. For example,
syntax shape = Rect | Circ
syntax size(shape)
syntax size(Rect) = (int, int)
syntax size(Circ) = int
def $area(shape, size(shape)) : int
def $area(Rect, (w, h)) = $(w * h)
def $area(Circ, r) = $(3 * r^2)
;; def $area(sh, r) = $(3 * r^2)
;; -- if sh = Circ
This program is fine. But if we instead use the commented out lines in lieu of the last function clause, it won't typecheck because it doesn't know sh = Circ in TC. From the last clause to the commented line is a common transformation that I use during animation.
Similarly, I think the same issue will manifest itself if I run the middle-end, which includes a pass to remove non-linear variables in patterns. It will similarly introduce equalities in premises, which I think will break typechecking. So the extended sample program is:
syntax shape = Rect | Circ
syntax size(shape)
syntax size(Rect) = (int, int)
syntax size(Circ) = int
def $area(shape, size(shape)) : int
def $area(Rect, (w, h)) = $(w * h)
def $area(Circ, r) = $(3 * r^2)
syntax size2(shape, shape)
syntax size2(Circ, Circ) = (int, int)
syntax size2(Rect, Rect) = ((int, int), (int, int))
def $size2to1(shape, size2(shape, shape)) : (size(shape), size(shape))
def $size2to1(Circ, (sz_1, sz_2)) = (sz_1, sz_2)
def $size2to1(Rect, (sz_1, sz_2)) = (sz_1, sz_2)
def $area2(shape_1, shape_2, size2(shape_1, shape_2)) : int
def $area2(shape, shape, sz) = $($area(shape, sz_1) + $area(shape, sz_2))
-- if $size2to1(shape, sz) = (sz_1, sz_2)
I expected it to fail in $area2 when we deduplicate shape in the pattern. But it fails much earlier:
╰─$ ./spectec -l -ll area.spectec --typefamily-removal --print-final-il 1 ↵
== Parsing...
== Elaboration...
== IL Validation...
== Running pass typefamily-removal...
== IL Validation after pass typefamily-removal...
area.spectec:7.18-7.23: (after pass typefamily-removal) validation error: case's type does not match expected type `int`
I haven't been able to debug it to see where the problem lies. But the more high-level question is that, in general, is our typechecking algorithm powerful enough to support these rather aggressive middle-end IL->IL passes?
@rossberg @DCupello1 While trying to produce a well-typed animated IL output, I came to the realisation that with the current typechecker, because term-level equality information in premises is not kept track of during TC, "valid" programs can fail to be typed. For example,
This program is fine. But if we instead use the commented out lines in lieu of the last function clause, it won't typecheck because it doesn't know
sh = Circin TC. From the last clause to the commented line is a common transformation that I use during animation.Similarly, I think the same issue will manifest itself if I run the middle-end, which includes a pass to remove non-linear variables in patterns. It will similarly introduce equalities in premises, which I think will break typechecking. So the extended sample program is:
I expected it to fail in
$area2when we deduplicateshapein the pattern. But it fails much earlier:I haven't been able to debug it to see where the problem lies. But the more high-level question is that, in general, is our typechecking algorithm powerful enough to support these rather aggressive middle-end IL->IL passes?