[TYPES] Inductive definition of order

[Stefan Holdermans]

L.S.,

In the context of higher-order functions, I remember seeing "order"  
defined by induction over the types of functions.

More precisely, let σ range over types with

   σ ::= base | σ₁ → σ₂ .

Then:

	order(base)	= 0
	order(σ₁ → σ₂)	= max {order(σ₁) + 1, order(σ₂)} .

So far, so good.

But let us now add type variables α and universal quantification:

	σ ::= ... | α | ∀α. σ₁ .

If we are to extend the inductive definition of order accordingly, then

	order(∀α. σ₁)	= order(σ₁)

seems reasonable. But what about order(α)? Should we choose

	order(α)	= 0 ?

Then, curiously an order-k₁ type can then be instantiated with an  
order-k₂ with k₁ < k₂. Are there any scenarios in which this can  
be problematic? Is zero a "fair" order for values of variable type?  
Does it even make sense to talk about the order of a type scheme  
rather than a type? I am just curious... Any references to similar  
definitions of order?

Thanks in advance,

   Stefan