Trying to get a dependent type working in ATS

Skip to first unread message


Jun 30, 2021, 10:12:34 PM6/30/21
to ats-lang-users
So, I'm trying to get the following code to work:
typedef tri_test2(v:int) = [un:int | 0 <= un; un+1 <= v; un == 0; v == 0] int(un)
val test2 = (0):tri_test2(0)
But I get the following error:
/tmp/patsopt_tcats_TCES3d: 196(line=6, offs=14) -- 197(line=6, offs=15): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<=); S2Eapp(S2Ecst(+); S2EVar(0->S2Eintinf(0)), S2Eintinf(1)), S2Eintinf(0)))
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_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
I am clueless as to why I keep getting this error.  What is ATS having trouble understanding here?

Hongwei Xi

Jun 30, 2021, 10:19:23 PM6/30/21
First, tri_test(0) is just:

[un:int | 0 <= un; un+1 <= 0; un == 0; 0 == 0] int(un)

Clearly, no value can be given the above type as 0 <= un and un+1 <= 0
yields a contradiction.

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
To view this discussion on the web visit


Jul 1, 2021, 8:56:13 AM7/1/21
to ats-lang-users
You're right, when I sent this message I was too tired to realize what was wrong I guess.  Thanks for the help.  :)
Reply all
Reply to author
0 new messages