Implicit constructors defeat syntactic equality

[wilbowma]

currently, implicit parameters confuse our pattern matcher, since the implicits are actually handled by by a new constructor. This became a problem in #103. We have a workaround, but a better work-around would be attaching meta-data to the constructor, and a system by which both the original constructor and the implicit version are always equal in pattern matching, etc.

[stchang]

define-implicit already defines a new pattern expander. Would it be sufficient if this new pattern matcher also matches the old (explicit) constructors?

[wilbowma]

I'm not really sure what the right solution to this is yet. I think the new pattern expander supporting the old would be helpful, though. I think Coq's behavior is that you have to always specify a position for all arguments, even implicit ones, when pattern matching. That is annoying behavior.

Right now, the specific problem is the new pattern matcher we're working on in #103/#105 decides totality by checking that there is a pattern for every constructor, using free-identifier=?. However, if you use a define-implicit constructor in the pattern clause, this doesn't work.

Right now, it has some kind of hack that I don't fully understand to make this work some of the time. For example, in Poly-pairs, you define fst as the implicit version of fst*. You can pattern match on either fst or fst*, and it will work... when you provide an extra keyword argument. However, it doesn't work for :: and cons*.

I think the root cause is probably that we're using free-identifier=? and instead we ought to be doing .. something else.

[stchang]

Yeah using free-id=? might not work because the pattern id is different from the constructor ids (in the match-info).

Are you implementing Coquand's algorithm for totality checking?

[wilbowma]

Don't remember; @pwang347, did you implement a particular algorithm? My guess would be it's ad-hoc, as the framework supports deep pattern matching and other things.

[pwang347]

No specific algorithm, I believe it was ad-hoc with some inspiration from pattern matrices