Compiler allowing invalid capacity variables

[Qata]

From my understanding of capacities, this function is incorrect, and lowerBound and upperBound are both supposed to be concrete types.

But the compiler (4.0.1) accepts this code and generates non-compiling C++ from it.

fun range(lowerBound : from, upperBound : upTo): list<int32, upTo - from> = {
    let length: int32 = cast(upTo - from)
    let mut result: a[length] = zeros()

    for i : int32 in 0i32 .. length {
        result[i] = Math:mapRange(
            i |> toFloat(),
            from |> toFloat(),
            upTo |> toFloat(),
            0.0,
            length |> toFloat()
        ) |> toInt32()
    }

    { data := result, length := cast(length) }
}

[calebh]

The above function now fails to compile with the following error:

There is a name collision between a type variable and a capacity variable named "from". Perhaps you are trying to use "from" as both a type and capacity variable?

file C:\Users\caleb\Documents\juniperproject\bugtest\test.jun, line 3 column 23 to line 3 column 27

fun range(lowerBound : from, upperBound : upTo): list<int32, upTo - from> = {
                       ^^^^

file C:\Users\caleb\Documents\juniperproject\bugtest\test.jun, line 3 column 68 to line 3 column 72

fun range(lowerBound : from, upperBound : upTo): list<int32, upTo - from> = {
                                                                    ^^^^

Note that Juniper doesn't have fully dependent types. This means that argument values cannot be used at the type level as you would see in something like Idris or Coq. In Juniper, type level integers can be demoted to value level integers, but not the other way around.