BinaryWrite по сравнению с WriteFile

Если GHC может сделать вывод (через FunDep), что c должно быть Term Int для = undefined

Не может. Если вы попытаетесь undefined :: Term Int, вы получите ту же ошибку переменной жесткого типа. Если вы используете типизированное отверстие = _undefined, вы увидите, что оно выводит undefined :: c. Я не знаю почему, но функциональная зависимость, кажется, используется только при применении eval к Lit, а не при его определении.

Как насчет этого?

class IsTerm a where
  type TermType a :: *
instance IsTerm Lit where
  type TermType Lit = Int
instance IsTerm a => IsTerm (Inc a) where
  type TermType (Inc a) = TermType a

class IsTerm a => Eval a   
  where eval :: a -> Term (TermType a) 

instance Eval Lit  where    
         eval (Lit i) = ToTerm i

-- needs UndecidableInstances
instance (Eval a, Num (TermType a)) => Eval (Inc a)  where    
         eval (Inc i) = ToTerm (fromTerm (eval i) + 1)