Array shape is zero but array contains elements.

[WilliamDue]

Error replication.

The test in the following piece of code does not succeed.

-- | file: error.fut
type maybe 'a = #just a | #nothing

def two_two_three [n] (_ : [n]u8) : maybe([]i64) =
  if n == 0
  then #just []
  else #just [2, 2, 3]

entry f s =
  match two_two_three s
  case #just s' -> s'
  case #nothing -> []

-- ==
-- entry: f
-- input { "uuv" }
-- output { [2i64, 2i64, 3i64] }

When running the tests it responds with.

error.fut:
Compiling with --backend=c:
Running compiled program:
Running ./error:
Entry point: f; dataset: #0 ("[117u8, 117u8, 118u8]"):
error.fut.f.0.actual and error.fut.f.0.expected do not match:
Value #0: expected array of shape [3], got [0]

I would think the shape of the output of f should be [3] for the input "uvv". When I use the function in the REPL, I also see that the shape is [0] but the array contains elements.

[0]> let x = f "uvv"
[1]> :t x
[0]i64
[2]> x
[2, 2, 3]

Also note that when testing with the interpreter the test succeeds futhark test -i error.fut.

Version

Futhark 0.26.0 (prerelease - include info below when reporting bugs)
git: 02579635d393c46589b1df1b4177292d7fbd7c76

[athas]

The problem here is that the size of the #just constructor in the first branch (0) is also simply taken to be the size of the second branch. We do have code that looks at whether branches differ in the sizes they return, but this does not look at unresolved type variables, and in this case the full sum type is not known at the point where size mismatches are checked.

This may be a bit tricky to solve in a very nice way without restructuring how we represent sum types in the type checker, by using some kind of row type variable. There is a rather rigid solution, which would be to detect and reject these cases (which is not so difficult), which can then be worked around by the programmer by adding an explicit type annotation to the constructor usage sites.

[catvayor]

Shouldn't ?[n]. maybe ([n]t) be illegal ? For me, maybe ([n]t) doesn't witness n as it doesn't guaranty to have an array of size n.

[athas]

That's an interesting perspective that I had not considered. I don't think we ever clarified the rules for which sizes are witnessed by a sum type.

[catvayor]

As I understood witnessing, sum type should witness the intersection of every constructor witnesses.
This said, there's still an error in the typing of the ite in the example, shouldn't both branch be typed as maybe ([0]t_1) and maybe ([3]t_2) with t_2 know as being an integer type ? Then the mismatch would be detected and converted as an unknown

[athas]

Yes, there is a real bug that will need to be fixed, regardless of what we decide with witnesses.

Your intuition of sum type witnesses being the intersection of the witnesses of each constructor is fine as such. What I'm wondering is whether it is too restrictive. It would be bad if we ruled out too many useful programs. In practice, sum types are desugared to records, so we actually keep all constructors around at runtime (in a sense).