Inferred type signature fails to unify ability type-params

[ChrisPenner]

This fails to compile unless I uncomment the type signature of todoHandle;

examples.books.logic : msg ->{Process e} ()
examples.books.logic _msg = match getCommandAutocomplete() with
  OrderRelated _kind        -> todoHandle ()
  ReturnStatus           -> todoHandle ()
  GiftCardStatus         -> todoHandle ()
  GiftCardPurchase      -> todoHandle ()
  NotficationRequest     -> todoHandle ()
  BookQuestion          -> todoHandle ()
  TalkToHuman          -> todoHandle ()
  FAQ                  -> todoHandle ()

-- todoHandle : '{Process e} ()
todoHandle = do
  books.logic ()

It fails with

  The expression in red needs the {Process e246} ability, but this location only has access to the {Process e255} ability,

     99 | examples.books.logic _msg = match getCommandAutocomplete() with

If I add the explicit type signature to todoHandle it unifies just fine.

I tried to minimize this with something like:

structural ability MyAbility e where
  incrementNat :  Nat -> Nat
  fail : e -> ()

useAbility : Nat -> {MyAbility e} Nat
useAbility n =
  match incrementNat n with
    1 -> doTheThing ()
    2 -> doTheThing ()
    _ -> 1

-- doTheThing : '{MyAbility e} Nat
doTheThing = do incrementNat  1

But this didn't trigger the error, so unfortunately there must be something going on that I don't understand 🤔

[dolio]

Here's a minimal-ish case

structural ability MyAbility e where
  incrementNat :  Nat -> Nat
  fail : e -> ()

-- useAbility : Nat -> {MyAbility e} Nat
useAbility n = doTheThing ()

doTheThing : '{MyAbility e} Nat
doTheThing = do useAbility 5

Has something to do with the two being mutually recursive. Providing both or neither signature is fine, but just one is a problem.

[dolio]

Okay, this is fundamentally an issue with the way we typecheck let rec. It always uses the procedure like inferring a set of un-annotated definitions, with any annotations just providing a specified type to go in the context for others to refer to.

This doesn't work with polymorphic definitions. The problem is that if you have a mix, one is supposed to have a generalized type, but the other has a type with a unification variable. When you go to check the annotated definition, the body will have a type mentioning that specific unification variable, which will fail to be general enough.

The proper procedure is

1. Split the definitions into annotated and un-annotated.
2. Infer the un-annotated definitions in a context containing the annotated types.
3. Generalize the types of the un-annotated definitions.
4. Check the annotated definitions in a context containing the generalized types.

Here's an even more minimal test case

f : a -> a
f x = g x x
g x y = f x