[isabelle-dev] Fwd: A possible bug with Isabelle 2013

Makarius makarius at sketis.net
Wed Feb 27 15:28:37 CET 2013

On Wed, 27 Feb 2013, Lawrence Paulson wrote:

> A behaviour where "..." denotes something other than the previous 
> right-hand side needs to be fixed.

Again this odd "bug -- fixed" terminology. Such problems are much deeper.

Fortunately, the solution for overly polymorphic results, and the extreme 
form of so-called hidden-polymorphism, has been mostly there for several 
years.  We had really big structural problems in the past, but this is now 

What is missing is some immediate visual feedback about what the system 
has produced from user input.  This applies to plain Hindley-Milner 
generalization, implicit itself arguments, and coercions.

Note that in mainstream programming communities, even just Hindley-Milner 
without anything in addition is often found in the "type-inference sucks" 
corner of discussion forums.


More information about the isabelle-dev mailing list