Existential constraint solving

[Shahab Tasharrofi]

I have generated a minimal program as follows that does not pass the
constraint solving phase but that I feel should pass this phase.

staload _(*anon*) = "prelude/DATS/list.dats"

typedef NatLt(n:int) = [k:nat | k < n] int(k)

typedef Tuple(ds:int, ar:int) = arrayref(NatLt(ds), ar)
typedef RI(ds:int, ar:int) = List0(Tuple(ds, ar))

fun loop {ds:pos} {ar:nat} (i:RI(ds, ar), cur_res:RI(ds, ar)) : RI(ds, ar) =
  case+ i of
    | list_nil() => cur_res
    | list_cons(row, rest) => loop(rest, cur_res)

If you run patscc on this program, you would get the following error:

311(line=10, offs=21) -- 318(line=10, offs=28): warning(3): the constraint [S2Eeqeq(S2Eexi(k$1668(4934); S2Eapp(S2Ecst(>=); S2Evar(k$1668(4934)), S2Eintinf(0)), S2Eapp(S2Ecst(<); S2Evar(k$1668(4934)), S2Evar(ds(4381))); S2Eapp(S2Ecst(int); S2Evar(k$1668(4934)))); S2Eexi(k$1669(4935); S2Eapp(S2Ecst(>=); S2Evar(k$1669(4935)), S2Eintinf(0)), S2Eapp(S2Ecst(<); S2Evar(k$1669(4935)), S2Evar(ds(4381))); S2Eapp(S2Ecst(int); S2Evar(k$1669(4935)))))] cannot be translated into a form accepted by the constraint solver.

If I am right, the constraint that is not satisfied translates to the following
human-readable constraint:

[k:int | k >= 0; k < ds] == [k:int | k >= 0; k <ds]

where [] stands for existential quantifier.

Now, looking at the program, I see that it has happened on the line
containing "list_nil() => cur_res" and since the "cur_res" is of exactly
the same type as the output type of function "loop", I believe that this
should not have happened.

However, looking at the error, what I see is a constraint that says a "k1"
which satisfies conditions "k1 >= 0" and "k1 < ds" should be equal to
"k2" that satisfies the conditions "k2 >= 0" and "k2 < ds". Thus, the
constraint is obviously not valid (while the program looks valid). I believe
that the right constraint to generate for this program should be of the
following form:
if k1 is an integer satisfying constraints k1 >= 0 and k1 < ds then
integer k2 exists such that k2 >= 0 and k2 < ds.

Please let me know what you think.

[gmhwxi]

Basically, the issue here is to show the following type equality:

NatLt(ds) = NatLt(ds)

Currently, the typechecker uses 'syntactic equality'
(no alpha-renaming) to show type equality. So it fails
to show the above type equality (because the syntax tree
for the left is different from the syntax tree for the right).

Of course, a more elaborate way can be used to show type
equality. For instance, you example can actually typecheck
in ATS1. However, I am reluctant to go this way as I would
like to encourage people to use abstract types from early on.

For instance, you code can readily typecheck after the following
modification:

abstype
Tuple (ds: int,    ar: int)