``` coq Inductive T : let U := Type in U := t. (* Anomaly: not an arity. Please report. *) ``` This works in trunk, but not in trunk-polyproj.