Attempting to fold functions results in incorrect type

Question

I have the following source code:

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

class Digit d  

data Zero
data One
data Two
data Three
data Four
data Five
data Six

instance Digit Zero
instance Digit One
instance Digit Two
instance Digit Three
instance Digit Four
instance Digit Five
instance Digit Six


class Sum a b c | a b -> c, a c -> b, c b -> a 

incSize :: (Digit z, Digit x, Sum x One z) => x -> z --written by me
incSize _ = undefined

intToSize :: (Digit x, Num a, Sum x One x) => a -> x -> t --inferred by GHCI
intToSize n v = intToSize (n-1) (incSize v)

intToSize' :: (Digit b, Sum b One b) => Int -> t -> b -> b --inferred by GHCI
intToSize' n v = foldr (.) id (replicate n incSize)

intToSize'' :: (Digit a, Digit b1, Digit b, Digit c, Sum a One b1, Sum b1 One b, Sum b One c) => a -> c --inferred by GHCI
intToSize'' = incSize . incSize . incSize 

Essentially the goal is to take an Int and convert it to one of the datatypes defined above. The function incSize works correctly; it increments the size by one. The function inToSize'' also works; it will increment the given number by 3. However, both intToSize and intToSize' do not work; GHCI infers their types as stated above (and obviously, a+1 =/= a). I am not sure why manually writing the composition works correctly, while anything else will fail (the functions I identified as not working compile, but will always give an error whenever they are used.) The use should look something like this:

> :t intToSize'' (undefined :: Zero)
> intToSize'' (undefined :: Zero) :: Three

However the eventual goal is to write a function which takes a list, and gives a datatype which encodes the length of the list in its type (essentially a vector):

data Vect s v = Vect v
instance forall s v . Show (Vect s v) where
     --toInt is a function which takes a type number and returns its data level value
     show (Vect v) = "Vect " ++ (show . toInt) (undefined :: s) ++ show v  

> let l = [1,2,3,4,5]
> vector l 
> Vect 5 [1,2,3,4,5] 

You may have noticed that some code is missing; it is rather boring to look at so instead I include it at the bottom.

instance Sum  Zero  Zero  Zero
instance Sum  Zero  One   One
instance Sum  Zero  Two   Two
instance Sum  Zero  Three Three
instance Sum  Zero  Four  Four
instance Sum  Zero  Five  Five
instance Sum  Zero  Six   Six
instance Sum  One   Zero  One
instance Sum  One   One   Two
instance Sum  One   Two   Three
instance Sum  One   Three Four
instance Sum  One   Four  Five
instance Sum  One   Five  Six
instance Sum  Two   Zero  Two
instance Sum  Two   One   Three
instance Sum  Two   Two   Four
instance Sum  Two   Three Five
instance Sum  Two   Four  Six
instance Sum  Three Zero  Three
instance Sum  Three One   Four
instance Sum  Three Two   Five
instance Sum  Three Three Six
instance Sum  Four  Zero  Four
instance Sum  Four  One   Five
instance Sum  Four  Two   Six
instance Sum  Five  Zero  Five
instance Sum  Five  One   Six
instance Sum  Six   Zero  Six

Answer 1

The problem is that you want to pass a polymorphically typed function to foldr. Note that while foldr itself has a polymorphic type, it expects its argument to have a monomorphic type.

For functions to take polymorphic functions as arguments (and in fact use those argument functions polymorphically), you need so-called higher-rank polymorphism. The good news is that GHC supports higher-ranked polymorphic types (use the RankNTypes extension); the bad news is that type inference is undecidable for them. Hence, you will need explicit type signatures in your code in order to convince the type checker that your code is correct. Then the question of course arises what would be the type signature that you need for your function intToSize'? And then there's more bad news: as the type of your function would need to depend on the integer value that you provide, it cannot straightforwardly be expressed in Haskell.

---

That said, with GADTs and type families, you can come a long way toward what you seem to be after:

{-# LANGUAGE GADTs        #-}
{-# LANGUAGE TypeFamilies #-}

data Zero
data Succ n

type One   = Succ Zero
type Two   = Succ One
type Three = Succ Two

data Nat :: * -> * where
  Zero :: Nat Zero
  Succ :: Nat n -> Nat (Succ n)

zero  = Zero
one   = Succ zero
two   = Succ one
three = Succ two

type family Sum m n          :: *
type instance Sum Zero n     =  n
type instance Sum (Succ m) n =  Succ (Sum m n)

add            :: Nat m -> Nat n -> Nat (Sum m n)
add Zero n     =  n
add (Succ m) n =  Succ (add m n)

incSize :: Nat m -> Nat (Sum One m)
incSize = add one  -- or just: Succ 

For example:

> :t incSize two
incSize two :: Nat (Sum One (Succ (Succ Zero)))

and note that Sum One (Succ (Succ Zero))) is the same as Three.

---

As for your bigger goal, writing "a function which takes a list, and gives a datatype which encodes the length of the list in its type": you simply cannot do that. You cannot have a function with a static (i.e., compile-time) type depending on a value (the length of the list) that possibly is not known until runtime.

The closest you can get is by wrapping your vector type in an existential wrapper:

{-# LANGUAGE DataKinds    #-}
{-# LANGUAGE GADTs        #-}
{-# LANGUAGE TypeFamilies #-}

data Nat = Zero | Succ Nat

data Vec :: Nat -> * -> * where
  Nil  :: Vec Zero a
  Cons :: a -> Vec n a -> Vec (Succ n) a

data EVec :: * -> * where
  Exists :: Vec n a -> EVec a

enil :: EVec a
enil =  Exists Nil

econs               :: a -> EVec a -> EVec a
econs x (Exists xs) =  Exists (Cons x xs)

vector :: [a] -> EVec a
vector =  foldr econs enil

Now, whenever you have a value of type EVec, you can open it and subject the contained vector to all kinds of processing with the increased type safety that is enabled by the encoding of its length in its type.