Confusing ability mismatch with record-of-functions

[sellout]

Describe and demonstrate the bug

I am trying to generalize corecursive structures to be ability-polymorphic. This works differently than recursive structures, because they’re lazy. An unfold ((a ->{g} f a) ->{} a ->{} t) delays its abilities, and so the structure needs to carry it explicitly for when they’re forced (Nu {g} f as opposed to Mu f).

This mostly works, except I can’t seem to create “instances” of the records-of-functions I’m using as “type classes”. The same thing works fine on the recursive side.

So, I first create this “type class” for corecursive structures. You can see that ana defers the ability as above, but then project needs the ability in order to force a layer of of the structure.

(NB: I’m trying to be very explicit with the ability sets just within this issue, so someone can point out if the abilities I expect to require are different than they should be.)

-- **NB**: This can’t be defined as a record, because the Unison can’t yet 
--         figure out how to generate the accessors correctly. So, the “getters”
--         are explicitly defined below.
structural type Corecursive g t f
  = Corecursive (∀ a. (a ->{g} f a) ->{} a ->{} t) (t ->{g} f t)

Corecursive.ana : Corecursive g t f ->{} (a ->{g} f a) ->{} a ->{} t
Corecursive.ana = cases Corecursive ana _ -> ana

Corecursive.project : Corecursive g t f ->{} t ->{g} f t
Corecursive.project = cases Corecursive _ project -> project

scratch/main> add

Now I define two structures that I think satisfy this class. First Cofix, which is more like a recursive data structure (Fix), but lazy:

structural type Cofix g f = Cofix ('{g} f (Cofix g f))

Cofix.ana :
  (∀ g a b. (a ->{g} b) ->{} f a ->{g} f b)
  ->{} (a ->{g} f a)
  ->{} a
  ->{} Cofix g f
Cofix.ana map ψ a = Cofix do map (Cofix.ana map ψ) (ψ a)

Cofix.project : Cofix g f ->{g} f (Cofix g f)
Cofix.project = cases Cofix f -> f()

scratch/main> add

And then Nu, which is more indirect, but should have the same behavior:

structural type Nu g f = Nu (∀ r. (∀ a. (a ->{g} f a) ->{} a ->{g} r) ->{g} r)

Nu.ana : (a ->{g} f a) ->{} a ->{} Nu g f
Nu.ana ψ seed = Nu (fn -> fn ψ seed)

Nu.project :
  (∀ g a b. (a ->{g} b) ->{} f a ->{g} f b) -> Nu g f ->{g} f (Nu g f)
Nu.project map = cases
  Nu fn -> fn (ψ seed -> map (next -> Nu (nextFn -> nextFn ψ next)) (ψ seed))

scratch/main> add

However, I can’t manage to define either instance:

Cofix.corec :
  (∀ g a b. (a ->{g} b) ->{} f a ->{g} f b) ->{} Corecursive g (Cofix g f) f
Cofix.corec map = Corecursive (Cofix.ana map) Cofix.project

  Loading changes detected in scratch.u.

  The expression in red

                needs the abilities: {g8}
    but was assumed to only require: {}

  This is likely a result of using an un-annotated function as an argument with concrete abilities. Try adding an annotation to the function definition whose body is red.

      3 | Cofix.corec map = Corecursive (Cofix.ana map) Cofix.project

Nu.corec :
  (∀ g a b. (a ->{g} b) ->{} f a ->{g} f b) ->{} Corecursive g (Nu g f) f
Nu.corec map = Corecursive Nu.ana (Nu.project map)

  Loading changes detected in scratch.u.

  The expression in red

                needs the abilities: {g8}
    but was assumed to only require: {}

  This is likely a result of using an un-annotated function as an argument with concrete abilities. Try adding an annotation to the function definition whose body is red.

      3 | Nu.corec map = Corecursive Nu.ana (Nu.project map)

You can’t see it in the transcript, but the entire rhs is red. If I extract the last argument from either instance, I can get it to narrow a bit.

Cofix.corec :
  (∀ g a b. (a ->{g} b) ->{} f a ->{g} f b) ->{} Corecursive g (Cofix g f) f
Cofix.corec map =
  proj : Cofix g f ->{g} f (Cofix g f)
  proj = Cofix.project
  Corecursive (Cofix.ana map) proj

  Loading changes detected in scratch.u.

  The expression in red

                needs the abilities: {g8}
    but was assumed to only require: {}

  This is likely a result of using an un-annotated function as an argument with concrete abilities. Try adding an annotation to the function definition whose body is red.

      6 |   Corecursive (Cofix.ana map) proj

Environment (please complete the following information):

• ucm --version: 0.5.38
• OS/Architecture: macOS 15.4.1, M1

Additional context

Sorry this example isn’t more minimal. I’ll try to strip it down a bit, but wanted to get it reported before I spun my wheels any more.