one type annotation in let means all other definitions must have type annotation

[shmish111]

If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!

Steps to Reproduce

Check

f : a -> b
f a' =
    let x : a
        x = a'
        y = 1
    in ?xyz

g : a -> b
g a' =
    let x : a
        x = a'
        y : Int
        y = 1
    in ?xyz

Expected Behavior

Type checks fine

Observed Behavior

Errors (1)
Test.idr:217:9
While processing right hand side of f at Test.idr:214:1--220:1:
No type declaration for Test.y

It can be 'fixed' by having a separate let block for things with type annotations and things without. If this is expected behaviour then:

1. I couldn't find any documentation about it
2. I found it very unintuitive. Indeed it took me a while to work out that I could have an additional block with the unannotated items

[gallais]

This bit of the parser is responsible: once we have seen let we commit to either a block of let-binders or a block of local definitions. We could instead allow interleavings of the two. https://github.com/edwinb/Idris2/blob/19426ecd141f93c34268a53ed09b5e48e64ba73b/src/Idris/Parser.idr#L553-L570

[edwinb]

I think it's reasonable to allow interleavings of the two different let forms.

[gallais]

Fighting the type errors but I have good hope I'll have something soon.