anchor.diff:  
       | Tm_unknown -> mk A.Wild
   
  -and resugar_ascription env (asc, tac_opt) =
  +and resugar_ascription env (asc, tac_opt, b) =
     (match asc with
      | Inl n -> (* term *)
        resugar_term' env n
      | Inr n -> (* comp *)
        resugar_comp' env n),
  -  BU.map_opt tac_opt (resugar_term' env)
  +  BU.map_opt tac_opt (resugar_term' env),
  +  b
   
   (* This entire function is of course very tied to the the desugaring
   of calc expressions in ToSyntax. This only really works for fully
  
positive.code:               let rec resugar_seq t = match t.tm with
                  | A.Let(_, [_, (p, t1)], t2) ->
                     mk (A.Seq(t1, t2))
                  | A.Ascribed(t1, t2, t3) ->
                     (* this case happens when the let is wrapped in Meta_Monadic which is resugared to Ascribe*)
                     mk (A.Ascribed(resugar_seq t1, t2, t3))
                  | _ ->
                     (* this case happens in typechecker.normalize when Tm_let is_pure_effect, then
                        only the body of Tm_let is used. *)
  
negative.code:                   List.map resugar_branch branches))
  
      | Tm_ascribed(e, asc, _) ->
        let asc, tac_opt, b = resugar_ascription env asc in
        mk (A.Ascribed (resugar_term' env e, asc, tac_opt, b))
  
      | Tm_let((is_rec, source_lbs), body) ->
        let mk_pat a = A.mk_pattern a t.pos in
  