いろいろ実験して、言語リファレンスを読んだ結果、一意性について理解が深まりました。 とりあえず、関数型と一意性の間には、通常の型のように共変反変の関係があります。 ::R a b :== .(a -> b) createR :: *Char -> *(R Int *Char) createR c = (\i = c) f :: u:(R Int *Char) -> u:(R *Int Char) f r = r Start = f (createR 'a') というプログラムは有効なプログラムです。関数fのところで、共変反変の関係が見て取れます。 この結果、抽象型の場合には、共変反変の判断を付けることができないので、 ::R f :: *R -> R f r = r Start = f (createR 1 2 3) というプログラムは、型エラーになります。