anchor.diff:            (match topt with | None -> "None" | Some t -> Print.term_to_string t)
             (if env.top_level then "true" else "false");
   
  -    let tfun_opt, bs, letrec_binders, c_opt, tacopt, envbody, body, g = expected_function_typ env topt body in
  -    let body, cbody, guard_body = tc_term ({envbody with top_level=false; use_eq=use_eq}) body in
  -
  -    let guard_body =  //we don't abstract over subtyping constraints; so solve them now
  -        Rel.solve_deferred_constraints envbody guard_body in
  -
  -    if Env.debug env <| Options.Other "Implicits"
  -    then BU.print2 "Introduced %s implicits in body of abstraction\nAfter solving constraints, cbody is %s\n"
  -        (string_of_int <| List.length guard_body.implicits)
  -        (Print.comp_to_string <| cbody.comp());
  -
  -    let body, cbody, guard = check_expected_effect ({envbody with use_eq=use_eq}) c_opt (body, cbody.comp()) in
  -    let guard = Rel.conj_guard guard_body guard in
  -//    let guard = match tacopt with
  -//                | None -> guard
  -//                | Some tac -> Rel.map_guard guard (Common.mk_by_tactic tac) in
  +    let tfun_opt, bs, letrec_binders, c_opt, envbody, body, g = expected_function_typ env topt body in
  +    let body, cbody, guard =
  +        let should_check_expected_effect =
  +            match (SS.compress body).n with
  +            | Tm_ascribed (_, (Inr _expected_c, _), _) ->
  +              //body is already ascribed a computation type;
  +              //don't check it again
  +              //Not only is it redundant and inefficient, it also sometimes leads to bizarre errors
  +              //e.g., Issue #1208
  +              false
  +            | _ -> true
  +        in
  +        let body, cbody, guard_body =
  +            tc_term ({envbody with top_level=false; use_eq=use_eq}) body in
  +        let guard_body =  //we don't abstract over subtyping constraints; so solve them now
  +            Rel.solve_deferred_constraints envbody guard_body in
  +        if should_check_expected_effect
  +        then let body, cbody, guard = check_expected_effect ({envbody with use_eq=use_eq}) c_opt (body, cbody.comp()) in
  +             body, cbody, Rel.conj_guard guard_body guard
  +        else body, cbody.comp(), guard_body
  +    in
       let guard = if env.top_level || not(Env.should_verify env)
                   then Rel.discharge_guard envbody (Rel.conj_guard g guard)
                   else let guard = Rel.close_guard env (bs@letrec_binders) (Rel.conj_guard g guard) in
  
positive.code:                 let envbody, bs, g, c = check_actuals_against_formals env bs bs_expected in
                  let envbody, letrecs = if Env.should_verify env then mk_letrec_env envbody bs c else envbody, [] in
                  let envbody = Env.set_expected_typ envbody (U.comp_result c) in
                  Some t, bs, letrecs, Some c, None, envbody, body, g
  
                | _ -> (* expected type is not a function;
                          try normalizing it first;
                          otherwise synthesize a type and check it against the given type *)
                  if not norm
                  then as_function_typ true (N.unfold_whnf env t)
                  else let _, bs, _, c_opt, tacopt, envbody, body, g = expected_function_typ env None body in
                        Some t, bs, [], c_opt, tacopt, envbody, body, g in
            as_function_typ false t
      in
  
  
negative.code:         * binders             (* binders from the abstraction checked against the binders in the corresponding Typ_fun, if any *)
          * binders             (* let rec binders, suitably guarded with termination check, if any *)
          * option<comp>        (* the expected comp type for the body *)
          * Env.env             (* environment for the body *)
          * term                (* the body itself *)
          * guard_t)            (* accumulated guard from checking the binders *)
  