Whitespace sensitive parsing of local definitions (type-ascribing let)

[edwinb]

Issue by ohad
Wednesday Nov 06, 2019 at 08:29 GMT
Originally opened as edwinb/Idris2-boot#150

---

Might be related to #113 .

Steps to Reproduce

$ cat Bar.idr 
X : Nat
X = let a : Nat
        a = 0
        in a
$ idris2 -c Bar.idr 

Expected Behavior

1/1: Building Bar2 (Bar.idr)
$

Observed Behavior

Bar.idr:4:9--4:9:Parse error: Couldn't parse declaration (next tokens: [in, identifier a, end of input])

If we dis-indent the in keyword, it parses fine:

$ cat Bar2.idr 
X : Nat
X = let a : Nat
        a = 0
       in a
$ idris2 -c Bar2.idr 
1/1: Building Bar2 (Bar2.idr)
$

[ska80]

I think this issue can be closed now as it typechecks now:

% cat Issue31.idr 
module Issue31

X : Nat
X = let a : Nat
        a = 0
        in a
% idris2 Issue31.idr
     ____    __     _         ___                                           
    /  _/___/ /____(_)____   |__ \                                          
    / // __  / ___/ / ___/   __/ /     Version 0.3.0-da92f9d67
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org           
 /___/\__,_/_/  /_/____/   /____/      Type :? for help                     

Welcome to Idris 2.  Enjoy yourself!
1/1: Building Issue31 (Issue31.idr)
Issue31> :t X
Issue31.X : Nat
Issue31> X
0