Re: [isabelle] Adhoc Overloading and Coercion not working well

Hi Isaac,

From the point of view of coercion inference, “foo True x” does not impose any constraint on x because of foo’s rather general declared type. In particular, coercion inference (which lives in Pure) knows nothing about adhoc_overloading (which lives in HOL).

As a result, you will either have to write type-correct terms (i.e., not use coercions) or at least make sure that you have enough type annotations for adhoc_overloading to do its work.

As for giving a variable a fixed type, you could fix it in an unnamed context:

context fixes a :: B begin



The idea of “default types” for names/name classes was floating around one day, but it turned out to be not so easy to find a flexible and understandable solution.

Best wishes,

On 5 Oct 2021, at 09:08, Isaac at wrote:

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.