Pulse: error on binder attributes, they are ignored

I was recently very confused by this, proposing to just error out until
they are handled (if that becomes desirable). I plan to add attributes
to the letbinding itself (instead of the individual pattern variables).

Author: mtzguido

pulse/src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -509,9 +509,13 @@ let rec desugar_stmt' (env:env_t) (s:Sugar.stmt)
 
     | Sequence { s1={s=LetBinding lb; range=s1range}; s2 } ->
       begin match lb.pat.pat with
-      | A.PatVar _
-      | A.PatWild _ ->
-        (* simple bind *)
+      | A.PatVar (_, _, attrs)
+      | A.PatWild (_, attrs) ->
+        (* A simple bind. But error out if the user wrote binder
+        attributes, since these are ignored. *)
+        if Cons? attrs then
+          fail "Binder attributes are not allowed." (pos (List.hd attrs))
+        else return ();!
         desugar_bind env lb s2 s.range
       | _ ->
         (* a single-branch pattern match *)

pulse/test/NoBinderAttributes.fst

@@ -0,0 +1,11 @@
+module NoBinderAttributes
+
+#lang-pulse
+open Pulse
+
+[@@expect_failure]
+fn test ()
+{
+  let [@@@123] x = 1;
+  ();
+}

pulse/test/NoBinderAttributes.fst.output.expected

@@ -0,0 +1,4 @@
+* Info at NoBinderAttributes.fst(9,10-9,13):
+  - Expected failure:
+  - Binder attributes are not allowed.
+