[isabelle-dev] TYPE_MATCH exception with adhoc_overloading
florian.haftmann at informatik.tu-muenchen.de
Thu Jan 29 19:44:26 CET 2015
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
> 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
All the best,
> 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 ...
>>> 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
>> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev