The Coq mailing list

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

Yes, there are nested patterns.
> sometimes Coq isn't very good at trying to infer the correct return clause
But he shouldn't try to infer it, only check. Coq already inferred correct type
Container (Tag2Type TagA) and it is remained only to normalize it.

Anyway, I think that I can redesign the codebase to avoid such matching.

Sincerely,
Kirill Taran

On Fri, Feb 14, 2014 at 2:25 AM, Daniel Schepler <dschepler AT gmail.com> wrote:

I don't think it's likely that unification is stopping too early.  But
if you have nested match statements, and some of the inner matches
don't have their own return clauses, then sometimes Coq isn't very
good at trying to infer the correct return clause (which is
unfortunate as the necessary nested return types often end up with
long expansions from the outer return type).  That would be my first
guess, without having more information to go on.
--
Daniel Schepler

On Thu, Feb 13, 2014 at 2:03 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:
> 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