{-# LANGUAGE MultiParamTypeClasses
           , FlexibleInstances
           , ExistentialQuantification
           , ExplicitForAll
  #-}

module FinListNew where

class FinList x l where
    toList :: l -> [x]

data ZeroList x    = ZeroList
data SuccList x xs = SuccList x xs

instance FinList x (ZeroList x) where
    toList _ = []
instance (FinList x xs) => FinList x (SuccList x xs) where
    toList (SuccList x xs) = x : toList xs

data FinList' x = forall xs. FinList x xs => FinList' xs

-- to equalize types.
zl' :: x -> ZeroList x
zl' _ = ZeroList

nil' :: x -> FinList' x
nil' x = FinList' $ zl' x

nil :: FinList' x
nil = nil' undefined

cons :: x -> FinList' x -> FinList' x
cons x (FinList' xs) = FinList' $ SuccList x xs

l1 = cons 5 . cons 4 . cons 1 $ nil

-- *DOES* typecheck. But it shouldn't!
lErr ::  FinList' Int
lErr = cons 1 lErr