Re: [isabelle] adhoc_overloading raises TYPE in locale when coercions are enabled



Am 18.11.2013 10:29, schrieb Dmitriy Traytel:
Hi Andreas,

the problem is that the coercion inference needs/wants to pretty print an error message containing an type-incorrect term. The uncheck phase of adhoc_overloading (that is performed during pretty printing) chokes on this. We had a similar interaction between other type inference phases and adhoc overloading before. That's why I've forced adhoc_overloading to leave type-incorrect terms alone in Isabelle/e2d08b9c9047.

Later, in Isabelle/54e290da6da8 in conjunction with Isabelle/e13b0c88c798 this check was (accidentally?) removed. Christian, would you please reintroduce it?
OK, I reintroduced it myself (f6ffe53387ef ). Christian, if the removal was on purpose, please give some motivation.

Additionally, I'll think about changing the behaviour on the coercions side.
Now that I thought about it: since the coercion inference reports an error, I cannot guarantee that some subterm of the type-incorrect term is well-typed in general (so I barely can print anything, if printing requires well-typed terms). Hence, uncheck should better work with type-incorrect terms.

Dmitriy



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.