Fixes #5293: Generate IsAbility constraint for ability sets

[tstat]

No description provided.

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

Makes sense to me. I haven't tested it yet but probably won't get time for a while.

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