Just for those who failed to build this on recent GHC. The fix was suggested by AI. I've applied it and it seems to work:
diff --git a/source/Main.hs b/source/Main.hs
index 0feef28..0416207 100644
--- a/source/Main.hs
+++ b/source/Main.hs
@@ -1,5 +1,6 @@
module Main where
+import Control.Monad
import Control.Monad.Trans
import Control.Monad.State
import Control.Exception
diff --git a/source/Stlc/Gentzen.hs b/source/Stlc/Gentzen.hs
index ae5c7e5..3d82adb 100644
--- a/source/Stlc/Gentzen.hs
+++ b/source/Stlc/Gentzen.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
module Stlc.Gentzen
( gentzendiagram
, showProofTree
@@ -11,9 +13,12 @@ import NamedLambda
import Data.Bifunctor
import qualified Data.Map as Map
-
data ProofTree a l = Inference a | Deduction a l [ProofTree a l]
+instance Functor (ProofTree a) where
+ fmap _ (Inference a) = Inference a
+ fmap g (Deduction a l ps) = Deduction a (g l) (fmap (fmap g) ps)
+
instance Bifunctor ProofTree where
bimap f _ (Inference a) = Inference (f a)
bimap f g (Deduction a l ps) = Deduction (f a) (g l) (map (bimap f g) ps)
Just for those who failed to build this on recent GHC. The fix was suggested by AI. I've applied it and it seems to work: