Deciding type equivalence in the presence of singleton kinds, through translation into the canonical presentation.
Karl Crary. A syntactic account of singleton types via hereditary substitution. LFMTP, 2009. DOI: https://doi.org/10.1145/1577824.1577829.