The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

You're right, the later is more likely to break. It all depends which part of your term are inferred with backtracking and which are printed. We should have infer(print_all t) = t now that universes and existentials can be parsed back. I explained myself poorly, what I wanted to convey is that this opened even more ways for ambiguity, although with type classes and the like you can already be quite ambiguous. You're right that the first solution should stay the same.

Cheers,
-- Matthieu

Le mer. 16 mars 2016 à 20:36, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> a écrit :

Usually one wants some control on what is produced, and the current type inference 

provides some, with the (informal) guarantee that print(infer(t)) = t. This determinism

can go away as soon as proof search is involved though, through type classes for 

example, and means to ensure that this search is predictable are useful too.

 

We'd rather like infer(print(t)) = t, I suppose. Neither are true in Coq, I don't know which is less true. I don't see how non-determinism affects print(infer(t)) = t. It may affect infer(print(t))=t, but let's keep in mind that, in most cases, a backtracking pretyper would return the first solution, which would be the same as a non-backtracking one. Also, we can already simulate non-determinism by specifying implicit arguments to values which are not found by the pretyper. In theory at least, the situation would not be significantly worse than today. Of course, in practice it may feel rather unpleasant, I don't know.