Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Type unification failed

Email Gateway (Aug 18 2022 at 18:16):

From: John Munroe <munddr@gmail.com>
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

Email Gateway (Aug 18 2022 at 18:16):

From: Ramana Kumar <rk436@cam.ac.uk>
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".

Email Gateway (Aug 18 2022 at 18:16):

From: "\"Mark\"" <mark@proof-technologies.com>
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@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@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

Email Gateway (Aug 18 2022 at 18:16):

From: Makarius <makarius@sketis.net>
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

Last updated: Nov 21 2024 at 12:39 UTC