[Ur] Incompatible kinds

[Karn Kallio]

Hello,

Last night I thought to use the System F embedded at the Ur/Web type/kind 
level to Girard encode some basic datatypes.  From the Ur Reference Manual I 
think we write polymorphic "pi types" with -->, so that in the Boolean case pi 
t. t -> t -> t we write B --> B -> B -> B in Ur/Web and that we write 
polymorphic abstraction ( upper case lambda = \\ , lower case lambda = \ ) \\t 
. \x : t . x as K ==> fn ( x :: K ) => x in Ur/Web. 

However, this does not compile:

con btrue = K ==> fn ( x :: K ) ( y :: K ) => x
con bfalse = K ==> fn ( x :: K ) ( y :: K ) => y

con bnot = fn ( b :: (B --> B -> B -> B) ) => K ==> fn ( x :: K ) ( y :: K ) 
=> b y x

con bnottrue = bnot btrue

giving error message

 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.  But I am not sure I am properly writing bnot in Ur/Web ... 
I am trying to write bnot = \b : Bool . \\t . \x : t . \y : t . b [t] y x  
where Bool is pi t. t -> t -> t and the \\, \ are uppercase, lowercase lambda.

Is this unification incompleteness or am I doing something wrong?