Finite List - not as easy as I thought

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
{-# 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