# Constraint cannot be translated into a form accepted by the constraint solver?

**URL:** <https://discourse.ats-lang.org/t/constraint-cannot-be-translated-into-a-form-accepted-by-the-constraint-solver/763>\
**Category:** Google Group\
**Created:** [April 16, 2015, 2:56am UTC](https://discourse.ats-lang.org/t/constraint-cannot-be-translated-into-a-form-accepted-by-the-constraint-solver/763 "2015-04-16T02:56:50Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 16, 2015, 2:56am UTC](https://discourse.ats-lang.org/t/constraint-cannot-be-translated-into-a-form-accepted-by-the-constraint-solver/763/1 "2015-04-16T02:56:50Z")

</div>

Hi all,

I have some code yielding the following errors:

warning(3): the constraint [S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238)))))] cannot be translated into a form accepted by the constraint solver.  
error(3): unsolved constraint: C3NSTRprop(main; S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238))))))  
error(3): unsolved constraint for var preservation  
warning(3): the constraint [S2Eeqeq(S2Eexi(p$6909(12235); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6909(12235)))); S2Eexi(p$6913(12239); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6913(12239)))))] cannot be translated into a form accepted by the constraint solver.  
error(3): unsolved constraint for var preservation  
typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.  
exit(ATS): uncaught exception: \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)

I’ve tried making the code less complex in various ways to make a simple test case, and each attempt makes the error go away (though in one case the compiler segfaulted, and in another it hit "exit(ATS): /home/hwxi/research/Postiats/git/src/pats\_typerase\_dynexp.dats: 18565 (line=816, offs=9) – 18617(line=816, offs=61): match failure.”). Is there any way I can debug this? Should I just attach the whole program?

Thanks,  
Shea

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 16, 2015, 10:25am UTC](https://discourse.ats-lang.org/t/constraint-cannot-be-translated-into-a-form-accepted-by-the-constraint-solver/763/2 "2015-04-16T10:25:26Z")

</div>

Thanks! Now I don’t get that error, I just get:

exit(ATS): /home/shlevy/src/ATS-Postiats/src/pats\_typerase\_dynexp.dats: 18567(line=820, offs=9) – 18619(line=820, offs=61): match failure.

Poking around a bit, it looks like s2exp2hnf is returning a None\_vt when only a Some\_vt is expected there, inside of a D3Earrinit. Does that mean somehow the type of the size of the array doesn’t have an HNF? The only array initialization in my code is:

var buf = @[byte]buf\_sz

where I have:

stadef buf\_sz = 10

earlier in the file.

OK, so if I replace every instance of buf\_sz with 10 it type checks. Is this somehow a bug in stadef? Or am I using it wrong?

Thanks,  
Shea\> On Apr 15, 2015, at 11:29 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:

> I think I know this one. I uploaded into Github a fix for it.
> 
> On Wednesday, April 15, 2015 at 10:56:52 PM UTC-4, Shea Levy wrote:  
> Hi all,
> 
> I have some code yielding the following errors:
> 
> warning(3): the constraint [S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238)))))] cannot be translated into a form accepted by the constraint solver.  
> error(3): unsolved constraint: C3NSTRprop(main; S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238))))))  
> error(3): unsolved constraint for var preservation  
> warning(3): the constraint [S2Eeqeq(S2Eexi(p$6909(12235); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6909(12235)))); S2Eexi(p$6913(12239); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6913(12239)))))] cannot be translated into a form accepted by the constraint solver.  
> error(3): unsolved constraint for var preservation  
> typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.  
> exit(ATS): uncaught exception: \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)
> 
> I’ve tried making the code less complex in various ways to make a simple test case, and each attempt makes the error go away (though in one case the compiler segfaulted, and in another it hit "exit(ATS): /home/hwxi/research/Postiats/git/src/pats\_typerase\_dynexp.dats: 18565 (line=816, offs=9) – 18617(line=816, offs=61): match failure.”). Is there any way I can debug this? Should I just attach the whole program?
> 
> Thanks,  
> Shea
> 
> –  
> 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/c22cae44-a9db-499f-921b-a18ea8372079%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/c22cae44-a9db-499f-921b-a18ea8372079%40googlegroups.com).

---

<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:** [April 16, 2015, 3:29am UTC](https://discourse.ats-lang.org/t/constraint-cannot-be-translated-into-a-form-accepted-by-the-constraint-solver/763/3 "2015-04-16T03:29:28Z")

</div>

I think I know this one. I uploaded into Github a fix for it.On Wednesday, April 15, 2015 at 10:56:52 PM UTC-4, Shea Levy wrote:

> Hi all,
> 
> I have some code yielding the following errors:
> 
> warning(3): the constraint [S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238)))))] cannot be translated into a form accepted by the  
> constraint solver.  
> error(3): unsolved constraint: C3NSTRprop(main;  
> S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1),  
> S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes);  
> S2Eintinf(1), S2Evar(p$6912(12238))))))  
> error(3): unsolved constraint for var preservation  
> warning(3): the constraint [S2Eeqeq(S2Eexi(p$6909(12235); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6909(12235)))); S2Eexi(p$6913(12239); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6913(12239)))))] cannot be translated into a form accepted by the  
> constraint solver.  
> error(3): unsolved constraint for var preservation  
> typechecking has failed: there are some unsolved constraints: please  
> inspect the above reported error message(s) for information.  
> exit(ATS): uncaught exception:  
> \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)
> 
> I’ve tried making the code less complex in various ways to make a simple  
> test case, and each attempt makes the error go away (though in one case the  
> compiler segfaulted, and in another it hit "exit(ATS):  
> /home/hwxi/research/Postiats/git/src/pats\_typerase\_dynexp.dats: 18565  
> (line=816, offs=9) – 18617(line=816, offs=61): match failure.”). Is there  
> any way I can debug this? Should I just attach the whole program?
> 
> Thanks,  
> Shea

