The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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.