Polymorphic Effect Inference Inconsistency for Function Values Across Multiple Call Sites

[chtenb]

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]

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)