Re: [isabelle] Type unification failed

One more aspect: the language of type constraints admits nameless dummies that *are* unified. For example

  term "(f :: _ => nat) (a::nat)"

Sort constraints may be also added here:

  term "(f :: _::plus => nat) (a::nat)"

The ML interfaces of the "term check" phase also admits named unification parameters (via Type_Infer.param), but this is an advanced concept without notation for end-users (as in ML/Haskell).


On Mon, 29 Aug 2011, "Mark" wrote:

It should be said that types explicitly provided in type annotations in term
quotations are not unified by the type checker, they are simply left as they
are, whereas implicit types in term quotations are unified.

on 29/8/11 8:07 AM, Ramana Kumar <rk436 at> wrote:

Because 'a is not equal to nat and in the first case you are asking for
to be the same.

In the second case, f is first specified to be polymorphic then the use,
"f a", is instantiated appropriately by type inference, that is, you
have "(f::nat => nat) a", which is allowed because "nat => nat" refines
=> nat".

On Aug 29, 2011 7:42 AM, "John Munroe" <munddr at> wrote:


Does anyone know why there's a type error in

ML {*
val trm = @{term "(f::'a=>nat) (a::nat)"};

but not in

f:: "'a => nat"
a :: nat

ML {* @{term "f a" *}

Why are the two cases treated differently?



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