{-# LANGUAGE MultiParamTypeClasses
           , FunctionalDependencies
           , FlexibleContexts
           , FlexibleInstances
           , UndecidableInstances
           #-}

module FinList where

-- type-level peano numbers
data Zero = Zero
data Succ n = Succ n

class Nat n where
    toInt :: n -> Int
instance Nat Zero where
    toInt _ = 0
instance (Nat n) => Nat (Succ n) where
    toInt (Succ n) = toInt n + 1

-- FinList x n l iff l is a list of x of length l. Because infinite types are
-- not allowed, n is finite.
class (Nat n) => FinList x n l | x n -> l where
    toList :: l -> [x]

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

instance FinList x Zero (ZeroList x) where
    toList _ = []

-- TODO: when I switch UndecidableInstances off, I get
-- finite_list.hs:31:0:
--     Illegal instance declaration for `FinList
--                                         x (Succ n) (SuccList x xs)'
--         (the Coverage Condition fails for one of the functional dependencies;
--          Use -XUndecidableInstances to permit this)
--     In the instance declaration for `FinList x (Succ n) (SuccList x xs)'
-- Why?!?
instance (Nat n, FinList x n xs) => FinList x (Succ n) (SuccList x xs) where
    toList _ = undefined
    -- TODO: this line fails to typecheck. The error is
    -- finite_list.hs:42:33:
    --     Could not deduce (FinList x n xs)
    --       from the context (FinList x (Succ n1) (SuccList x xs),
    --                         Nat n1,
    --                         FinList x n1 xs)
    --       arising from a use of `toList' at finite_list.hs:42:33-41
    --     Possible fix:
    --       add (FinList x n xs) to the context of the instance declaration
    --     In the second argument of `(:)', namely `toList xs'
    -- toList (SuccList x xs) = x : toList xs

nil :: ZeroList x  -- a FinList x Zero
nil = ZeroList

-- todo: add a type class constraint "there is an n such that FinList x n xs"
cons :: x -> xs -> SuccList x xs
cons = SuccList

l1 = cons 3 . cons 2 . cons 1 $ nil

-- Does *NOT* typecheck, as required. The error is
-- finite_list.hs:66:7:
--     Occurs check: cannot construct the infinite type:
--       xs = SuccList t xs
--       Expected type: xs
--       Inferred type: SuccList t xs
--     In the expression: cons 1 lErr
--     In the definition of `lErr': lErr = cons 1 lErr
-- lErr = cons 1 lErr

In line 22: s/of length l/of length n/