Idris2-boot
Idris2-boot copied to clipboard
Whitespace-sensitive parsing of let binding without ascription
Sorry if this is a feature!
Steps to Reproduce
Type-check the following declarations:
x1 : Nat
x1 =
let u =
S
Z
in
1
x2 : Nat
x2 =
let u =
S Z
in
1
x3 : Nat
x3 =
let u =
S Z
in
1
x4 : Nat
x4 =
let u = S Z
in
1
x5 : Nat
x5 =
let u =
S Z
in
1
Expected Behavior
These should all type-check.
Observed Behavior
The following don't type-check, with the below errors:
x1 : Nat
x1 =
let u =
S
Z
in
1
Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier u, symbol =, identifier S, identifier Z, in, literal 1, end of input])
x2 : Nat
x2 =
let u =
S Z
in
1
Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier u, symbol =, identifier S, identifier Z, in, literal 1, end of input])
x3 : Nat
x3 =
let u =
S Z
in
1
Foo.idr:21:7--22:7:While processing right hand side of Main.x4 at Foo.idr:20:1--42:1:
No type declaration for Main.u
The following type-check
x4 : Nat
x4 =
let u = S Z
in
1
x5 : Nat
x5 =
let u =
S Z
in
1
I don't think they should, because the body of the let should be indented further right than the u. Actually I think x5 should also be rejected but I can see why it isn't, looking at the code for the parser.