Fixes #5293: Generate IsAbility constraint for ability sets

[tstat]

Choose your PR title well: Your pull request title is what's used to create release notes, so please make it descriptive of the change itself, which may be different from the initial motivation to make the change.

Overview

What does this change accomplish and why? i.e. How does it change the user experience? i.e. What was the old behavior/API and what is the new behavior/API?

Feel free to include "before and after" examples if appropriate. (You can copy/paste screenshots directly into this editor.)

If relevant, which Github issues does it close? (See closing-issues-using-keywords.)

Implementation notes

How does it accomplish it, in broad strokes? i.e. How does it change the Haskell codebase?

Interesting/controversial decisions

Include anything that you thought twice about, debated, chose arbitrarily, etc. What could have been done differently, but wasn't? And why?

Test coverage

Have you included tests (which could be a transcript) for this change, or is it somehow covered by existing tests?

Would you recommend improving the test coverage (either as part of this PR or as a separate issue) or do you think it’s adequate?

If you only tested by hand, because that's all that's practical to do for this change, mention that.

Loose ends

Link to related issues that address things you didn't get to. Stuff you encountered on the way and decided not to include in this PR.

[aryairani]

@tstat Hey thanks for this PR; I skimmed #5293 but wasn't sure: is this a proof of concept and we should take it from here, or was there more you wanted to do on it? (in which case I'll switch it to Draft for now)

[tstat]

This is the fix for the linked issue, although I see it breaks a test that depends on the previous failure to generate a constraint:

structural ability Foo where
  foo : {Foo} Nat

structural type Wrap a = Wrap Nat

blah : Wrap {Foo} -> Nat
blah = cases
  Wrap.Wrap n -> n + 1

> blah (Wrap 99)

The a in Wrap a is unconstrained, so it is defaulted to Type. On trunk when we kind check blah's annotation we erroneously didn't generate an IsAbility constraint for {Foo}, so, this annotation was permitted. However, this is an expected failure since we don't support polymorphic kinds.

So, I'll leave it to you all to decide what to do about this test, but this PR simply constrains ability sets to be of kind ability, which was just an oversight when generating constraints.

[aryairani]

Gotcha — thanks!

[puffnfresh]

I loaded up the optics library and can confirm that this fix makes a lot of the library now compile!

[aryairani]

@tstat

I think in the cloud library we rely on having a type like Wrap, having kind Ability -> Type (doesn't have to be polymorphic), but with this PR and no other changes, I think we wouldn't be able to. e.g. Location {HTTP}, a node with access to the web.

The a in Wrap a is unconstrained, so it is defaulted to Type.

Is there a way to constrain it to Ability? We would need to add a syntax for kind annotations?

[pchiusano]

@aryairani this actually works fine:

type Location g = Location Nat

ability Remote where forkAt : Location g -> '{g, Remote} a -> a

ex0 : Location {IO, Exception} -> ()
ex0 loc = () 

ex1 : Location {IO, Exception} ->{Remote} ()
ex1 loc = forkAt loc do printLine "hello world"

-- does not typecheck as expected
{- Kind mismatch arising from
       12 | ex2 : Location Nat -> ()
    
    Location expects an argument of kind: Ability; however, it is applied to Nat which has kind:
    Type.
ex2 : Location Nat -> ()
ex2 loc = ()
-}

So I think we're good. It looks like the PR only defaults a parameter to Type if there are no usages within constructors of dependent types. For instance, this does not work, and this must have been what you tried (adding a function definition that constrains the kind, rather than a constructor):

type Location g = Location Nat

ex0 : Location {IO, Exception} -> ()
ex0 loc = () 

But as soon as you add Remote to the file, it typechecks, since it is looking at the full dependency graph of types when doing kind inference.

type Location g = Location Nat

ability Remote where forkAt : Location g -> '{g, Remote} a -> a

-- works
ex0 : Location {IO, Exception} -> ()
ex0 loc = () 

Adding a surface syntax for kind annotations seems like an independently good idea, but I'd say is out of scope for this PR. Also, even with kind annotations, that would change the hash of the type which we'd like to avoid when possible.

[aryairani]

@pchiusano

this must have been what you tried (adding a function definition that constrains the kind, rather than a constructor)

Okay yes, thanks.

Then I'll update the failing test with your example and go from there.