``` coq Inductive test : $(let U := type of Type in exact U)$ := t. (* Anomaly: Unable to handle arbitrary u+k <= v constraints. Please report. *) ```