Constraint solver only works with separate function in some cases

[antoyo]

Hi. It seems I sometimes need to create a separate function in order to solve a constraint. For instance, the following code:

#include "share/atspre_staload.hats"

implement main0(argc, argv) = {
    val optstring = Some("test")
    val string =
        case+ optstring of
        | Some(string) => string
        | None() => "default"
    val test = string1_append(string, "toto")
    val _ = free(test)
}

gives the following error:

unsolved constraint: C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eint(4); S2Eint(7)))

while it works with a separate function:

#include "share/atspre_staload.hats"

fun format_string(str: Option(String)): String =
    case+ str of
    | Some(string) => string
    | None() => "default"

implement main0(argc, argv) = {
    val optstring = Some("test")
    val string = format_string(optstring)
    val test = string1_append(string, "toto")
    val _ = free(test)
}

Thanks to fix this issue.

[sparverius]

No need to write a separate function. You have some choices,

1. use string_append which overloads string0_append and string1_append as it does not require the programmer to know if the strings are indexed or not.
2. use string0_append
3. use string1_append when you are certain that you are providing it with two indexed strings.
4. use type annotations in this particular example to persuade the typechecker into thinking "Oh, 4 is not equal to 7 but hey, they must know what they are doing"

In this situation, the first two options are the best because they should always work. To illustrate this point, say we have two indexed strings x and y, the options 1, 2 and 3 all work,

  val x = "hi"  : [i:int] string(i)
  val y = "hey" : [i:int] string(i)

  val test  = string_append(x, y)
  val test0 = string0_append(x, y)
  val test1 = string1_append(x, y)

  val () = (free(test);free(test0);free(test1))

However, option 3 only works when both strings are indexed,

  val x = "hi"  : string
  val y = "hey" : [i:int] string(i)

  val test  = string_append(x, y)  // works 
  val test0 = string0_append(x, y) // works 
  val test1 = string1_append(x, y) // does not work because 'x' is not an indexed string

That being said, option 4 works fine for the given example.

// Example with type annotation.
// note String is shorthand for [i:int] string(i) 

implement main0(argc, argv) = {
    val opstring = Some("test")
    val string = (
        case+ opstring of
        | Some(string) => string
        | None() => "default"
    ) : String // added type annotation here

    val test = string1_append(string, "toto")
    val _ = free(test)
}

[githwxi]

Strictly speaking, a case-expression (or if-expression) requires a type annotation unless the typechecker knows what type is to be assigned to the expression.

[antoyo]

Ah, thank you. I always forget that:

val string: String =
    case+ opstring of
    | Some(string) => string
    | None() => "default"

is not equivalent to:

val string = (
    case+ opstring of
    | Some(string) => string
    | None() => "default"
) : String