PatternMatchFailure when pattern matching function argument with ability

[ThisFunctionalTom]

Normally when a function has multiple arguments one can pattern match with multiple arguments like this:

test: Nat -> Nat -> Nat
test = cases x, y -> x + y

> test 1 2

But once the second argument is an ability request I get the PatternMatchFailure from the compiler.

structural ability MyStream a where emit : a -> {MyStream a} ()

MyStream.toList : '{g, MyStream a} r -> '{g} [a]
MyStream.toList streamFunction = 'let
  handler : [a] -> Request {MyStream a} r -> [a]
  handler = cases
      acc, { emit x -> continue } -> handle !continue with handler (acc :+ x)
      acc, { r } -> acc
  handle !streamFunction with handler []

Matching just on the ability request works as expected:

MyStream.toList : '{g, MyStream a} r -> '{g} [a]
MyStream.toList streamFunction = 'let
  handler : [a] -> Request {MyStream a} r -> [a]
  handler acc = cases
      { emit x -> continue } -> handle !continue with handler (acc :+ x)
      { r } -> acc
  handle !streamFunction with handler []

[ChrisPenner]

Here's a minimal reproduction:

myHandler : Text -> Request {Abort} a -> Text
myHandler = cases
        arg, {Abort.abort -> resume} -> "a"
        arg, {x} -> "b"

Saving that resolves to just PatternMatchFailure in ucm.

Do either of @tstat or @dolio know what's happening here?

[dolio]

I'm not exactly sure why this is happening, but this is a compiler crash during type checking. It's not a unison pattern match failure. Something about how this function gets desugared is confusing the type checker. But I don't actually know what this code turns into internally.

[ChrisPenner]

Here's a really simple reproduction,

I've run into this error a couple times now and had to stare at it for a bit before realizing what I did wrong.

ability Ask a where ask : {Ask a} a

provide : a -> '{Ask a} r -> r
provide a action = 
  h = cases
        {ask -> resume} -> handle resume a with h
        r -> r
  handle !action with h

Results in just:

  PatternMatchFailure

in UCM 😢

[dolio]

My immediate guess for that example would be that the r -> r case is causing trouble, because it's supposed to be { r } -> r. The other examples don't (appear to) have that aspect, though. Do the multiple cases desugar into something similar?

[ChrisPenner]

Sorry, forgot to point out that yes, the r -> r case is definitely the problem and it should be {r} -> r, but I'd love a better error message :D

[dolio]

Yeah, it definitely shouldn't just crash the type checker. I'm just wondering what the common factor is. Or are there two bugs? :)