GADTs.hs

{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE GADTs              #-}
{-# LANGUAGE KindSignatures     #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators      #-}
import GHC.TypeLits

data Stack :: * -> Nat -> * where
    Nil  :: Stack t 0
    Cons :: a -> Stack a b -> Stack a (1 + b)

deriving instance Show a => Show (Stack a b)

pop :: Stack a (1 + b) -> (a, Stack a b)
pop (Cons a b) = (a, b)

push :: a -> Stack a b -> Stack a (1 + b)
push = Cons

empty :: Stack t 0
empty = Nil

gistfile1.txt

[1 of 1] Compiling Main             ( GADTs.hs, interpreted )

GADTs.hs:15:22:
    Could not deduce (b1 ~ b)
    from the context ((1 + b) ~ (1 + b1))
      bound by a pattern with constructor
                 Cons :: forall a (b :: Nat). a -> Stack a b -> Stack a (1 + b),
               in an equation for ‘pop’
      at GADTs.hs:15:6-13
      ‘b1’ is a rigid type variable bound by
           a pattern with constructor
             Cons :: forall a (b :: Nat). a -> Stack a b -> Stack a (1 + b),
           in an equation for ‘pop’
           at GADTs.hs:15:6
      ‘b’ is a rigid type variable bound by
          the type signature for pop :: Stack a (1 + b) -> (a, Stack a b)
          at GADTs.hs:14:8
    Expected type: Stack a b
      Actual type: Stack a b1
    Relevant bindings include
      b :: Stack a b1 (bound at GADTs.hs:15:13)
      pop :: Stack a (1 + b) -> (a, Stack a b) (bound at GADTs.hs:15:1)
    In the expression: b
    In the expression: (a, b)