haskell - 関数を折りたたもうとすると、型が正しくない

Question

次のソースコードがあります。

{-# 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 

基本的に、目標は を取得して、Int上で定義したデータ型のいずれかに変換することです。関数incSizeは正しく動作します。サイズを 1 ずつ増やします。関数inToSize''も機能します。指定された数値を 3 ずつ増やします。ただし、 と の両方は機能intToSizeしintToSize'ません。GHCI は上記のようにそれらの型を推測します (そして明らかに a+1 =/= a)。構成を手動で書くと正しく機能する理由はわかりませんが、他のものは失敗します (コンパイルが機能していないと特定した関数は、使用されるたびに常にエラーになります)。使用方法は次のようになります。

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

ただし、最終的な目標は、リストを受け取り、リストの長さをその型 (基本的にはベクトル) にエンコードするデータ型を与える関数を作成することです。

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] 

一部のコードが欠落していることにお気づきかもしれません。見るのはかなり退屈なので、代わりに一番下に含めます。

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