[ fix ] Parse let _ = as Let rather than LetPat

Author: gallais

src/Idris/Parser/Let.idr

@@ -87,4 +87,7 @@ mkDoLets origin lets = letFactory
             then DoLet fc fc' (UN n) rig ty val
             else DoLetPat fc (PRef fc' (UN n)) ty val []
          ) :: buildDoLets rest
-      (MkLetBinder rig pat ty val alts) => DoLetPat fc pat ty val alts :: buildDoLets rest
+      (MkLetBinder rig (PImplicit fc') ty val []) =>
+        DoLet fc fc' (UN "_") rig ty val :: buildDoLets rest
+      (MkLetBinder rig pat ty val alts) =>
+        DoLetPat fc pat ty val alts :: buildDoLets rest

tests/idris2/basic061/IgnoreDo.idr

@@ -3,11 +3,13 @@ module IgnoreDo
 bound : Maybe () -> Maybe b -> Maybe b
 bound m n = do
   x <- m
+  let y = Z
   n
 
 ignored : Maybe () -> Maybe b -> Maybe b
 ignored m n = do
   _ <- m
+  let _ = Z
   n
 
 seqd : Maybe () -> Maybe b -> Maybe b

tests/idris2/basic061/expected

@@ -1,6 +1,6 @@
 1/1: Building IgnoreDo (IgnoreDo.idr)
 IgnoreDo> IgnoreDo.bound : Maybe () -> Maybe b -> Maybe b
-bound m n = m >>= (\x => n)
+bound m n = m >>= (\x => let y = 0 in n)
 IgnoreDo> IgnoreDo.ignored : Maybe () -> Maybe b -> Maybe b
 ignored m n = m >>= (\_ => n)
 IgnoreDo> IgnoreDo.seqd : Maybe () -> Maybe b -> Maybe b