linear lambda claims to consume unrelated binder

[MarcelineVQ]

Idris 2, version 0.1.0-b617cae88

Steps to Reproduce

foo1 : (1 f : (1 x : a) -> b) -> Maybe Char
foo1 f = Just 'c' >>= (\arr => ?foo1_rhs)

foo2 : (1 f : (1 x : a) -> b) -> Maybe Char
foo2 f = Just 'c' >>= (\1 arr => ?foo2_rhs)

Examine hole foo1_rhs and foo2_rhs

Expected Behavior

Both holes should have 1 f : (1 x : a) -> b and foo2_rhs should additionally have 1 arr : Char

Observed Behavior

foo2_rhs has 1 arr : Char but also has 0 f : (1 x : a) -> b f is shown as having been consumed, which is incorrect as I understand it. But further, this is not actually the case, as:

foo2 : (1 f : (1 x : a) -> b) -> Maybe Char
foo2 f = Just 'c' >>= (\1 arr => Just arr)

will give a correct error of There are 0 uses of linear name f. Meaning that f isn't really consumed but just being wrongly reported.

[MarcelineVQ]

No, actually, something else is going on here after all. So this could just be my lack of understanding about linearity. Could anyone comment?

foo3 : (1 f : (1 x : Nat) -> Maybe Char) -> Maybe Char
foo3 f = Just (S Z) >>= (\1 arr => f arr)

Gives me While processing right hand side of foo3 at Test.idr:10:1--11:1: f is not accessible in this context which would explain the 0 f : ... from earlier, but why is it inaccessible?

Additionally my editor gives me another error there that I'm not sure how to get idris2 to give me: Error(s) building file Test.idr: Test.idr:10:1--11:1:When elaborating right hand side of Main.foo3: Test.idr:10:36--10:41:Trying to use linear name f in irrelevant context

[rgrover]

foo4 : (1 f : (1 x : Nat) -> Maybe Char) -> Maybe Char
foo4 f = Just (S Z) >>= (\arr => ?rhs arr)

The above variation on foo3 says that f is still unused, but clearly foo3 complains when f gets used. hmm...

[edwinb]

You can't use f there because of the type of >>=, which is unrestricted in its second argument.

There's still some glitches in the calculation of quantities in holes under case blocks, which is an unrelated thing, but still needs to be fixed.

[MarcelineVQ]

I see so the foo3 error is akin to the tried to use linear name f in a non-linear context error. It was a bit confusing because "f is not accessible in this context" made it seem like some sort of a scoping error, and I guess it is.

[edwinb]

yes, that error message isn't very good, but it'll take a bit more work to come up with a clearer one I think - since it depends a bit on the surrounding context. So to report something more usefully, it needs to know that you're inside an argument that's unrestricted.