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



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.