これはもうだめです

{-# 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 | 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 {- bはSTV上仕方がない。b = a'-} )) (arg :: Exp c) :: Exp (App a')) (ELam k :: Kont1 (Exp (App a')) (Exp b')) = v
        where
          k' :: Exp a' -> Exp b'
          k' = k

          k1_body :: (CPS (Exp c) d,Kont1 (Exp c) d ~ Exp (arg -> b')) => Exp (arg -> b) -> Kont2 (Exp c) d -- Exp b'
          k1_body = (\(f' :: Exp (arg -> b)) -> case f' of
                                                  ELam f'' -> k2_body f'''
                                                      where
                                                        f''' :: Exp arg -> Exp a'
                                                        f''' = f''
                    )

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

          v :: (CPS (Exp (arg -> a')) cps_b,CPS (Exp c) d,Kont1 (Exp c) d ~ Exp (arg -> b'),Kont2 (Exp c) d ~ Exp z,Kont1 (Exp (arg -> a')) cps_b ~ Exp ((arg -> a') -> z)) => Kont2 (Exp (arg -> a')) cps_b
          v = cps f k1

はてなに張ると、突き破って横に伸びちゃうのをなんとかしたいです。

スーパーpre記法使う時に、スクロールバーさんが出てくれれば良いのかな？

む、しかしGoogle Chorme使ってると自動で改行されてる。

Firefoxだと突き破る。(スクロールするようにした)