The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Ben Horsfall wrote:
> Suppose I'm trying to define an inductive relation on terms that have
> an indexed type (i.e. Inductive tm : ty ->  Set), and I have also
> defined some Fixpoints f, g (let's say of type ty ->  ty for
> simplicity). Suppose also that I know that f x == g y (decidable
> equality). Is there a way to induce the type checker to unify types tm
> (f x) and tm (g y)? This should not require the fixpoints to be
> computed during type-checking, only judicious use of a known equality.
> Or is there a better way to approach this kind of difficulty?
>    

Coq's type theory definitely doesn't support this.  I don't know the 
details of your problem, but it's possible you could get the result you 
desire just by adding explicit equality premises to some constructors of 
some inductive definitions.

I'm dubious about the broader idea, though, since, even if we put off 
your question about type-checking convenience, I don't believe [f x == g 
y -> tm (f x) = tm (g y)] will be provable, in general, for an arbitrary 
[==].  Almost no equalities between types are provable in Coq, beyond 
those where the two types are syntactically equal.  Perhaps if you added 
an _axiom_ justifying the inference you want, you would be able to use 
the Program feature to queue up equality statements that you could then 
discharge with the axiom.  I don't understand Coq metatheory well enough 
to give conditions under which such an axiom would be consistent.