Email Gateway (Aug 19 2022 at 12:31): Email Gateway (Aug 19 2022 at 12:31):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 19 2022 at 12:32):From: Dmitriy Traytel <traytel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 12:33):From: Dmitriy Traytel <traytel@in.tum.de>
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
Email Gateway (Aug 19 2022 at 12:39):From: Makarius <makarius@sketis.net>
Syntax.uncheck_terms is indeed required to allow printing of bad terms,
otherwise most error messages would be impossible to deliver. The burden
here is on all user-space tools that add to that abstract syntax phase via
Syntax_Phases.term_uncheck.
These are not everyday user applications, but user-space nonetheless --
analogous to simplification procedures written in Isabelle/ML.
The particular problem with adhoc_overloading is addressed in the next
release (in about 1 week).
Makarius
Last updated: Apr 26 2024 at 12:28 UTC