[isabelle-dev] type unification

[Makarius]

On Thu, 11 Jul 2013, Christian Sternagel wrote:

> Dear list,
>
> what is the proper way of obtaining a type from a term, in case I want 
> to give it as argument to Sign.typ_unify (of Sign.typ_match for that 
> matter)?
>
> My question arises as follows. In adhoc_overloading.ML previously 
> Sign.the_const_type was used to obtain the type of a constant. The 
> result is a type with schematic type variables. Now that I want to use 
> terms instead of constants (as strings) I replaced Sign.the_const_type 
> by fastype_of, but this yields a type with fixed type variables and thus 
> unification may fail. So once again: What is the proper way of getting a 
> "schematic" type from a term?

This perfectly normal Isabelle/ML user question is covered to some extent 
in the "implementation" manual, concerning Variable.polymorphic.

The reference in isabelle-dev style is
http://isabelle.in.tum.de/repos/isabelle/annotate/cb6634eb8926/doc-src/IsarImplementation/Thy/Proof.thy#l162 
"The following example shows how to work with fixed term and type 
parameters and with type-inference."


Furthermore, to oral tradition of short Isabelle sayings has this entry 
about it:

   "A local context is characterized by a mixture of free and schematic
   variables.  Flipping coins via varify / unvarify only works in a global
   context."


 	Makarius