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

[Christian Sternagel]

Dear Florian,

sorry, I fail to understand both parts of your message ;)

First, I do not understand your justification why nothing is wrong. 
Could you elaborate?

Second, are you saying that ad-hoc overloading should not be expanded on 
rhss of abbreviations. If so, why? For me that does not sound desirable.

cheers

chris

On 12/05/2013 05:05 PM, Florian Haftmann wrote:
> 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
>>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>