have a brief look at one of the infer_d_complete cheats

not really any progress. feels like there's an extra bind_tvar in the
implementation (or something missing in the theorem statement).