It’s possible to construct values of the wrong type

[loewenheim]

The following constructs a value [[]] : [Nat].

use .base Boolean Nat Request

ability Decide where
    decide : Boolean

ability Fail where
    fail : ∀ a. a

decideAll : Request Decide a -> [a]
decideAll r = case r of
    { Decide.decide -> k } -> (handle decideAll in k true) ++ (handle decideAll in k false)
    { x } -> [x]

failDefault : a -> Request Fail a -> a
failDefault d r = case r of
    { Fail.fail -> k } -> handle failDefault d in k d
    { x } -> x

foo : [Nat]
foo = handle failDefault [] in handle decideAll in Fail.fail

> foo
    22 | > foo
           ⧩
           [[]]

[aryairani]

Thanks for this report, @loewenheim

[TomasMikula]

Quoting the "Do Be Do Be Do" paper:

Abilities (Frank’s realisation of algebraic effects) are collections of parameterised interfaces, each of which describes a choice of commands (known elsewhere as operations [49]). Command types may refer to the parameters of their interface but are not otherwise polymorphic.

So Frank would not allow the Fail ability, since its fail operation is polymorphic.

Just noting, maybe there is a solution that does not prohibit polymorphic operations in abilities.

[TomasMikula]

So I think the typechecking should fail here:

failDefault : a -> Request Fail a -> a
failDefault d r = case r of
    { Fail.fail -> k } -> handle failDefault d in k d
                                                  ^^^

because d has type a from the outer scope, but k should either

• take a value of type ∀ a. a, because that's the return type of Fail.fail; or
• if we interpret the Fail.fail pattern as type-applied, i.e. something like

  case r of
      { Fail.fail @b -> k } -> handle failDefault d in k d

  then k takes a value of type b, because that's the return type of Fail.fail @b.

[TomasMikula]

Slightly reduced example:

use .base Boolean Nat Request

ability Fail where
    fail : ∀ a. a

failDefault : a -> Request Fail a -> a
failDefault d r = case r of
    { Fail.fail -> k } -> handle failDefault d in k d
    { x } -> x

foo : [Nat]
foo = handle failDefault [] in [Fail.fail]

> foo

    14 | > foo
           ⧩
           [[]]

[atacratic]

@TomasMikula Interestingly they seem to have lifted that limitation you mentioned in the Frank implementation: https://github.com/frank-lang/frank/blob/master/examples/polyAbort.fk defines Fail (under the name Abort).

[TomasMikula]

Thanks, @atacratic.

[loewenheim]

So I think the typechecking should fail here:

failDefault : a -> Request Fail a -> a
failDefault d r = case r of
    { Fail.fail -> k } -> handle failDefault d in k d
                                                  ^^^

because d has type a from the outer scope, but k should either

* take a value of type `∀ a. a`, because that's the return type of `Fail.fail`; or

* if we interpret the `Fail.fail` pattern as type-applied, i.e. something like
  ```haskell
  case r of
      { Fail.fail @b -> k } -> handle failDefault d in k d
  ```

  then `k` takes a value of type `b`, because that's the return type of `Fail.fail @b`.

To be honest, I was initially surprised that failDefault typechecked; the type of fail is uninhabited, so your only choice should be to discard the continuation in the handler. I guess there aren’t really higher rank types in Unison as of now?