Merge pull request #2737 from W95Psp/revert-attrs-restriction-local-n…

…ames

Revert restriction from #2621: allow local names in attrs

src/typechecker/FStar.TypeChecker.TcTerm.fst

@@ -4334,17 +4334,7 @@ and tc_trivial_guard env t =
   t,c
 
 and tc_attributes env attrs =
-  // we don't want attributes to depend on local names (otherwise,
-  // this would imply dependent attributes, substitutions within
-  // attributes...) hence we get rid of [gamma] (the local names)
-  // below.
-  let env = { env with gamma = []; gamma_sig = []; gamma_cache = BU.smap_create 100 } in
-  try List.map (fun attr -> fst (tc_trivial_guard env attr)) attrs
-  with | Error (Fatal_VariableNotFound, msg, rng, ctx) -> // adding small hint for the user
-           raise (Error ( Fatal_VariableNotFound
-                        , msg ^ ". Hint: local names are not allowed in attributes."
-                        , rng, ctx))
-       | e -> raise e
+  List.map (fun attr -> fst (tc_trivial_guard env attr)) attrs
 
 let tc_check_trivial_guard env t k =
   let t, _, g = tc_check_tot_or_gtot_term env t k "" in

tests/micro-benchmarks/BinderAttributes.fst

@@ -21,9 +21,8 @@ let f (#[@@@ description "x_imp"] x_imp:int) ([@@@ description "y"] y:string) :
 let f2 (#[@@@ description "x_imp"]x_imp [@@@ description "y"]y : int) : Tot unit =
     ()
 
-[@@expect_failure [230]]
-let local_names_in_attributes_are_forbidden
-  = x:unit -> [@@@x]y:unit -> unit
+let attributes_with_local_name (s: string)
+  = [@@@ description s] y:string -> unit
 
 type binder =
     {
@@ -148,3 +147,12 @@ let _ =
         let expected = [[{ name = "x_imp"; qual = "Implicit"; desc = Some "x_imp"; }; { name = "y"; qual = "Explicit"; desc = Some "y"; }]] in
         iter2 (fun ex bs -> validate ex bs) expected b
     end
+
+let _ =
+    // Substitution within attributes
+    assert True by begin
+        let foo = "foo" in
+        let t = attributes_with_local_name foo in
+        let bs = binders_from_arrow (quote t) in
+        validate [{ name = "y"; qual = "Explicit"; desc = Some foo; }] bs
+    end