koka-lang / koka

Koka language compiler and interpreter
http://koka-lang.org
Other
3.25k stars 161 forks source link

Type inference broken for `return` handler #248

Open eduardvercaemer opened 2 years ago

eduardvercaemer commented 2 years ago

Trying to use with return to extract a tuple element, it won't play nice as if done manually.

fun this-works( action : () -> e (a, b) ) : e a
  action().fst

fun this-also-works( action : () -> e (a, b) ) : e a
  fun extract( x : (a, b) ) : a
    x.fst
  action().extract

fun this-wont-work( action : () -> e (a, b) ) : e a
  with return( x : (a, b) ) x.fst
  action()
TimWhiting commented 9 months ago

So this works, but I agree that this should be fixed:

fun this-actually-work( action : () -> e (a, b) ) : e a
  with return( x:some<a,b> (a,b) ) x.fst
  action()

Specifically if a type variable is not bound, but is in a context where a forall<> is not appropriate we should suggest some<> which is underdocumented.

anfelor commented 8 months ago

Another option would be to change Koka's type inference so that type variables like a,b in the example always refer to the type variables bound by the top-level function signature (like Haskell's scoped type variables). While that feature makes it harder to copy functions from the top-level into a function body, I would argue that it is more intuitive and what I usually want when writing type signatures on variables.