unisonweb
ability check failure with list of functions/thunks
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 --version7172bb8e4- OS/Architecture: x86 NixOS
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 to 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.
@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.
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.
