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

[Christian Sternagel]

Reviving this old thread once more ;)

I think I need some clarifications first:

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.
Does that also mean that the resulting "unit itself" is as you would 
expect in the following?

   abbreviation
     "abbr2 == do {
       Some ();
       Some False
     }" -- "additional type variable"

>
> 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.
>
By "expanding adhoc overloading" do you mean replacing concrete 
constants by overloaded generic ones?

When is Proof_Context.abbrev_mode actually true?

What I first thought was that I should avoid to insert overloaded (i.e., 
generic constants; cf. Adhoc_overloading.insert_overloaded) constants 
whenever Proof_Context.abbrev_mode is true. But just trying this on some 
examples did not change anything (as far as I can tell).

What's the concrete suggestion?

cheers

chris