項が複製される場所を減らした。そのかわり気持ち悪い関数が発生した。これどうにもならんもんなん？

result

*Main> r
TArrow TBool TBool
TArrow (TArrow TBool TBool) (TArrow TBool TBool)
(\a -> (\b -> a b)) (\a -> if a then False else True) True
(\a -> (\b -> if b then False else True) a) True
(\a -> if a then False else True) True
if True then False else True
False

STLC.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
-- {-# LANGUAGE FlexibleInstances #-}
-- {-# LANGUAGE ImpredicativeTypes #-}

import Control.Monad.Reader

data Typ where
  TBool  :: Typ
  TArrow :: Typ -> Typ -> Typ
  deriving (Show, Eq)

data Val v where
  VBool :: Bool -> Val v
  VAbs :: Typ -> (v -> TermP v) -> Val v

data TermP v where
  TmVal :: Val v -> TermP v
  TmVar :: v -> TermP v
  TmApp :: TermP v -> TermP v -> TermP v
  TmIf  :: TermP v -> TermP v -> TermP v -> TermP v

type Term = forall a. TermP a

data TermD where
  TmValD :: (forall a. Val a) -> TermD
  TmVarD :: (forall a. a) -> TermD
  TmAppD :: Term -> Term -> TermD
  TmIfD  :: Term -> Term -> Term -> TermD

caseTerm :: Term -> TermD
caseTerm tm = case tm of
  TmVal _ -> TmValD (val tm)
  TmVar _ -> TmVarD (var tm)
  TmApp _ _ -> TmAppD (app1 tm) (app2 tm)
  TmIf _ _ _ -> TmIfD (if1 tm) (if2 tm) (if3 tm)
  where
    val  :: Term -> Val b
    var  :: Term -> b
    app1 :: Term -> Term
    app2 :: Term -> Term
    if1  :: Term -> Term
    if2  :: Term -> Term
    if3  :: Term -> Term
    val (TmVal v) = v
    val _ = undefined
    var (TmVar v) = v
    var _ = undefined
    app1 (TmApp t _) = t
    app1 _ = undefined
    app2 (TmApp _ t) = t
    app2 _ = undefined
    if1 (TmIf t _ _) = t
    if1 _ = undefined
    if2 (TmIf _ t _) = t
    if2 _ = undefined
    if3 (TmIf _ _ t) = t
    if3 _ = undefined

joinTerm :: TermP (TermP v) -> TermP v
joinTerm (TmVal (VBool v)) = TmVal (VBool v)
joinTerm (TmVal (VAbs ty f)) = TmVal (VAbs ty $ joinTerm . f . TmVar)
joinTerm (TmVar t) = t
joinTerm (TmApp t1 t2) = TmApp (joinTerm t1) (joinTerm t2)
joinTerm (TmIf t1 t2 t3) = TmIf (joinTerm t1) (joinTerm t2) (joinTerm t3)

isval :: Term -> Bool
isval (TmVal _) = True
isval _ = False

eval1 :: Term -> Term
eval1 tm = case caseTerm tm of
  TmVarD v -> v
  TmAppD (TmVal v1) t2@(TmVal _) ->
    case v1 of
      VAbs _ f -> joinTerm $ f t2
      _ -> error "Not applicative"
  TmAppD t1@(TmVal _) t2 -> TmApp t1 (eval1 t2)
  TmAppD t1 t2 -> TmApp (eval1 t1) t2
  TmIfD (TmVal (VBool True))  t2 _ -> t2
  TmIfD (TmVal (VBool False)) _ t3 -> t3
  TmIfD (TmVal _) _ _ -> error "Not bool"
  TmIfD t1 t2 t3 -> TmIf (eval1 t1) t2 t3
  _ -> error "No rule applies"

showsTerm :: TermP Char -> ShowS
showsTerm tm = runReader (showR tm) 'a'
  where
    showR :: TermP Char -> Reader Char ShowS
    showR (TmVal (VBool True)) = return ("True"++)
    showR (TmVal (VBool False)) = return ("False"++)
    showR (TmVal (VAbs _ f)) =
      do i <- ask
         s <- local succ $ showR (f i)
         return $ ("(\\"++) . (i:) . (" -> "++) . s . (")"++)
    showR (TmVar i) = return $ (i:)
    showR (TmApp t1 t2) = do
      s1 <- showR t1
      s2 <- showR t2
      return $ s1 . (" "++) . s2
    showR (TmIf t1 t2 t3) = do
      s1 <- showR t1
      s2 <- showR t2
      s3 <- showR t3
      return $ ("if "++) . s1 . (" then "++) . s2 . (" else "++) . s3

instance (a ~ Char) => Show (TermP a) where
  show t = showsTerm t ""

typeof :: Term -> Typ
typeof tm = go tm
  where
    err = error "type check failed"
    go :: TermP Typ -> Typ
    go t = case t of
      TmVal (VBool _) -> TBool
      TmVal (VAbs ty f) -> TArrow ty (go (f ty))
      TmVar v -> v
      TmApp t1 t2 ->
        case go t1 of
          TArrow ty1 ty2 | ty1 == go t2 -> ty2
          _ -> err
      TmIf t1 t2 t3 ->
        case go t1 of
          TBool | ty2 == ty3 -> ty2
          _ -> err
        where
          ty2 = go t2
          ty3 = go t3

termNot = TmVal $ VAbs TBool $ \x -> TmIf (TmVar x) (TmVal $ VBool False) (TmVal $ VBool True)
testFun = TmVal (VAbs (TArrow TBool TBool) $ \x -> TmVal (VAbs TBool $ \y -> TmApp (TmVar x) (TmVar y)) )
test v = TmApp (TmApp testFun termNot) (TmVal $ VBool v)

r = do print (typeof termNot)
       print (typeof testFun)
       go (test True)
  where
    go :: Term -> IO ()
    go t = do
      print t
      unless (isval t) (go (eval1 t))