Functions with only implicit arguments are never eta-expanded

[HeikoRibberink]

Consider the following example:

val int/impl = -1

fun tuple2/impl(?a/impl : a, ?b/impl : b) : (a, b)
  (a/impl, b/impl)

fun main()
  val tup : (int, (int, int)) = impl()
  tup

Hovering over ... = impl():

fun tuple2/impl : (?a/impl : int, ?b/impl : (int, int)) -> (int, (int, int))  
?a/impl=int/impl
?b/impl=tuple2/impl(?a/impl=int/impl,?b/impl=int/impl)

Look at the second argument:

?b/impl=tuple2/impl(?a/impl=int/impl,?b/impl=int/impl)

It is not eta-expanded! This is very neat, because one can use implicits to construct other values, without having to call functions.

But there is a catch! Consider the following example:

effect fun foo(x : string) : ()

fun int/impl() : foo int
  foo("Int")
  -1

fun tuple2/impl(?a/impl : () -> foo a, ?b/impl : () -> foo b) : foo (a, b)
  foo("Tuple2:")
  (a/impl(), b/impl())

fun print-foo(?impl : () -> foo a) : console a
  with fun foo(x)
    println(x)
  impl()

fun main()
  val tup : (int, (int, int)) = print-foo()
  tup

Now we don't care as much about the value that is returned, but more about the effect foo, which we want to run under our own handler.
Seems fine to me; I remember that Koka eta-expands implicits. But alas, the dreaded red squiggles show us that this is not fine:

1. types do not match
   context      :                                         
   term         :                                         
   inferred type: () -> foo (int, (int, int))
   expected type: (_a, _b)
   because      : type cannot be instantiated to match the annotation

Koka did not eta-expand the function for us, rendering our use-case entirely impossible!
To make it even worse, supplying a few implicits doesn't even help:

val tup : (int, (int, int)) = print-foo(tuple2/impl) // Still errors!
val tup : (int, (int, int)) = print-foo(fn() tuple2/impl()) // Still!

Until finally, we've manually provided every tuple2/impl:

val tup : (int, (int, int)) = print-foo(fn() tuple2/impl(?b/impl=tuple2/impl))

It compiles, but it is very ugly.

Suggested change

Try to eta-expand functions with only implicit arguments once. The current behaviour is nice in many cases, but only works for total functions.

[HeikoRibberink]

There is a hacky solution: give it a non-implicit parameter to force eta-expansion.

effect fun foo(x : string) : ()

fun int/impl(_ : ()) : foo int
  foo("Int")
  -1

fun tuple2/impl(_ : (), ?a/impl : (()) -> foo a, ?b/impl : (()) -> foo b) : foo (a, b)
  foo("Tuple2:")
  (().a/impl, ().b/impl)

fun print-foo(?impl : (()) -> foo a) : console a
  with fun foo(x)
    println(x)
  ().impl

fun main()
  val tup : (int, (int, int)) = print-foo()
  tup