[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.

Thanks,
Giuliano

theory Test
imports Main
begin

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.