(* should mention "the implicit parameter A of eq" *)
Fail Type (forall x, x = x).