>>389
空popを制限するだけなら自然数を数える必要はなくて、

http://en.wikibooks.org/wiki/Haskell/GADT
ここのsafelistを参考

{-# LANGUAGE EmptyDataDecls, GADTs #-}

data Empty
data NotEmpty

data Stack a b where
EmptyS :: Stack a Empty
PushS :: a -> Stack a b -> Stack a NotEmpty

pop :: Stack a NotEmpty -> a
pop (PushS x _) = x

push = PushS


pop (push 1 EmptyS) ---> 1
pop EmptyS ---> 型検査ではじかれる Couldn't match expected type `NotEmpty' (略