Haskell GADTs baby steps

SafeListExperiments.hs

{-# LANGUAGE GADTs , KindSignatures #-}

data Zero
data Succ a

data List :: * -> * -> * where
  Nil  :: List Zero a
  Cons :: a -> List t a -> List (Succ t) a
  
data AnyList :: * -> * where
  AnyList :: List t a -> AnyList a

safeHead :: List (Succ _t) a -> a
safeHead (Cons x _) = x

safeTail :: List (Succ t) a -> List t a
safeTail (Cons _ tl) = tl

safeFilter :: (a -> Bool) -> List _t a -> AnyList a
safeFilter _ Nil = AnyList Nil
safeFilter p (Cons hd tl)  
  | p hd = case safeFilter p tl of AnyList l -> AnyList $ Cons hd l
  | otherwise = safeFilter p tl 


-- essai

type P1 = Succ Zero
type P2 = Succ P1
type P3 = Succ P2
type P4 = Succ P3

l1 :: List P4 Integer
l1 = Cons 1 $ Cons 2 $ Cons 3 $ Cons 4 $ Nil

testFilter :: [Integer]
testFilter = case safeFilter (odd) l1 of AnyList l -> safeList2List l

safeList2List :: List _t a -> [a]
safeList2List Nil = []
safeList2List (Cons hd tl) = hd : safeList2List tl