Merge pull request #3409 from mtzguido/tac_fix

normalizer: a fix for a plugin returned by a function

src/syntax/FStar.Syntax.Util.fst

@@ -356,14 +356,19 @@ let head_and_args t =
     | Tm_app {hd=head; args} -> head, args
     | _ -> t, []
 
-let rec head_and_args_full t =
+let rec __head_and_args_full unmeta t =
     let t = compress t in
     match t.n with
     | Tm_app {hd=head; args} ->
-      let (head, args') = head_and_args_full head
+      let (head, args') = __head_and_args_full unmeta head
       in (head, args'@args)
+    | Tm_meta {tm} when unmeta ->
+      __head_and_args_full unmeta tm
     | _ -> t, []
 
+let head_and_args_full        t = __head_and_args_full false t
+let head_and_args_full_unmeta t = __head_and_args_full true t
+
 let rec leftmost_head t =
     let t = compress t in
     match t.n with

src/typechecker/FStar.TypeChecker.Normalize.fst

@@ -381,9 +381,9 @@ let reduce_primops norm_cb cfg (env:env) tm : term & bool =
     if not cfg.steps.primops
     then tm, false
     else begin
-         let head, args = U.head_and_args tm in
+         let head, args = U.head_and_args_full tm in
          let head_term, universes = 
-           let head = SS.compress head in
+           let head = SS.compress (U.unmeta head) in
            match head.n with
            | Tm_uinst(fv, us) -> fv, us
            | _ -> head, []
@@ -2429,7 +2429,7 @@ and do_rebuild (cfg:cfg) (env:env) (stack:stack) (t:term) : term =
            norm cfg env stack' e
 
         | Tm_app _ when cfg.steps.primops ->
-          let hd, args = U.head_and_args t in
+          let hd, args = U.head_and_args_full_unmeta t in
           (match (U.un_uinst hd).n with
            | Tm_fvar fv ->
                begin

tests/tactics/PluginReturned.fst

@@ -0,0 +1,31 @@
+module PluginReturned
+
+open FStar.Tactics.V2
+
+(* This used to trip the normalizer due to an extra Meta_monadic
+node on the returned and_elim or inspect (which are plugins). *)
+
+assume val p : prop
+assume val q : prop
+
+let foo (b:bool) : Tac (term -> Tac unit) =
+  if b
+  then and_elim
+  else fail "no"
+
+let test (x : squash (p /\ q)) =
+  assert True by (
+    let f = foo true in
+    f (quote x);
+    dump ""
+  )
+
+let bar () : Tac (term -> Tac term_view) =
+  inspect
+
+let test2 () =
+  assert True by (
+    let f = bar () in
+    let tv = f (`1) in
+    dump ""
+  )