The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Currently, coq complains that a coercion does not respect the uniform inheritance condition if some parameters to the coercion function do not show up as parameters to the source type.  It seems to me that if these parameters are typeclasses or canonical structures, it should still be permissible to declare the coercion, and let the typeclass/canonical structure machinery pick up the missing parameters.  However, this is not the case, and instead I get a warning and then "Anomaly: apply_coercion_args: mismatch between arguments and coercion." when I try to use it.  I would like this, for example, when I use the Funext typeclass from homotopy type theory, and want to declare a coercion from one definition that does not use Funext to another definition which does use Funext, conditional on there being an instance of Funext around. 

It seems also that it should be possible to weaken the uniform inheritance condition so that a coercion is permissible if every parameter to the coercion function shows up either as a parameter to the source class, or as a parameter to the target class.

Am I ignorant of any theoretical or practical issues that would make this unsound or hard to implement?

Thanks,

Jason