# Understanding unsolved constraints

**URL:** <https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67>\
**Category:** Google Group\
**Created:** [August 1, 2014, 12:41pm UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67 "2014-08-01T12:41:30Z")\
**Posts on this page:** 6\
**Page:** 1

<div class="post-metadata">

**Author:** ![Alex\_Miller](https://avatars.discourse-cdn.com/v4/letter/a/e480ec/32.png) [@Alex\_Miller](https://discourse.ats-lang.org/u/Alex_Miller)\
**Post date:** [August 1, 2014, 12:41pm UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67/1 "2014-08-01T12:41:30Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [August 6, 2014, 3:15am UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67/2 "2014-08-06T03:15:22Z")

</div>

| 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.comOn Tue, Aug 5, 2014 at 2:26 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> 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.
> 
> On Tuesday, August 5, 2014 1:02:00 PM UTC-4, Brandon Barker wrote:
> 
> > 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:  
> > [ats2-lang / Wiki / Internal types](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?
> > > 
> > > –  
> > > 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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> > > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com)  
> > > [https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 5, 2014, 6:26pm UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67/3 "2014-08-05T18:26:26Z")

</div>

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.On Tuesday, August 5, 2014 1:02:00 PM UTC-4, Brandon Barker wrote:

> 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:  
> [ats2-lang / Wiki / Internal types](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?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 1, 2014, 8:33pm UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67/4 "2014-08-01T20:33:01Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [August 6, 2014, 3:37am UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67/5 "2014-08-06T03:37:39Z")

</div>

Usually such a variable is universally quantified.On Tuesday, August 5, 2014 11:15:42 PM UTC-4, Brandon Barker wrote:

> | 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  
> [brand...@gmail.com](mailto:brand...@gmail.com) \<javascript:\>
> 
> On Tue, Aug 5, 2014 at 2:26 PM, gmhwxi \<[gmh...@gmail.com](mailto:gmh...@gmail.com) \<javascript:\>\> wrote:
> 
> > 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.
> > 
> > On Tuesday, August 5, 2014 1:02:00 PM UTC-4, Brandon Barker wrote:
> > 
> > > 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:  
> > > [ats2-lang / Wiki / Internal types](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?
> > > > 
> > > > –  
> > > > 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...@googlegroups.com](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com)  
> > > > \<javascript:\>.  
> > > > Visit this group at [http://groups.google.com/group/ats-lang-users](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](https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com)  
> > > > [https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/6da6bb9c-d26a-49e0-8d34-abceeaa12f91%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [August 5, 2014, 5:01pm UTC](https://discourse.ats-lang.org/t/understanding-unsolved-constraints/67/6 "2014-08-05T17:01:59Z")

</div>

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](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?