Composition of effectful functions typechecks when it shouldn't

[runarorama]

This typechecks, but shouldn't:

  IO.tryEval : '{g, IO, Exception} a ->{g, IO, Exception} a
  IO.tryEval = reraise << catchAll.impl

  IO.catchAll.impl : '{IO, Exception} a ->{IO} Either Failure a
  IO.catchAll.impl thunk =
    handle tryEval.impl '(catch thunk)
    with
      cases
        { x }                    -> x
        {Exception.raise f -> _} -> Left f

The argument to IO.tryEval requires an ability g, but the type of catchAll.impl should prohibit that.

Note that this does not typecheck:

  IO.tryEval : '{g, IO, Exception} a ->{g, IO, Exception} a
  IO.tryEval x = reraise (catchAll.impl x)

The type of << is:

  (Function.<<) : (b ->{𝕖} c) -> (a ->{𝕖} b) -> a ->{𝕖} c
  (Function.<<) f g x = f (g x)