長さ付きのスタックから残りの長さを取得する型関数RestLenがあるとして、
例えば実行するのにスタックをm消費する関数fがあると
f :: ((LestLen s) :<: m, n' ~ n - m ,s ~ Stack n a) => Stack n a -> Stack n' a
みたいな感じで制約付きの関数が定義できるといいかもなーとか考えてるんだけど
できそうにないのか残念