Typechecking error involving Either datatype

[August Alm]

Hi!

I am fooling around with rewriting some Haskell code in ATS2 and hit a stumbling block. Consider the following snippet:

           datatype
           Either_bool (a: t0ype+, b: t0ype+, bool) =
             Left(a, b, true) of a | Right(a, b, false) of b
      
           typedef
           Either (a: t0ype+, b: t0ype+) =
             [p: bool] Either_bool(a, b, p)
        
           fun {a, b: t0ype}
           right_list (zs: List(Either(a,b))) : List(b) =
             case+ zs of
             | list_nil() => list_nil()
             | list_cons (Right(y), ws) => list_cons (y, right_list (ws))
             | list_cons (_, ws) => right_list (ws)
        
The function [right_list] does not typecheck. The error message is short but still beats me:

"unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(>=); S2EVar(8061->S2Evar(n$12946$12947(21290))), S2Eintinf(0)))
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.
exit(ATS): uncaught exception: _2usr_2lib_2ATS2_2src_2pats_error_2esats__FatalErrorExn(1025)"

From browsing through the documentation my (very unconfident) guess is that the compiler can't assert that the second case line
[list_cons (y, right_list (ws))] is a list of non-negative length; is that correct? How should the function be written? I'm a bit embarrassed to ask since a vaguely similar type-checking problem
is discussed in https://github.com/githwxi/ATS-Postiats/wiki/typechecking-errors ...

What makes the error even more mysterious to me is that the exact same code, but with [List] throughout replaced by [List0] does typecheck!!

Best wishes,
August

[gmhwxi]

If you change List(b) to List0(b), the code should typecheck.

Here is the reason:

typedef List(b) = [n:int] list(b, n)
typedef List0(b) = [n:nat] list(b, n)

list_cons : {n:nat} (a, list(a, n)) => list(a, n+1)

[Artyom Shalkhakov]

Hi August,

You could use this tool:

https://ashalkhakov.github.io/pats-ef/

to turn the error message into a structured tree. If it doesn't work for you (or the tree produced isn't that useful but you have some ideas how to fix it), you could file a bug on GitHub:

https://github.com/ashalkhakov/pats-ef

In your case, as HX already answered, the typechecker asks you to prove that the list you are consing onto has non-negative length (in expression [list_cons (y, right_list (ws))]); there's a lemma for that because we know it holds, but the typechecker typically doesn't know it.