pop.idr

module Main

data Stack_ : Type -> Type where
  Empty : Stack_ a
  One : Stack_ a -> Stack_ a

-- This is intentionally oversimplified to be the identity function
-- It's just what's left from erasing all irrelevant domain-specific details
-- so we can focus on Idris's type system.
pop_ : Stack_ a -> Stack_ a
pop_ Empty = Empty
pop_ (One s) with (pop_ s)
  pop_ (One s) | Empty = One Empty
  pop_ (One s) | One s' = One (One s')

data DStack : Stack_ a -> Type where
  DOne : {s : _} -> Nat -> DStack s -> DStack (One s)
  DEmpty : DStack Empty

dpop_ : DStack s -> DStack (pop_ s)
dpop_ DEmpty = DEmpty
dpop_ (DOne {s} n ds) with (pop_ s)
  dpop_ (DOne {s} n ds) | Empty = ?foo2
  dpop_ (DOne {s} n ds) | (One y) with (dpop_ ds)
    dpop_ (DOne {s} n ds) | (One y) | DOne n' ds' = ?bar


{-
pop.idr:24:39--24:50:While processing left hand side of with block in with block in dpop_ at pop.idr:24:5--37:1:
Can't solve constraint between:
        One ?s
and
        pop_ ?s
at:
24          dpop_ (DOne {s} n ds) | (One y) | DOne n' ds' = ?bar
                                              ^^^^^^^^^^^
-}

pop2.idr

-- One working version, with the drawback that you have to name every case split.

module Main

data Stack_ : Type -> Type where
  Empty : Stack_ a
  One : Stack_ a -> Stack_ a

flattenPop : Stack_ a -> Stack_ a
flattenPop Empty = One Empty
flattenPop (One s') = One (One s')

pop_ : Stack_ a -> Stack_ a
pop_ Empty = Empty
pop_ (One s) = flattenPop (pop_ s)

data DStack : Stack_ a -> Type where
  DEmpty : DStack Empty
  DOne : Nat -> DStack s -> DStack (One s)

dflattenPop : Nat -> DStack s' -> DStack (flattenPop s')
dflattenPop n DEmpty = DOne n DEmpty
dflattenPop n (DOne m ds) = DOne n (DOne m ds)

dpop_ : DStack s -> DStack (pop_ s)
dpop_ DEmpty = DEmpty
dpop_ (DOne {s} n ds) = dflattenPop n (dpop_ ds)