ability check failure with list of functions/thunks

[ceedubs]

Describe and demonstrate the bug

In the following example when I try to use a '{} () as type '{Exception} (), I get a type checker error. But I believe that a -> {} b is supposed to conform to type a -> {g} b for all g.

Input:

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

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

runThunk : '{Exception} () -> ()
runThunk thunk = todo "not important"

thunks : ['{} ()]
thunks = []

main = do
  List.foreach runThunk thunks

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.merge

  Done.

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

runThunk : '{Exception} () -> ()
runThunk thunk = todo "not important"

thunks : ['{} ()]
thunks = []

main = do
  List.foreach runThunk thunks

  Loading changes detected in scratch.u.

  I found an ability mismatch when checking the application

     11 |   List.foreach runThunk thunks

  When trying to match [Unit -> Unit] with [Unit ->{𝕖51,
  Exception} Unit] the right hand side contained extra
  abilities: {𝕖51, Exception}

🛑

The transcript failed due to an error in the stanza above. The error is:

I found an ability mismatch when checking the application

 11 |   List.foreach runThunk thunks

When trying to match [Unit -> Unit] with [Unit ->{𝕖51, Exception} Unit] the right hand side contained extra abilities: {𝕖51, Exception}

**Screenshots**

It isn't visible in the transcript output, but if you do the same in a scratch file, the error message is confusing. It highlights `thunks` in green and the associated green type is `[Unit ->{𝕖51, Exception} Unit]`. But that is surprising to me since `thunks` is explicitly `[Unit -> {} Unit]`.

![image](https://github.com/unisonweb/unison/assets/977929/82f8b6b1-d61f-470a-b47e-6b9175808657)

**Environment (please complete the following information):**
 - `ucm --version` 7172bb8e4
 - OS/Architecture: x86 NixOS

[pchiusano]

I suspect this is just because data types are invariant in Unison. List happens to be covariant, so we could special case it in the typechecker, and I could also imagine inferring variance of type params for user defined data types. It could hook in at a similar place as kind inference. Then the typechecker would need maintain and use this variance info in various places.

Summary: this isn’t an easy “bugfix”, it’s more like a new type system feature, but I think it could be worth doing at some point.

[ceedubs]

@pchiusano it doesn't seem to me like you should need lists to be treated as covariant for this code to compile. But I'm not a type system expert, and I'd like to better understand how I'm wrong.

List.foreach : (a -> {g} ()) -> [a] -> ()

In my case a is '{} (). But I don't really need the type system to understand that ['{} ()] conforms to ['{Exception} ()]. I just need it to recognize that I can call runThunk with a '{} ().

If I change my main like this it compiles:

main = do
  List.foreach (thunk -> let
    thunk' : '{Exception} ()
    thunk' = do thunk ()
    runThunk thunk'
  ) thunks

But this still fails:

main = do
  List.foreach (thunk -> let
    thunk' : '{Exception} ()
    thunk' = thunk
    runThunk thunk'
  ) thunks

To me this seems off. The code works fine with thunk' = do thunk (), so with thunk' = thunk (with an explicit type annotation), I would expect it to either compile or to complain that thunk' has type '{} () instead of '{Exception} (). I don't understand why instead the type error shows up in the outer scope.

[dolio]

I think Paul is right.

The sort of thing that's going to happen is that a gets solved to '{Exception} () from the first argument to foreach. Then we check the type of thunks against List ('{Exception} ()). This second check is with the ability list in an invariant position. There's a little extra where a slack variable is introduced when solving a I guess, but that doesn't help this scenario.

Your second example doesn't help because it's just going to solve for thunk and thunk' to have the same type, I think, so it works just like with runThunk. It's again just solving a variable (type of thunk) with a particular expression (annotation of thunk').

The one where you apply thunk has enough indirection to work differently. There you are solving the type of thunk to () ->{e} a, then later imposing {e} <= {Exception}, which defaults to e not including Exception, so it's still free to match with your empty ability set in thunks.