---

<div class="post-metadata">

**Author:** ![Shea\_Levy](https://avatars.discourse-cdn.com/v4/letter/s/b38774/32.png) [@Shea\_Levy](https://discourse.ats-lang.org/u/Shea_Levy)\
**Post date:** [April 16, 2015, 10:32am UTC](https://discourse.ats-lang.org/t/constraint-cannot-be-translated-into-a-form-accepted-by-the-constraint-solver/763/4 "2015-04-16T10:32:04Z")

</div>

Ah, I misdiagnosed, the buf\_sz in the array initialization came from the _dynamic_ buf\_sz val I declared on the previous line, not the stadef. I opened up a github issue [1] for this.

~Shea

[1]: [Pattern match failure in pats\_typerase\_dynexp.dats · Issue #133 · githwxi/ATS-Postiats · GitHub](https://github.com/githwxi/ATS-Postiats/issues/133)\> On Apr 16, 2015, at 6:25 AM, Shea Levy [sh...@shealevy.com](mailto:sh...@shealevy.com) wrote:

> Thanks! Now I don’t get that error, I just get:
> 
> exit(ATS): /home/shlevy/src/ATS-Postiats/src/pats\_typerase\_dynexp.dats: 18567(line=820, offs=9) – 18619(line=820, offs=61): match failure.
> 
> Poking around a bit, it looks like s2exp2hnf is returning a None\_vt when only a Some\_vt is expected there, inside of a D3Earrinit. Does that mean somehow the type of the size of the array doesn’t have an HNF? The only array initialization in my code is:
> 
> var buf = @[byte]buf\_sz
> 
> where I have:
> 
> stadef buf\_sz = 10
> 
> earlier in the file.
> 
> OK, so if I replace every instance of buf\_sz with 10 it type checks. Is this somehow a bug in stadef? Or am I using it wrong?
> 
> Thanks,  
> Shea
> 
> > On Apr 15, 2015, at 11:29 PM, gmhwxi [gmh...@gmail.com](mailto:gmh...@gmail.com) wrote:
> > 
> > I think I know this one. I uploaded into Github a fix for it.
> > 
> > On Wednesday, April 15, 2015 at 10:56:52 PM UTC-4, Shea Levy wrote:  
> > Hi all,
> > 
> > I have some code yielding the following errors:
> > 
> > warning(3): the constraint [S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238)))))] cannot be translated into a form accepted by the constraint solver.  
> > error(3): unsolved constraint: C3NSTRprop(main; S2Eeqeq(S2Eexi(p$6908(12234); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6908(12234)))); S2Eexi(p$6912(12238); ; S2Eapp(S2Ecst(filedes); S2Eintinf(1), S2Evar(p$6912(12238))))))  
> > error(3): unsolved constraint for var preservation  
> > warning(3): the constraint [S2Eeqeq(S2Eexi(p$6909(12235); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6909(12235)))); S2Eexi(p$6913(12239); ; S2Eapp(S2Ecst(filedes); S2Eintinf(2), S2Evar(p$6913(12239)))))] cannot be translated into a form accepted by the constraint solver.  
> > error(3): unsolved constraint for var preservation  
> > typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.  
> > exit(ATS): uncaught exception: \_2home\_2hwxi\_2research\_2Postiats\_2git\_2src\_2pats\_error\_2esats\_\_FatalErrorExn(1025)
> > 
> > I’ve tried making the code less complex in various ways to make a simple test case, and each attempt makes the error go away (though in one case the compiler segfaulted, and in another it hit "exit(ATS): /home/hwxi/research/Postiats/git/src/pats\_typerase\_dynexp.dats: 18565 (line=816, offs=9) – 18617(line=816, offs=61): match failure.”). Is there any way I can debug this? Should I just attach the whole program?
> > 
> > Thanks,  
> > Shea
> > 
> > –  
> > 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/c22cae44-a9db-499f-921b-a18ea8372079%40googlegroups.com](https://groups.google.com/d/msgid/ats-lang-users/c22cae44-a9db-499f-921b-a18ea8372079%40googlegroups.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](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/241B3CE2-7888-47E1-8B26-6596828D8AA6%40shealevy.com](https://groups.google.com/d/msgid/ats-lang-users/241B3CE2-7888-47E1-8B26-6596828D8AA6%40shealevy.com).