[isabelle] adhoc_overloading removes type constraints



Hi,

in the following theory, the term "overload [] :: bool list" is parsed as "overload [] :: 'a list". It seems there is some accidental erasure of the type constraint in the adhoc overloading mechanism.

(Tested with 2018 and 2019-RC0, so it's not a regression.)

theory Scratch
  imports "HOL-Library.Adhoc_Overloading"
begin

consts someop :: "'a list ⇒ 'a list"
consts overload :: "'a ⇒ 'b"
adhoc_overloading overload someop
term "overload [] :: bool list"
(* Prints:

"overload []"
  :: "'a list"

 *)

By the way, I would like to check whether this mailing list is the right place for sharing this kind of reports.

Best wishes,
Dominique.






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