First, I know there are some plans to clean up the error reporting format
that sound interesting, so what follows may not be entirely relevant except
in the short term, so feel free to ignore. However, documenting the
internal types used in the ATS compiler could still be useful in the long
term maintenance of the system, I would think.
I still think it is a bit hard for me to read the types though, not because
the output is ugly (I don’t think it is, anymore - maybe I got used to it),
but just because I don’t know what it all means - both the grammar of the
types and the type parameters themselves.
For instance, here are two types:
S2Eapp(S2Ecst(g1int_int_t0ype); S2Ecst(int_kind), S2Eintinf(7))
S2Eapp(S2Ecst(g0int_t0ype); S2Ecst(int_kind))
My guess is as follows:
Clearly the first is a g1int and the second is a g0int, and they are
composed of the c-type (S2Ecst — I guess this may not mean exactly
c-type) of int_kind. Additionally, a g1int requires some constraints, which
is what the S2Eintinf is; “intinf” reflects that ATS2 by default uses GMP
for infinite precision integer sorts.
So what is before the semicolon shows the name of the type, and what is
after it shows its machine representation type, and constraints follow the
comma (I probably need a bigger sample size with more complex examples).
I can’t recall what S2Eapp (or S2Eexi, not shown in this example) is at the
outer level for example.
I believe documenting these types is probably a high priority so I will
start collecting what information I can. I’ve quickly put a few things here:
https://sourceforge.net/p/ats2-lang/wiki/Internal%20types/On Friday, August 1, 2014 4:33:01 PM UTC-4, gmhwxi wrote:
S2Eintinf means an integer of infinite precision.
S2EVar(561) is a unification variable introduced by the typechecker.
S2Eintinf and S2EVar are names of some constructors introduced in
the file pats_staexp2.sats.
Say you have a function foo declared as follows:
fun foo {n:nat} (): void
If you typecheck the following line
val () = foo()
you will get a type-error message just like what you described
because the typechecker cannot figure what value n should take.
To get more informative type-error messages, you can supply
static arguments manually:
val () = foo{0}() // this one typechecks
Or you can do
val () = $showtype (foo())
to request that the type of ‘foo()’ be printed out.
If you post the ATS code involved, I should be able to say more.
A big part of the difficulty in programming with dependent types is due to
“incomprehensible” type-error messages 
On Friday, August 1, 2014 3:41:32 PM UTC-4, Alex Miller wrote:
I’ve been running into trouble where I’ll write some code, and get an
error message back that looks like
error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=);
S2EVar(561), S2Eintinf(0)))
from the compiler. Sometimes the line and column is enough to explain
what’s going on, but in this case, I’m lost. I don’t have a >=
comparison at the specified point in the program, and even with looking
at pats_intinf.{sats,dats}, I still don’t understand what an S2Eintinf
is. Is there any way to see what variable S2EVar(561) maps back to?
Is there a mapping somewhere of cryptic names (e.g. S2Eintinf) to what
source level construct they represent? How should I go about trying to
solve these sort of errors?