[isabelle] Unification bound exceeded on "show"

Hello, I encountered a proof in which the processing of "show ?thesis"
would not terminate, displaying many "Unification bound exceeded" messages.
I reduced it to the following example, where the processing of "show
"P"" does not terminate.
Could anyone explain this behavior? Is it possible to reliably avoid it?
Removing the type annotation ::"'a â 'a â 'a" in the "fix" line resolves
the problem.
However, I don't understand why.
I'm using Isabelle 2015.


theory Test
imports Main

notepad begin
  have "â Q (f::'a â 'a â 'a) P . (âs. Q (f s)) â P"
  proof -
    fix Q and f::"'a â 'a â 'a" and P
    assume "â s . Q (f s)"
    show "P"

Attachment: signature.asc
Description: OpenPGP digital signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.