Local definitions in irrelevant definitions are incorrectly checked for relevance

[ohad]

I thought we discussed/reported this at some point, but I can't find the report/fix.

Steps to Reproduce

$ cat Irrel.idr 
0
foo : (0 b : Bool) -> Bool
foo b = b

0
bar : Bool
bar = q
  where
    q : Bool
    q = foo True

0
baz : Bool
bar = let q : Bool
          q = foo True in
      q

$ idris2 -c Irrel.idr 

Expected Behavior

1/1: Building Irrel (Irrel.idr)

Observed Behavior

1/1: Building Irrel (Irrel.idr)
Irrel.idr:10:9--12:1:While processing right hand side of bar at Irrel.idr:7:1--12:1:
While processing right hand side of bar,q at Irrel.idr:10:5--12:1:
Main.foo is not accessible in this context
Irrel.idr:15:15--15:24:While processing right hand side of bar at Irrel.idr:14:1--19:1:
While processing right hand side of bar,q at Irrel.idr:15:11--15:24:
Main.foo is not accessible in this context

[edwinb]

Hmm, it's probably just not propagating the multiplicity to the local definition properly. You probably at least noticed that you can work around this for now with an explicit annotation on q. (Also that your last bar should be baz :))

[ziman]

Assuming that let (omega q : Bool) = foo True in q should be equivalent to (\omega q : Bool => q) (foo True), this should typecheck because the result of the lambda is used zero times.

So I don't think the annotation on q is inferred wrong. I think that the type checker should accept an omega there; is that right?

[ohad]

@ziman : This is a local definition, and not a let-binding. See the README

[ziman]

Oh, I see, thanks!