Kind inference only seems to infer types and not other abilities

[puffnfresh]

Describe and demonstrate the bug

Input:

ability Exceptional f where
  _throw : f {Exception}

type NaturalAbility e = NaturalAbility (() -> {e} Nat)

oneNaturalAbility : NaturalAbility {Exception}
oneNaturalAbility = 
  NaturalAbility (_ -> 1)

main : () -> {IO, Exception} ()
main =
  match oneNaturalAbility with
    NaturalAbility f -> do
      n = f()
      printLine (toText n)

-- Below does not compile, but I think it should!

badNat : {Exceptional NaturalAbility} Nat
badNat =
  _throw

Output:

  Kind mismatch arising from
       19 | badNat : {Exceptional NaturalAbility} Nat

    Exceptional expects an argument of kind: Type -> Type; however, it is applied to NaturalAbility
    which has kind: Ability -> Type.

Screenshots

Environment (please complete the following information):

• OS/Architecture: Windows 11

I have tried versions from 4af93e9 (Jan 2024) all the way to e388786 (Aug 2024).

Additional context

In the error, the claim that NaturalAbility has kind Ability -> Type is true. It's wrong that Exceptional should expect an argument of kind Type -> Type. It seems like something is off with kind inference there.

[puffnfresh]

You can see lots of this live in the optics library, for example:

src.util.get0MapOf :
  (Get0Of m {Ix is, Err js, e} a b
  ->{g,
  Coindexed (Get0Of m),
  Prism (Get0Of m),
  Prism1 (Get0Of m),
  Lens (Get0Of m),
  MLens0 (Get0Of m),
  Indexed (Get0Of m),
  MLens (Get0Of m),
  Getter (Get0Of m),
  MLens1 (Get0Of m),
  Getter0 (Get0Of m),
  Lens0 (Get0Of m)} Get0Of m {Ix (), Err Void, e} s t)
  -> (a ->{e, Err js, Ix is} Optional m)
  -> s
  ->{e, g} Optional m
src.util.get0MapOf op ar s =
  (Get0Of sr) = Get0Of.handles op (Get0Of ar)
  (do sr s) |> errToEither |> ixProvide!() |> Either.fold absurd id

type src.carriers.Get0Of r e a b = Get0Of (a ->{e} Optional r)

ability src.abilities.Coindexed p where
  _withErr :
    p {Err js, e} a (Either j b)
    ->{src.abilities.Coindexed p} p {Err (Either j js), e} a b
  _absorbErr :
    p {Err (Either j js), e} a b
    ->{src.abilities.Coindexed p} p {Err js, e} a (Either j b)

[puffnfresh]

You don't need an ability declaration - probably unsurprising since abilities are basically data declarations:

type Exceptional f = Exceptional (f {Exception})

type NaturalAbility e = NaturalAbility (() -> {e} Nat)

oneNaturalAbility : NaturalAbility {Exception}
oneNaturalAbility = 
  NaturalAbility (_ -> 1)

-- badNat : Exceptional NaturalAbility
badNat =
  Exceptional oneNaturalAbility

What's interesting about the above is that it compiles!

    ⍟ These new definitions are ok to `add`:

      type Exceptional f
      type NaturalAbility e
      badNat            : Exceptional NaturalAbility
      oneNaturalAbility : NaturalAbility {Exception}

But if you try to copy/paste that type into the file:

  Kind mismatch arising from
        9 | badNat : Exceptional NaturalAbility

    Exceptional expects an argument of kind: Type -> Type; however, it is applied to NaturalAbility
    which has kind: Ability -> Type.

[pchiusano]

Agree this seems wrong, thanks for detailed report! Basically it looks like kind checker won’t infer a type parameter of kind Ability -> Type for some reason. Even when the type param is only applied to things of kind Ability within the type.

@tstat what do you think?

[puffnfresh]

@pchiusano my theory is actually that it's the type application syntax which is generating a bad constraint. It seems like Unison can and does infer the right kind. It just breaks if I write it out.

[puffnfresh]

Yeah, confirmed. I commented out kindCheckAnnotations and the example above "works"

[puffnfresh]

More minimal example, using the ByteArray builtin (a special case in the constraint generation):

type IOF f = IOF (f {IO})

array : '{IO} IOF mutable.ByteArray
array _ =
  n = IO.byteArray 10
  IOF n

[puffnfresh]

Something else interesting. This compiles:

type IOF f = IOF (f {IO})

type G = G (IOF mutable.ByteArray)

array : IOF mutable.ByteArray -> Nat
array _ = 0

But this does not:

type IOF f = IOF (f {IO})

array : IOF mutable.ByteArray -> Nat
array _ = 0

[tstat]

This final example is a result of kind defaulting. Looks like the inferred kind for f in IOF f is _ -> Type, which is incorrect. Kind defaulting takes these unconstrained vars and defaults them to Type, resulting in the erroneous Type -> Type constraint.

So, this looks like a constraint generation failure where {IO} isn't constrained to be of kind Ability? Yeah, if you swap {IO} for IO then it does infer the kind Ability -> Type for f.