[isabelle-dev] Abbreviations + Monad_Syntax introduce "unit itself" additional type variable

[Florian Haftmann]

Reviving this old thread, Peter and me found out what is actually going
on here.

Basically, nothing wrong.  When abbreviations are declared, terms are
checked such that no abbreviations themselves are expanded.  So in the
examples, the do-syntax produces an abbreviation bind_do which in this
case is not unfolded and so does not trigger the adhoc-overloading
disambiguation of bind.  So, there is nothing wrong here.

Even more, given the analogy that ad-hoc overloading represents some
kind of overloaded abbreviations, adhoc-overloading should never be
expanded while abbreviations are checked (query
Proof_Context.abbrev_mode).  @Christian.  You might consider to adjust
your code accordingly after a second round of thinking about.

Cheers,
	Florian


On 13.10.2013 17:36, Florian Haftmann wrote:
>>> Here a bisect would be helpful when this came to happen
>>> actually (or is it already present in Isabelle2013).
>>
>> This one already goes wrong in Isabelle2013.
> 
> OK.  I guess it is some variant of the ever recurring problem of »hidden
> polymorphism«.  Will take some time to figure out actually.
> 
> 	Florian
> 
> 
> 
> _______________________________________________
> 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: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131205/587ef686/attachment.asc>