anchor.diff:     *)
   
     match (SS.compress top).n with
  -  | Tm_match(e1, ret_opt, eqns) ->  //ret_opt is the return annotation
  +  | Tm_match(e1, ret_opt, eqns, _) ->  //ret_opt is the return annotation
       let e1, c1, g1 = tc_term
         (env |> Env.clear_expected_typ |> fst |> instantiate_both)
         e1 in
  
positive.code:         let branches = t_eqns |> List.map (fun ((pat, wopt, br), _, eff_label, _, _, _, _) ->
            pat, wopt, TcUtil.maybe_lift env br eff_label cres.eff_name cres.res_typ
          ) in
          let e = mk (Tm_match(scrutinee, ret_opt, branches)) top.pos in
          let e = TcUtil.maybe_monadic env e cres.eff_name cres.res_typ in
          //The ascription with the result type is useful for re-checking a term, translating it to Lean etc.
          //AR: revisit, for now doing only if return annotation is not provided
  
negative.code:         | Tm_meta _
          | Tm_type _ ->
            universe_of_aux env hd, args
          | Tm_match(_, _, hd::_, _) ->  //AR: TODO: use return annotation? Or the residual_comp?
            let (_, _, hd) = SS.open_branch hd in
            let hd, args' = U.head_and_args hd in
            type_of_head retry hd (args'@args)
  