Asllow writing fancier kinds. This is in preparation for type primitives/abstract types.

src/Cryptol/Parser.y

@@ -585,6 +585,7 @@ schema_quals                   :: { Located [Prop PName] }
 kind                             :: { Located Kind      }
   : '#'                             { Located $1 KNum   }
   | '*'                             { Located $1 KType  }
+  | kind '->' kind                  { combLoc KFun $1 $3 }
 
 schema_param                   :: { TParam PName }
   : ident                         {% mkTParam $1 Nothing           }

src/Cryptol/Parser/AST.hs

@@ -343,7 +343,7 @@ data Named a = Named { name :: Located Ident, value :: a }
 data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range)
   deriving (Eq, Show, Generic, NFData, Functor)
 
-data Kind = KNum | KType
+data Kind = KNum | KType | KFun Kind Kind
   deriving (Eq, Show, Generic, NFData)
 
 data TParam n = TParam { tpName  :: n
@@ -821,11 +821,13 @@ instance PPName name => PP (Schema name) where
 instance PP Kind where
   ppPrec _ KType  = text "*"
   ppPrec _ KNum   = text "#"
+  ppPrec n (KFun k1 k2) = wrap n 1 (ppPrec 1 k1 <+> "->" <+> ppPrec 0 k2)
 
 -- | "Conversational" printing of kinds (e.g., to use in error messages)
 cppKind :: Kind -> Doc
-cppKind KType = text "a value type"
-cppKind KNum  = text "a numeric type"
+cppKind KType     = text "a value type"
+cppKind KNum      = text "a numeric type"
+cppKind (KFun {}) = text "a type-constructor type"
 
 instance PPName name => PP (TParam name) where
   ppPrec n (TParam p Nothing _)   = ppPrec n p

src/Cryptol/Parser/Position.hs

@@ -120,4 +120,9 @@ instance AddLoc (Located a) where
 at :: (HasLoc l, AddLoc t) => l -> t -> t
 at l e = maybe e (addLoc e) (getLoc l)
 
+combLoc :: (a -> b -> c) -> Located a -> Located b -> Located c
+combLoc f l1 l2 = Located { srcRange = rComb (srcRange l1) (srcRange l2)
+                          , thing    = f (thing l1) (thing l2)
+                          }
+
 

src/Cryptol/TypeCheck/Kind.hs

@@ -206,6 +206,7 @@ withTParams allowWildCards flav xs m
 cvtK :: P.Kind -> Kind
 cvtK P.KNum  = KNum
 cvtK P.KType = KType
+cvtK (P.KFun k1 k2) = cvtK k1 :-> cvtK k2