Confusing type error in variant pattern match

[LightAndLight]

Example

$ cat test.ipso
test : Array a -> Bool
test items =
  case array.find (\_ -> false) of
    None () -> false
    Some _ -> true

$ ipso --check test.ipso
test.ipso:4:5: error: expected kind "Type", got kind "Row"
  |
4 |     None () -> false
  |     ^

The mistake is that I forgot to pass the array argument to array.find, so I'm trying to pattern match on a function Array a -> (| Some : a, None : () |).

If the scrutinee determines the type of the pattern, then the type error should be:

test.ipso:4:5: error: expected type "Array a -> (| Some : a, None : () |)", got type "(| None : (), r |)"
  |
4 |     None () -> false
  |     ^

[LightAndLight]

A similar issue:

$ cat test.ipso
fn : (| Some : a, None : () |) -> String
fn x =
  case x of
    Nothing () -> "Nothing"
    Just a -> "Just"

$ ipso --check test.ipso
test.ipso:4:5: error: expected type "(| Some : a, None : () |)", got type "(| Nothing : ?3, Some : a, None : (), ?5 |)"
  |
4 |     Nothing () -> "Nothing"
  |     ^

I think I'd expect the error to be:

test.ipso:4:5: error: expected type "(| Some : a, None : () |)", got type "(| Nothing : ?3, ?5 |)"
  |
4 |     Nothing () -> "Nothing"
  |     ^

That is to say: Nothing is not a valid constructor for this variant.