Ability matching fails on functions wrapped in other structures

[dfreeman]

It seems like the typechecker is better able to line up expected vs actual abilities on a delayed computation used directly than it is when that same computation is wrapped in any other type.

The functions takesOne and takesMany below both accept computations that require {g, Ask ('{g} ())}, but as it says on the tin, takesMany accepts a list rather than a single computation. The typechecker is happy with takesOne x, but rejects takesMany [x]:

takesOne : '{g, Ask ('{g} ())} () -> ()
takesOne x = bug "not implemented"

takesMany : ['{g, Ask ('{g} ())} ()] -> ()
takesMany x = bug "not implemented"

go : '{g, Ask ('{g} ())} () -> ()
go x =
  takesOne x -- succeeds
  takesMany [x] -- fails

I found an ability mismatch when checking the application
  
     10 |   takesMany [x] -- fails
  
  
  When trying to match [Unit ->{𝕖49, g31, Ask (Unit ->{g31} Unit)} Unit] with [Unit ->{g41, Ask
  (Unit ->{g41} Unit)} Unit] the left hand side contained extra abilities: {𝕖49, g31}

Notably, if I drop the type annotation from go, everything passes.

The type that UCM infers for go is lexically identical to the one in the original example above, and if I click to have the suggested type populated by the language server in my editor, the error returns.

This essentially makes for a round-tripping error, as the inferred annotation is always emitted when the function is brought into the editor.

[dfreeman]

A bit of discussion and further examples in Discord: https://discord.com/channels/862108724948500490/1205574011480707082/1205574011480707082

[ceedubs]

This slight variation does compile:

takesMany : ['{g1, Ask ('{g2} ())} ()] -> ()
takesMany x = bug "not implemented"

I've noticed a general pattern that using multiple ability type variables instead of forcing them to be unified tends to achieve better inference. Often this means that in your return type you'll need to declare something like {g1, g2}, but in my experience that is usually fine.