Understanding unsolved constraints

[Alex Miller]

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?

[gmhwxi]

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 :(

[Brandon Barker]

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/

[gmhwxi]

g0int and g1int are defined in basic_sta.sats

For S2Eapp and S2Eexi, please see pats_staexp2.sats.

Basically, S2Eapp is used to for forming an application term; S2Eexi
for forming an existentially quantified type.

Trying to use $showtype to relate such static constructs to concrete syntax
is good way to explore ATS in depth.

[Brandon Barker]

  | S2Evar of s2var // variable

  | S2EVar of s2Var // existential variable

I don't understand the comments; does this imply S2Evar (lower case) is a variable associated with a universal quantifier, or something else?

Brandon Barker
brandon...@gmail.com

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com.

[gmhwxi]

Usually such a variable is universally quantified.