Stateモナドで結合を制限できませんか？

例えば状態としてスタックがある場合
push :: forall n, a -> State (Stack (n :+: 1)) ()
pop :: forall n m, n :+: 1 :==: m => State (Stack n) a
みたいに型の制約付きでpush,popが定義されていて、
空スタックを表現する型付きの値をpopすると型システムに弾かれるようなやつです