あと、ここに型レベル式が書ける拡張が期待できる