tailが動くものが作れたので公開しておきますです＞ω＜　型安全なリストですー＞ω＜

SafeList_by_GADTs.hs

-- Generalized Algebraic Data Types(一般的代数データ型)が使えるようになるみたいです＞ω＜
{-# LANGUAGE GADTs #-}
module Main where
import Prelude hiding (head, tail, map)

-- EmptyとNonEmptyもリストのような構造にすることで、
-- あと何回tailすることが出来るのか、という情報を保持しますです＞ω＜
data Empty
data NonEmpty x

-- Phantom Typeではラッパー関数が必要でしたけれど、
-- GADTではデータ構築子の返す型を別々にできるみたいですー＞ω＜
-- シンプルで堅牢で、とても素敵ですっ＞ω＜
infixr 5 :::
data SafeList x a where
  Nil :: SafeList Empty a
  (:::) :: a -> SafeList x a -> SafeList (NonEmpty x) a

head :: SafeList (NonEmpty x) a -> a
head (x ::: _) = x

tail :: SafeList (NonEmpty x) a -> SafeList x a
tail (_ ::: xs) = xs

map :: (a -> b) -> SafeList x a -> SafeList x b
map _ Nil = Nil
map f (x ::: xs) = f x ::: map f xs

-- Windowsだと文字化けするのでShiftJISを直接埋め込んでますです＞ω＜
wafu = "\x81\x84\x83\xd6\x81\x83"

main = do
  putStrLn $ head (wafu ::: Nil) -- これはOK(*・ω・*)
  putStrLn $ head (tail (wafu ::: wafu ::: Nil)) -- tailが二重に絡んでも無問題なのです＞ω＜
--  print $ head Nil -- 例によってコンパイル時にエラーです＞ω＜
--  print $ head tail (Cons wafu Nil) -- これも当然エラーです＞ω＜