Re: [isabelle] adhoc_overloading raises TYPE in locale when coercions are enabled
Am 18.11.2013 10:29, schrieb Dmitriy Traytel:
OK, I reintroduced it myself (f6ffe53387ef ). Christian, if the removal
was on purpose, please give some motivation.
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
Later, in Isabelle/54e290da6da8 in conjunction with
Isabelle/e13b0c88c798 this check was (accidentally?) removed.
Christian, would you please reintroduce it?
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
Additionally, I'll think about changing the behaviour on the coercions
This archive was generated by a fusion of
Pipermail (Mailman edition) and