anchor.diff:      debug (fun () -> BU.print1 "Readback: %s\n" (t_to_string x));
       match x with
       | Univ u -> failwith "Readback of universes should not occur"
  -
  +    
  +    | Unknown -> S.mk Tm_unknown None Range.dummyRange
  +    
       | Constant Unit -> S.unit_const
       | Constant (Bool true) -> U.exp_true_bool
       | Constant (Bool false) -> U.exp_false_bool
  
positive.code:     (match x with
       | Univ u -> Construct (i, u::us, ts)
       | _ -> Construct (i, us, (x,q)::ts))
    | Constant _ | Univ _ | Type_t _ -> failwith "Ill-typed application"
  
  and iapp (f:t) (args:list<(t * aqual)>) =
    match args with
  
negative.code:   | Constant of constant
    | Type_t of universe
    | Univ of universe
    | Unknown (* For translating unknown types *)
    // NS:
    // | Refinement of binder * t
    // | Arrow of list binder * comp_t
  