The TILT compiler for Standard ML represents programs internally
  using a predicative lambda calculus based on Girard's $F_\omega$.
  At the kind level, this language is notable for containing singleton
  kinds and dependent product and function kinds.  Previous work
  the decidability of type equivalence for this language.
  
  This paper presents a typechecking algorithm for the full TILT
  internal language and discusses some of the more interesting
  features of the language.  The particular use of intensional type
  analysis to handle arrays of unboxed floating point numbers is
  described.  An extended calculus is also introduced which permits
  unlabelled singletons at higher kind, in order to allow for more
  compact program representation.  The extended calculus is related to
  the restricted calculus via a transformation that eliminates the
  unlabelled singletons, and the decidability of the typechecking
  algorithms for both the original and extended calculus is shown.