Skew binary tree with the invariants enforced by the type system, using a nested data type.

skewbintree.hs

{-# LANGUAGE GADTs #-}

type Id = Int

data Path a where
  P :: P a -> Path a
  Two :: b -> b -> P (Br b) -> (P (Br b) -> P a) -> Path a
data Br a = Br a Id a
data P a = Nil | Zero (P (Br a)) | One a (P (Br a))

cons :: Id -> Path Id -> Path Id
cons x (P p) = consP x p
cons x (Two y z zs f) = case consP (Br y x z) zs of
  P p -> P (f p)
  Two y' z' zs' f' -> Two y' z' zs' (f . f')

consP :: a -> P a -> Path a
consP x Nil = P $ One x Nil
consP x (Zero xs) = P $ One x xs
consP x (One y xs) = Two x y xs Zero