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
```

```unison
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:

```ucm
.> 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.

```
```unison
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
```

```ucm

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

Environment (please complete the following information):

• ucm --version 7172bb8
• 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.