Any example of usage of Coreader?

[nilp0inter]

Hi,

I am having a hard time trying to figure out how to use the Coreader Coeffect. Specifically trying to get more than one Var in the same computation:

example n wa = 
    let wb = extend getY wa
        wc = extend getX wb
    in (extract wc) + (extract wb)
  where
    getX = ask (Var::(Var "x"))
    getY = ask (Var::(Var "y"))

The above expression fails to type check with this error:

    • Couldn't match type ‘'[ "x" ':-> a]’ with ‘'[]’
      Expected type: IxCoreader (Plus IxCoreader '[] '[ "x" ':-> a]) a
        Actual type: IxCoreader '[] a
    • In the second argument of ‘extend’, namely ‘wb’
      In the expression: extend getX wb
      In an equation for ‘wc’: wc = extend getX wb
    • Relevant bindings include
        wc :: IxCoreader '[] a
          (bound at /home/nil/Project/coeffects/app/Main.hs:25:9)
        wb :: IxCoreader '[] a
          (bound at /home/nil/Project/coeffects/app/Main.hs:24:9)
        wa :: IxCoreader '[ "y" ':-> a] b
          (bound at /home/nil/Project/coeffects/app/Main.hs:23:11)
        example :: p -> IxCoreader '[ "y" ':-> a] b -> a
          (bound at /home/nil/Project/coeffects/app/Main.hs:23:1)
   |
25 |         wc = extend getX wb
   |                          ^

Any kind of help would be greatly appreciated.

Thank you!