anchor.diff:        let body = SS.subst subst body in
   
         let ret_type =
  -        match (SS.compress t).n with
  +        (* match (SS.compress t).n with
           | Tm_arrow (binders, comp) ->
               let binders, comp = open_comp binders comp in
               begin match comp.n with
               | Total t | GTotal t | Comp { result_typ = t } ->
                   t
  -            end
  +            end *)
  +        match what with
  +        | Some (Inl { res_typ = t }) ->
  +            t
           | _ ->
  -            failwith "impossible"
  +            failwith "what impossible"
         in
   
         let binders = List.map (fun (bv, qual) ->
           let sort = star_type bv.sort in
           { bv with sort = sort }, qual
         ) binders in
  -      let body = star_expr body ret_type (if is_monadic what then InMonad else InPure) in
  +      let body = star_expr body (if is_monadic what then InMonad ret_type else InPure) in
         let body = close binders body in
         let binders = close_binders binders in
  -      mk (Tm_abs (binders, body, what))
  +      wrap_if m (mk (Tm_abs (binders, body, what)))
   
     | Tm_ascribed (e, _, _) ->
  -      star_expr e t m
  +      star_expr e m
   
     | Tm_match (e0, branches) ->
  -      // Assuming here that this is not a dependent pattern-matching and all
  -      // branches match on the same type
  -      let t0 = match branches with
  -      | ({ ty = t0 }, _, _) :: _ ->
  -          t0
  -      | _ ->
  -          raise (Err ("No empty pattern-matches in the definition language"))
  -      in
         // TODO: currently, no one is checking that [e0] is a pure computation
  -      let e0 = star_expr e0 (mk t0) InPure in
  +      let e0 = star_expr e0 InPure in
         let branches = List.map (fun b ->
           match open_branch b with
           | pat, None, body ->
  -            let body = star_expr body t m in
  +            let body = star_expr body m in
               close_branch (pat, None, body)
           | _ ->
               raise (Err ("No when clauses in the definition language"))
  
positive.code:       mk (Tm_match (e0, branches))
  
    | Tm_app (head, args) ->
        failwith "TODO: Tm_app"
  
  
    | Tm_bvar _ ->
        failwith "TODO: Tm_bvar"
    | Tm_name _ ->
        failwith "TODO: Tm_name"
    | Tm_fvar _ ->
        failwith "TODO: Tm_fvar"
    | Tm_uinst _ ->
        failwith "TODO: Tm_uinst"
    | Tm_constant _ ->
  
negative.code:       let x_binders, e2 = SS.open_term x_binders e2 in
        // Two cases.
        if is_monadic then begin
          match m with
            | InPure ->
                raise (Err ("monadic [let] in a context that does not return [M]"))
            | InMonad t ->
                // p: A* -> Type
                let p_type = mk_star_to_type t in
                let p = S.gen_bv "p" None p_type in
                // e1*
                let e1 = star_expr e1 InPure in
                // e2*
                let e2 = star_expr e2 m in
                // e2* p
                let e2 = mk (Tm_app (e2, [ mk (Tm_bvar p), S.as_implicit false ])) in
                // fun x -> e2* p; this takes care of closing [x].
                let e2 = U.abs x_binders e2 None in
                // e1* (fun x -> e2* p)
                let body = mk (Tm_app (e1, [ e2, S.as_implicit false ])) in
                U.abs [ S.mk_binder p ] body None
        end else
          let e1 = star_expr e1 InPure in
          let e2 = star_expr e2 InPure in
          mk (Tm_let ((false, [ { binding with lbdef = e1 } ]), SS.close x_binders e2))
  
    | Tm_let _ ->
        raise (Err ("[let rec] and [let and] not supported in the definition
  