Extraction drops calls to divergent functions

[gebner]

module Div2

let rec uhoh t : Div t (requires True) (ensures fun _ -> False) = uhoh t

let foo (x: option nat) : Dv string =
  uhoh unit;
  coerce_eq () x

let _ = String.length (foo None) // crash 🎉

I haven't debugged this one yet. FWIW, the bug seems to be related to the final type argument. If I change it to uhoh t (), then the call to uhoh is extracted correctly.