Using "type"

[Samuel E. Moelius III]

I apologize if this question has been asked before...

It seems to me the following code should be legal:

	type Thing m = m ()
	
	type Const a b = a
	
	f :: Thing m -> Thing m
	f x = x
	
	test :: Thing (Const Int) -> Thing (Const Int)
	test = f

However, GHC gives the following error:

     Couldn't match `Thing m' against `Thing (Const Int)'
         Expected type: Thing m
         Inferred type: Thing (Const Int)
         Expected type: Thing (Const Int) -> Thing (Const Int)
         Inferred type: Thing m -> Thing m

But if you change the definition of Const

	newtype Const a b = MakeConst a

the code compiles fine.

Is this the desired behavior?

Is it the case that when you have quantification of a type variable of 
kind * -> * (in this case, m), that variable may only become bound to a 
type constructor?

Sam Moelius