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

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?

Additionally, I'll think about changing the behaviour on the coercions side.

Thanks for the report!

Am 15.11.2013 16:17, schrieb Andreas Lochbihler:
Dear developers of adhoc_overloading and coercions,

When I enable coercions and have imported adhoc_overloading, type-incorrect terms sometimes raise a TYPE exception instead of providing a useful error message - even if there is nothing that adhoc_overloading can replace. In the following example, the ill-typed term at the end gives the following error message:

*** exception TYPE raised (line 319 of "term.ML"):
*** type_of: type mismatch in application
*** ??'b
*** ??'a
*** <malformed>
*** At command "term"

It is relatively hard to realise from this message that the last s should be changed to ().

theory Scratch imports Main "~~/src/Tools/Adhoc_Overloading" begin

declare [[coercion_enabled]]

typedecl ('a, 'b, 'c) foo
typedecl ('a, 'b) bar

consts t1 :: "nat => (unit, 'b option, 'c option) foo"
consts t2 :: "'a => 'b => ('a, 'b) bar"
consts t3 :: "nat => 'a option"

locale l = fixes r :: "'out => 'in set" begin
definition ex :: "('a, 'out, 'in) foo => (('out × 'in), 'a) bar set"
  where "ex x = (let z = r in undefined)"

locale l' = fixes r :: "'m1 => 'm2 set" begin
definition r' :: "'m1 option => 'm2 option set"
  where "r' x = (let z = r in undefined)"
sublocale l r' .
term "ex (t1 s) = {t2 (t3 s, None) s}"


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