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!
Dmitriy

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)"
end

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}"
end

Best,
Andreas





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