higher kinded typeでやりたいのって functor みたいな制約を書いたり、 functor に対して抽象的に map を使ったコードが書けたりってことじゃないですか？ some P はプロコトルの制約として使えないから難しそうな気が。