bblum

137     and subkind g Ktype Ktype = ()138       | subkind g Ktype (Ksing _) = ()139       | subkind g (Ksing _) Ktype = ()140       | subkind g (Ksing c1) (Ksing c2) = equiv g c1 c2 Ktype141       | subkind g (Kpi (a,k1,k2)) (Kpi (a',k1',k2')) =142         let143           val _ = subkind g k1' k1 (* with contravariance *)144           val alpher = Variable.newvar()145         in146           subkind (Variable.extend g alpher k1') (Subst.krename alpher a k2)147                                         (Subst.krename alpher a' k2')148         end149       | subkind g (Ksigma (a,k1,k2)) (Ksigma (a',k1',k2')) =150         let151           val _ = subkind g k1 k1' (* without contravariants *)152           val alpher = Variable.newvar()153         in154           subkind (Variable.extend g alpher k1) (Subst.krename alpher a k2)155                                        (Subst.krename alpher a' k2')156         end157       | subkind g _ _ = raise TypeError