koka-lang / koka

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

Polymorphic Effect Inference Inconsistency for Function Values Across Multiple Call Sites #401

Open chtenb opened 9 months ago

chtenb commented 9 months ago

Take the following code

pub fun take-div(i : () -> div int) ()
pub fun take-total(i : () -> <> int) ()
pub fun get() : e int 42

Now this will compile

pub fun main()
  take-div(get)
  take-total(get)

But this will not

pub fun main()
  val f = get
  take-div(f)
  take-total(f)

with the error message being

repro.kk(4,14): error: effects do not match context : take-total(f) term : f inferred effect: <div|_e> expected effect: (<>)

Superficially the problem seems to be that the effect is inferred for the value f once, rather than for each call site individually.

anfelor commented 8 months ago

As already pointed out by Tim in issue #402 this is due to the missing let-generalization of effects. In particular, the example can be checked if the type signature of f is provided:

pub fun main()
  val f : forall <e> () -> e int = get 
  take-div(f)
  take-total(f)