いわゆる依存型だよね
素朴に導入する静的な型推論が決定不能になるんじゃなかったっけ