anchor.diff:                              (Print.tag_of_term t1) (Print.tag_of_term t2)
                               (Print.term_to_string t1) (Print.term_to_string t2)) t1.pos
   
  -      | _ -> giveup env "head tag mismatch" orig
  +      | _ -> giveup env (Thunk.mkv "head tag mismatch") orig
   
   and solve_c (env:Env.env) (problem:problem<comp>) (wl:worklist) : solution =
       let c1 = problem.lhs in
  
positive.code:                     end
                  in aux wl us
  
              | _ -> UFailed (BU.format3 "Unable to unify universes: %s and %s (%s)" (Print.univ_to_string u1) (Print.univ_to_string u2) msg) in
  
      match u1, u2 with
          | U_bvar _, _
  
negative.code:             solve_t env (problem_using_guard orig t1 problem.relation t2 None "result type") wl
  
           | GTotal _, Total _ ->
              giveup env (Thunk.mkv "incompatible monad ordering: GTot </: Tot")  orig
  
           | Total  (t1, _), Total  (t2, _)
           | GTotal (t1, _), GTotal (t2, _) -> //rigid-rigid 1
              solve_t env (problem_using_guard orig t1 problem.relation t2 None "result type") wl
  
           | Total  (t1, _), GTotal (t2, _) when problem.relation = SUB ->
              solve_t env (problem_using_guard orig t1 problem.relation t2 None "result type") wl
  
           | Total  (t1, _), GTotal (t2, _) ->
              giveup env (Thunk.mkv "GTot =/= Tot") orig
  
           | GTotal _, Comp _
           | Total _,  Comp _ ->
  