Internal error on confluence check when rewriting a defined symbol with a hole

[ionathanch]

Internal error on confluence check when rewriting a defined symbol with a hole

[jespercockx]

Thank you for reporting. The problem here is that the confluence checker assumes there are no metavariables in any of the rewrite rules it gets. This is true for normal rewrite rules, since the REWRITE pragma makes sure that the rule is fully instantiated before adding it to the signature. However, the confluence checker also takes into account the clauses of regular pattern-matching definitions, and THOSE might contain unsolved metas, as is the case for myrefl. Possible solutions:

• Refuse to add any rewrite rules to a function if there are still unsolved metas in the definition of that symbol and the confluence checker is on (the simplest but crudest solution).
• Postpone the confluence check by adding it as a new constraint (@liesnikov is gonna love this) and retrying the check once all the metas have been resolved.
• Actually do something smart with metavariables in the confluence checker, which would likely adding a constraint for syntactic equality of terms (up to instantiation of metavariables).
• Or we could even make the confluence checker instantiate the metavariables to the correct solution that makes the rewriting system confluent. In the example here that would mean the ? would be instantiated to refl (at least when you would put the whole thing in a mutual block).

I think the first option is what I'll implement for now, but the others are certainly interesting to think about.