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


	Makarius


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 cam.ac.uk> wrote:

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

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

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

Hi,

Does anyone know why there's a type error in

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

but not in

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

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

Why are the two cases treated differently?

Thanks

John









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