The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hello,

I have quiet strange problem with depent pattern matching.
I can't reproduce it on small example and my real code is too complex to paste it here.

But I am trying something like:

match x in Something t return Container (Tag2Type t) with
| ... y => y
| ... z => z
end.

And this doesn't pass type-check with message like:
The term y has type "Container TypeA" while
it is expected to have type "Container (Tag2Type TagA)".

I checked if I am trying to give wrong term:
Eval simpl in Tag2Type TagA gives TypeA, so there is no my mistake, I think.

I suspect, that Coq stops normalization of Container (Tag2Type TagA) too early.
I failed to reproduce error on smaller examples, so maybe reason is too complex structure.
Is there way to force this normalization?

Sincerely,
Kirill Taran