anchor.diff:      | Type_t u ->
         S.mk (Tm_type u) None Range.dummyRange
   
  -    | Lam (f, q) ->
  -      let x = S.new_bv None S.tun in
  +    | Lam (f, t, q) ->
  +      let x = S.new_bv None (readback env t) in (* (readback env t) is the type of the binder *)
         let body = readback env (f (mkAccuVar x)) in
         U.abs [(x, q)] body None
   
  
positive.code: 
      | Tm_abs ([x], body, _) ->
        debug (fun () -> BU.print2 "Tm_abs body : %s - %s\n" (P.tag_of_term body) (P.term_to_string body));
        Lam ((fun (y:t) -> translate env (y::bs) body), snd x)
  
      | Tm_abs (x::xs, body, _) ->
        let rest = S.mk (Tm_abs(xs, body, None)) None Range.dummyRange in
  
negative.code: let rec app (f:t) (x:t) (q:aqual) =
    debug (fun () -> BU.print2 "When creating app: %s applied to %s\n" (t_to_string f) (t_to_string x));
    match f with
    | Lam (f, _, _) -> f x
    | Accu (a, ts) -> Accu (a, (x,q)::ts)
    | Construct (i, us, ts) ->
      (match x with
  