[isabelle-dev] TYPE_MATCH exception with adhoc_overloading

[Florian Haftmann]

Am 28.01.2015 um 13:37 schrieb Christian Sternagel:
> During a visit of Florian in Innsbruck we had some discussion on adhoc
> overloading. One suspicion was that schematic type variables from
> variants had to be "paramified" before using the resulting type unifier.
> 
> I tried to do so in the attached patch. Unfortunately, I still obtain
> the following error in
> 
>   ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy
> 
>   Illegal schematic type variable: ?'a2
> 
> Please let me know if you have any comments on this topic (especially on
> what is going on in the function "unify_filter").

The idea was to imitate how regular constants are handled by type
inference.  I am not sure whether I interpreted the sources right during
our session, and I did not have a close look at the patch either.

Beside that, the same applies as mentioned in my previous post on ad-hoc
overloading.

All the best,
	Florian

> 
> cheers
> 
> chris
> 
> On 01/20/2015 06:16 PM, Makarius wrote:
>> On Mon, 19 Jan 2015, Jasmin Blanchette wrote:
>>
>>>> Just a reminder that this old thread is not yet resolved and
>>>> currently I'm essentially stuck.
>>>
>>> I hope somebody who has a clue will answer your email.
>>
>> I still have various "important" markers on this mail thread, to see if
>> I can tell something about it, but I did not manage to pick it up again.
>> It will happen really soon now ...
>>
>>
>>>> drop_semicolons
>>>
>>> I’ve applied and push your first change.
>>>
>>> As for semicolon, the standard style is rather to put them, not to
>>> drop them.
>>
>> Strictly speaking there is no standard for semicolons in Isabelle/ML,
>> only the universal standard of uniformity: a file either has extra
>> semicolons or does not have extra semicolons.
>>
>>
>> More than 20 years ago, semicolons where generally en-vogue, and no
>> surprise for me in SML.  Then they became less popular, e.g. in Scala we
>> now see sophisticated rules for implicit "semicolon inference".  The
>> Isar language has lost its semicolon altogether some weeks ago
>> (5ff61774df11).
>>
>> Over the decades I have occasionally experimented with writing less
>> semicolons in ML, but each time I ran into practical inconveniences
>> concerning error situations (broken partial input), and closed ML
>> modules versus open sequences of declarations (e.g. in the 'ML' command).
>>
>> My present style of doing it (approx. the last 10 years) is somehow
>> optimized in that respect.  Whenever I do serious renovations on some
>> old ML module, I first normalize the semicolon style (and other styles
>> as well), just to save a lot of time in the actual work.
>>
>>
>>      Makarius
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150129/968ae2e8/attachment.sig>