実装したい(2)

GHCのバージョンは6.10.4です。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}

data COP a b
data App b

class TyEq a b | a -> b where
    f :: a -> b
    f v = undefined
instance TyEq Int Int
instance TyEq (App b) b
instance TyEq (COP a b) a
instance (TyEqProxy a a') => TyEq a a'

s1 :: Int
s1 = undefined
s2 :: App a
s2 = undefined
s3 :: COP a b
s3 = undefined
s4 :: a 
s4 = undefined

class TyEqProxy a b | a -> b
instance TyEqProxy a a

data Exp t where
    EInt :: Int -> Exp Int
    ELam :: (Exp a -> Exp b) -> Exp (a -> b)
    EApp :: (TyEq t t',t' ~ a) => Exp (a -> b) -> Exp t -> Exp (App b)
    Cop :: (TyEq c c',c' ~ b) => Exp ((a -> b) -> c) -> Exp (COP a b)

e1 :: Exp Int
e1 = EInt 1

e2 :: Exp (Int -> Int)
e2 = ELam (\(EInt x) -> EInt (x + 1))

e3 :: Exp (App Int)
e3 = EApp e2 e1

aux_e4 :: Exp (COP Int b)
aux_e4 = Cop (ELam (\k -> EApp k (EInt 2)))

e4 :: Exp (App Int)
e4 = EApp e2 aux_e4

exit :: Exp (a -> b)
exit = ELam exit'
    where
      exit' :: Exp a -> Exp b
      exit' v = error "exit"

class CPS cps_a cps_b where
    type Kont1 cps_a cps_b
    type Kont2 cps_a cps_b
    cps :: cps_a -> Kont1 cps_a cps_b -> Kont2 cps_a cps_b

instance CPS (Exp (App a')) (Exp b') where
    type Kont1 (Exp (App a')) (Exp b') = Exp (a' -> b')
    type Kont2 (Exp (App a')) (Exp b') = Exp b'
    cps (EApp (f :: Exp (arg -> b)) (arg :: Exp c) :: Exp (App a')) (ELam k) = undefined
        where
          k' :: Exp a' -> Exp b'
          k' = k

{-
          k1_body :: Exp (arg -> b) -> Exp b'
          k1_body = (\(f' :: Exp (arg -> b)) -> case f' of
                                                  ELam f'' -> k2_body f''
                    )
-}

          -- k2_body :: (Exp arg -> Exp b) -> Exp b'
          k2_body :: (CPS (Exp c) b,Kont1 (Exp c) b ~ Exp (a -> b')) => (Exp a -> Exp a') -> Kont2 (Exp c) b
          k2_body (f'' :: Exp a -> Exp a') = cps
                                             (arg :: Exp c)
                                             (ELam
                                              (\(arg' :: Exp a) ->
                                                   ((k'
                                                     ((f'' arg') :: Exp a')) :: Exp b'
                                                   )
                                              )
                                              :: Exp (a -> b'))

cont4.hs:89:45:
    Could not deduce (CPS (Exp t) cps_b)
      from the context (Kont1 (Exp t) b ~ Exp (a2 -> b'),
                        CPS (Exp t) cps_b1,
                        CPS (Exp t) b)
      arising from a use of `cps' at cont4.hs:(89,45)-(97,62)
    Possible fix:
      add (CPS (Exp t) cps_b) to the context of
        the type signature for `k2_body'
      or add an instance declaration for (CPS (Exp t) cps_b)

その他...

と言われるが、cps_bってどこから引っ張って来たら良いんだろう。

あともう兎に角前に進もうって感じで書いているので、相当メチャクチャになってる...

ただ、ghciでこいつを推論させる事自体は出来ているらしくて・・・ううーん・・・。
ghci -ddump-tc で吐かせてもrenameされちゃってて良く分からない(なので、型をそのままコピペしても駄目)

ddump-tcに従って見ると

          k2_body :: forall a cps_b.(Exp (a -> b') ~ Kont1 (Exp c) cps_b,CPS (Exp c) cps_b) =>
                              (Exp a -> Exp a') -> Kont2 (Exp c) cps_b
          k2_body f'' = cps
                        (arg :: Exp c)
                        (ELam
                         (\arg' ->
                              (k'
                                (f'' arg')
                              )
                         )
                        )

これでいけるはずだけれども、駄目と言われてしまう。うーん...??

同様の問題(なのか、それとも単に私が間違ってる気もするのですが)が発生するもっと小さいコードを作ってみようか。