Email Gateway (Oct 06 2021 at 09:40): Email Gateway (Oct 06 2021 at 09:40):From: "Isaac@ecs.vuw.ac.nz" <Isaac@ecs.vuw.ac.nz>
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
Email Gateway (Oct 06 2021 at 12:39):From: Dmitriy Traytel <traytel@di.ku.dk>
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
...
end
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,
Dmitriy
Last updated: Jul 15 2022 at 23:21 UTC