+Open Scope string_scope.
+Fixpoint kindToString (k:Kind) : string :=
+ match k with
+ | KindStar => "*"
+ | KindArrow KindStar k2 => "*=>"+++kindToString k2
+ | KindArrow k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
+ | KindUnliftedType => "#"
+ | KindUnboxedTuple => "(#)"
+ | KindArgType => "??"
+ | KindOpenType => "?"
+ end.
+Instance KindToString : ToString Kind := { toString := kindToString }.
+
+Notation "'★'" := KindStar.
+Notation "a ⇛ b" := (KindArrow a b).
+
+Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
+ match k with
+ | ★ => rawLatexMath "\star"
+ | ★ ⇛ k2 => (rawLatexMath "\star\Rightarrow ")+++kindToLatexMath k2
+ | k1 ⇛ k2 => (rawLatexMath "(")+++kindToLatexMath k1+++(rawLatexMath ")\Rightarrow ")+++kindToLatexMath k2
+ | KindUnliftedType => rawLatexMath "\text{\tt{\#}}"
+ | KindUnboxedTuple => rawLatexMath "\text{\tt{(\#)}}"
+ | KindArgType => rawLatexMath "\text{\tt{??}}"
+ | KindOpenType => rawLatexMath "\text{\tt{?}}"
+ end.
+Instance KindToLatexMath : ToLatexMath Kind := { toLatexMath := kindToLatexMath }.