anchor.diff:      let binders = close_binders binders in
       mk (Tm_arrow (binders, effect_marker))
     in
  -  recheck_debug "turned into the effect signature" env effect_signature;
  +  let effect_signature = recheck_debug "turned into the effect signature" env effect_signature in
   
     // TODO: we assume that reading the top-level definitions in the order that
     // they come in the effect definition is enough... probably not
  
positive.code:   let recheck_debug s env t =
      Util.print2 "Term has been %s-transformed to:\n%s\n----------\n" s (Print.term_to_string t);
      let t, _, _ = tc_term env t in
      Util.print1 "Re-checked; got:\n%s\n----------\n" (Print.term_to_string t)
    in
  
    // TODO: check that [_comp] is [Tot Type]
  
negative.code: 
    let dmff_env = DMFF.empty env (tc_constant Range.dummyRange) in
    let dmff_env, wp_type = DMFF.star_type_definition dmff_env repr in
    let wp_type = recheck_debug "*" env wp_type in
  
    // Building: [a -> wp a -> Effect]
    let effect_signature =
  