[Ur] Incompatible kinds

[Adam Chlipala]

Karn Kallio wrote:
>   Wrong kind
> Constructor:  (fn x ::<UNIF:U116>  =>  (fn y ::<UNIF:U116>  =>  x))
>    Have kind:<UNIF:U116>  ->  <UNIF:U116>  ->  <UNIF:U116>
>    Need kind:  B -->  B ->  B ->  B
> Incompatible kinds
> Kind 1:<UNIF:U116>  ->  <UNIF:U116>  ->  <UNIF:U116>
> Kind 2:  B -->  B ->  B ->  B
>
>  From the error message ( incompatible kinds when as I understand it they
> should be compatible ) I think this is an example of incompleteness in the
> kind unification.
>    

You're right.  I've only implemented kind polymorphism in a way similar 
to let-polymorphism in ML.  You can't really treat kind-polymorphic 
constructors as first-class.