[isabelle] Adhoc Overloading and Coercion not working well



I'm not sure if this is the wrong place to post my question, but basically, adhoc_overloading's are failing to resolve when a coercion also needs to be inserted, here is the simplest example I could construct:

datatype A = makeA
datatype B = makeB A
declare [[coercion_enabled, coercion makeB]]

abbreviation barB :: ‹B ⇒ bool› where ‹barB b ≡ True›

consts foo :: ‹'a ⇒ 'b  ⇒ bool›
definition fooA :: ‹bool  ⇒ A ⇒ bool› where ‹fooA b a ≡ True›
definition fooB :: ‹nat ⇒ B ⇒ bool› where ‹fooB n a ≡ True›
adhoc_overloading foo fooB

term ‹barB a ∧ fooA True a›
term ‹barB (makeB a) ∧ foo True x›
term ‹barB a ∧ foo True (a :: A)›
term ‹barB a ∧ foo True a› ―‹ERRO: Unresolved adhoc overloading of constant foo :: "[bool, B] ⇒ bool" in term "True ∧ foo True x"; no instances›

Basically, I would assume that the "barB x" call gives a constraint that "x" is coercible to "B", and the call to "foo True x" should give that "x" is coercible to "A", as there are no other possible "foo" implementations (fooB isn't a possibility because True isn't coercible to nat).
Sadly it's not working it out, unless I basically tell it what the type of 'x' needs to be.

Any ideas how I can improve this?

(Alternatively, if I could get it to infer the type of a variable from it's name that might make dealing with overloaded definitions more manageable,
e.g. coq lets you do "Implicit Type a : A." and then it will infer a variable called a or a' a1 etc as having type "A" (unless you give a type)).

— Isaac Oscar Gariano


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