Phantom Type(幽霊型)を使った型安全なリストですー＞ω＜ まだ勉強中なので間違っているところがあるかもしれませんが、そういうときは斜め四十五度からのツッコミを決めてもらえると嬉しいですっ＞ω＜

StrongList.hs

-- 存在量子化されたデータ構築子が使えるみたいです＞ω＜←よく分かってないヾ(ﾟДﾟ )ｫｨｫｨ
{-# LANGUAGE ExistentialQuantification #-}
module Main where
import Prelude hiding (head)

data Empty
data NoEmpty
data StrongList a x = forall y. Cons a (StrongList a y)
                               |Nil

-- 上のStrongListだけでは型が決定されないのでラップする関数が要ります＞ω＜
-- GADTsならデータ構築子側で型を決定できるみたいですが…
-- もし決定できる方法があれば教えてくださいですー＞ω＜
nil :: StrongList a Empty
nil = Nil
cons :: a -> StrongList a x -> StrongList a NoEmpty
cons x ys = Cons x ys

head :: StrongList a NoEmpty -> a
head (Cons x _) = x

main = do
  print $ head (cons "＞ω＜" nil)
  print $ head nil -- コンパイル時にエラーになります＼_(・ω・`)ココ重要！