Function accepting an `'{g, Stream a} ()` is assuming `g = {}` unless annotation is accepted at call site

[pchiusano]

I'm not sure what's going on here, but I'm having to supply a type annotation on the argument to a function, it's like it's assuming the g effect on Stream.uncons is {} when it clearly should be Remote.

structural ability Stream a where emit : a -> ()

uncons : '{g, Stream a} r ->{g} Either r (a, '{g, Stream a} r)
uncons s = todo "uncons"

type Value a = Value a
ability Remote where blah : Nat

Value.pure : a -> Value a
Value.pure = Value

Value.map : (a ->{Remote} b) -> Value a -> Value b
Value.map f v = todo "Value.map" 

example = do 
  s : '{Remote, Stream Nat} ()
  s = do Stream.emit 42

  v0 : Value ('{Remote, Stream Nat} ())
  v0 = Value.pure s
  _ = Value.map uncons v0 -- doesn't typecheck
  _ = Value.map -- DOES typecheck
        (uncons : '{Remote, Stream Nat} () ->{Remote} Either () (Nat, '{Remote, Stream Nat} ()))
        (Value.pure s)
  ()

[pchiusano]

I wonder if the fact that g is in invariant position in the type signature is relevant...