type checker not catching disallowed ability

[ceedubs]

Describe and demonstrate the bug

Below I have a forkThread function that takes a thunk that is only allowed to use the IO ability. But when I call into it via List.foreach, I am able to pass in a thunk that requires another ability (in this case Exception, but I can add arbitrary abilities to the same effect). The type checker should catch that this is not allowed.

Input:

```ucm
.> project.create-empty proj
proj/main> builtins.mergeio

forkThread :
  '{IO} ()
  ->{IO} ()
forkThread thunk = todo "not important"

List.foreach : (a -> {g} ()) -> [a] -> {g} ()
List.foreach = todo "not important"

main : '{IO, Exception} ()
main = do
  thunk : '{IO, Exception} ()
  thunk = todo "you shouldn't be able to pass this into forkThread because it requires the Exception ability"
  List.foreach forkThread [thunk]

Output:

.> project.create-empty proj

  🎉 I've created the project proj.

  🎨 Type `ui` to explore this project's code in your browser.
  🔭 Discover libraries at https://share.unison-lang.org
  📖 Use `help-topic projects` to learn more about projects.

  Write your first Unison code with UCM:

    1. Open scratch.u.
    2. Write some Unison code and save the file.
    3. In UCM, type `add` to save it to your new project.

  🎉 🥳 Happy coding!

proj/main> builtins.mergeio

  Done.

forkThread :
  '{IO} ()
  ->{IO} ()
forkThread thunk = todo "not important"

List.foreach : (a -> {g} ()) -> [a] -> {g} ()
List.foreach = todo "not important"

main : '{IO, Exception} ()
main = do
  thunk : '{IO, Exception} ()
  thunk = todo "you shouldn't be able to pass this into forkThread because it requires the Exception ability"
  List.foreach forkThread [thunk]

  Loading changes detected in scratch.u.

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:

    ⍟ These new definitions are ok to `add`:

      List.foreach : (a ->{g} ()) -> [a] ->{g} ()
      forkThread   : '{IO} () ->{IO} ()
      main         : '{IO, Exception} ()

🛑

The transcript was expecting an error in the stanza above, but did not encounter one.

Environment (please complete the following information):

• ucm --version 7172bb8e4
• OS/Architecture: x86 NixOS

Additional context

I ran into both this and #5128 in the same definition for a confusing double whammy.

[ceedubs]

This might ultimately be the same issues as #3513.

[dolio]

Took a quick look. I think this is what's going on:

When you do foreach forkThread, the type checker solves a = '{IO} (). When it does this, it adds a slack variable, so actually a = '{g, IO} (). which unifies with '{Exception, IO} (). So, adding the slack variable in this situation doesn't actually make sense.

I'll have to take a look at what's actually introducing the variable in this situation.

[dolio]

I think this might actually be simple to fix. Fixes #3513, too.