empty と non-emptyを型で分離した上で、という話じゃなくなってしまうのですが。
GADT による制限で
GADT による制限で
Nil は Branch にも Tip にも持たれないので、空の Patricia を表現するときだけに使われると思っていいですよね。もしそうなら、`Patricia` が必ず1つ以上の要素をもつ (`Semigroup` みたいに) としてしまえば Nil がなくなって inhabited を区別しなくてよくなり、existential type もいらなくなると思ったのですが、そういうのってありなんでしょうか。empty がなくなると不便ですかね。