anchor.diff:     match (SS.compress e).n with
      | Tm_bvar _
      | Tm_unknown
  -   | Tm_delayed _ -> failwith "Impossible"
  +   | Tm_delayed _ ->
  +     failwith ("TcTerm.universe_of:Impossible (bvar/unknown/lazy) " ^
  +               (Print.term_to_string e))
      //normalize let bindings away and then compute the universe
      | Tm_let _ ->
        let e = N.normalize [] env e in
  
positive.code:     in
  
      let e =
        let mk_match scrutinee =
          (* TODO (KM) : I have the impression that lifting here is useless/wrong : the scrutinee should always be pure... *)
          (* let scrutinee = TypeChecker.Util.maybe_lift env scrutinee c1.eff_name cres.eff_name c1.res_typ in *)
          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
  
negative.code:     let e, cres, g_expected_type =
        match ret_opt with
        | None -> e, cres, Env.trivial_guard
        | _ -> comp_check_expected_typ env e cres in
  
      if debug env Options.Extreme
      then BU.print2 "(%s) Typechecked Tm_match, comp type = %s\n"
  