Resolving dependencies... Starting applicative-extras-0.1.8 Starting call-stack-0.4.0 Starting clock-0.8.4 Building applicative-extras-0.1.8 Building call-stack-0.4.0 Building clock-0.8.4 Completed call-stack-0.4.0 Starting HUnit-1.6.2.0 Completed applicative-extras-0.1.8 Building HUnit-1.6.2.0 Completed clock-0.8.4 Starting extra-1.7.14 Building extra-1.7.14 Completed HUnit-1.6.2.0 Completed extra-1.7.14 Starting atp-haskell-1.14.2 Building atp-haskell-1.14.2 Failed to install atp-haskell-1.14.2 Build log ( /home/builder/.cabal/logs/ghc-9.6.3/atp-haskell-1.14.2-7D87sioQSAiIoS70WYZm1v.log ): cabal: Entering directory '/tmp/cabal-tmp-3959456/atp-haskell-1.14.2' Configuring atp-haskell-1.14.2... Preprocessing library for atp-haskell-1.14.2.. Building library for atp-haskell-1.14.2.. [ 1 of 25] Compiling Data.Logic.ATP.Lib ( src/Data/Logic/ATP/Lib.hs, dist/build/Data/Logic/ATP/Lib.o, dist/build/Data/Logic/ATP/Lib.dyn_o ) src/Data/Logic/ATP/Lib.hs:70:1: warning: [-Wunused-imports] The import of Data.Monoid is redundant except perhaps to import instances from Data.Monoid To import instances alone, use: import Data.Monoid() | 70 | import Data.Monoid ((<>)) | ^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/Lib.hs:94:3: warning: [-Wnoncanonical-monad-instances] Noncanonical return definition detected in the instance declaration for Monad Failing. return will eventually be removed in favour of pure Either remove definition for return (recommended) or define as return = pure See also: https://gitlab.haskell.org/ghc/ghc/-/wikis/proposal/monad-of-no-return | 94 | return = Success | ^^^^^^^^^^^^^^^^ [ 2 of 25] Compiling Data.Logic.ATP.Pretty ( src/Data/Logic/ATP/Pretty.hs, dist/build/Data/Logic/ATP/Pretty.o, dist/build/Data/Logic/ATP/Pretty.dyn_o ) src/Data/Logic/ATP/Pretty.hs:40:1: warning: [-Wunused-imports] The import of Data.Monoid is redundant except perhaps to import instances from Data.Monoid To import instances alone, use: import Data.Monoid() | 40 | import Data.Monoid ((<>)) | ^^^^^^^^^^^^^^^^^^^^^^^^^ [ 3 of 25] Compiling Data.Logic.ATP.Formulas ( src/Data/Logic/ATP/Formulas.hs, dist/build/Data/Logic/ATP/Formulas.o, dist/build/Data/Logic/ATP/Formulas.dyn_o ) [ 4 of 25] Compiling Data.Logic.ATP.Lit ( src/Data/Logic/ATP/Lit.hs, dist/build/Data/Logic/ATP/Lit.o, dist/build/Data/Logic/ATP/Lit.dyn_o ) src/Data/Logic/ATP/Lit.hs:39:1: warning: [-Wunused-imports] The import of Data.Monoid is redundant except perhaps to import instances from Data.Monoid To import instances alone, use: import Data.Monoid() | 39 | import Data.Monoid ((<>)) | ^^^^^^^^^^^^^^^^^^^^^^^^^ [ 5 of 25] Compiling Data.Logic.ATP.LitWrapper ( src/Data/Logic/ATP/LitWrapper.hs, dist/build/Data/Logic/ATP/LitWrapper.o, dist/build/Data/Logic/ATP/LitWrapper.dyn_o ) [ 6 of 25] Compiling Data.Logic.ATP.Prop ( src/Data/Logic/ATP/Prop.hs, dist/build/Data/Logic/ATP/Prop.o, dist/build/Data/Logic/ATP/Prop.dyn_o ) src/Data/Logic/ATP/Prop.hs:97:1: warning: [-Wunused-imports] The import of Data.Monoid is redundant except perhaps to import instances from Data.Monoid To import instances alone, use: import Data.Monoid() | 97 | import Data.Monoid ((<>)) | ^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/Prop.hs:499:7: warning: [-Wunused-local-binds] Defined but not used: byPrec | 499 | byPrec = groupBy ((==) `on` fst) . sortBy (compare `on` fst) $ binops | ^^^^^^ src/Data/Logic/ATP/Prop.hs:504:7: warning: [-Wunused-local-binds] Defined but not used: binops | 504 | binops = ands ++ ors ++ imps ++ iffs | ^^^^^^ src/Data/Logic/ATP/Prop.hs:515:7: warning: [-Wunused-local-binds] Defined but not used: preops | 515 | preops = nots | ^^^^^^ src/Data/Logic/ATP/Prop.hs:951:11: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [PFormula Prop] not matched: [] [_] [_, _] [_, _, _] ... | 951 | [p, q, r, s, t, u, v] = List.map (Atom . P) ["p", "q", "r", "s", "t", "u", "v"] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [ 7 of 25] Compiling Data.Logic.ATP.DefCNF ( src/Data/Logic/ATP/DefCNF.hs, dist/build/Data/Logic/ATP/DefCNF.o, dist/build/Data/Logic/ATP/DefCNF.dyn_o ) src/Data/Logic/ATP/DefCNF.hs:42:9: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [PFormula Prop] not matched: [] [_] [_, _] (_:_:_:_:_) | 42 | [p, q, r] = (List.map (atomic . P) ["p", "q", "r"]) in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [ 8 of 25] Compiling Data.Logic.ATP.PropExamples ( src/Data/Logic/ATP/PropExamples.hs, dist/build/Data/Logic/ATP/PropExamples.o, dist/build/Data/Logic/ATP/PropExamples.dyn_o ) src/Data/Logic/ATP/PropExamples.hs:166:20: error: [GHC-39999] " Could not deduce Show a arising from a superclass required to satisfy IsAtom (AtomOf formula), arising from a superclass required to satisfy IsFormula formula, arising from a superclass required to satisfy Data.Logic.ATP.Lit.IsLiteral formula, arising from a superclass required to satisfy IsPropositional formula, arising from a use of mk_knows from the context: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a) bound by the type signature for: mk_adder_test :: forall formula a. (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a) => a -> a -> formula at src/Data/Logic/ATP/PropExamples.hs:(162,1)-(163,34) Possible fix: add (Show a) to the context of the type signature for: mk_adder_test :: forall formula a. (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a) => a -> a -> formula " In the first argument of Prelude.map, namely mk_knows In the expression: Prelude.map mk_knows ["x", "y", "c", "s", ....] In a pattern binding: [x, y, c, s, c0, s0, c1, s1, c2, s2] = Prelude.map mk_knows ["x", "y", "c", ....] | 166 | List.map mk_knows ["x", "y", "c", "s", "c0", "s0", "c1", "s1", "c2", "s2"] in | ^^^^^^^^ [10 of 25] Compiling Data.Logic.ATP.Term ( src/Data/Logic/ATP/Term.hs, dist/build/Data/Logic/ATP/Term.o, dist/build/Data/Logic/ATP/Term.dyn_o ) src/Data/Logic/ATP/Term.hs:46:31: warning: [-Wunused-imports] The import of <> from module Data.Logic.ATP.Pretty is redundant | 46 | import Data.Logic.ATP.Pretty ((<>), Associativity(InfixN), Doc, HasFixity(associativity, precedence), Precedence, prettyShow, text) | ^^^^ [11 of 25] Compiling Data.Logic.ATP.Apply ( src/Data/Logic/ATP/Apply.hs, dist/build/Data/Logic/ATP/Apply.o, dist/build/Data/Logic/ATP/Apply.dyn_o ) src/Data/Logic/ATP/Apply.hs:36:41: warning: [-Wunused-imports] The import of <> from module Data.Logic.ATP.Pretty is redundant | 36 | import Data.Logic.ATP.Pretty as Pretty ((<>), Associativity(InfixN), Doc, HasFixity(associativity, precedence), pAppPrec, text) | ^^^^ src/Data/Logic/ATP/Apply.hs:64:39: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 64 | atomFuncs :: (HasApply atom, function ~ FunOf (TermOf atom)) => atom -> Set (function, Arity) | ^ src/Data/Logic/ATP/Apply.hs:69:20: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 69 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Apply.hs:70:20: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 70 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Apply.hs:71:24: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 71 | function ~ FunOf term) => | ^ src/Data/Logic/ATP/Apply.hs:78:36: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 78 | foldApply :: (JustApply atom, term ~ TermOf atom) => (PredOf atom -> [term] -> r) -> atom -> r | ^ src/Data/Logic/ATP/Apply.hs:82:19: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 82 | prettyApply :: (v ~ TVarOf term, IsPredicate predicate, IsTerm term) => predicate -> [term] -> Doc | ^ src/Data/Logic/ATP/Apply.hs:94:37: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 94 | zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1, | ^ src/Data/Logic/ATP/Apply.hs:94:63: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 94 | zipApplys :: (JustApply atom1, term ~ TermOf atom1, predicate ~ PredOf atom1, | ^ src/Data/Logic/ATP/Apply.hs:95:37: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 95 | JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) => | ^ src/Data/Logic/ATP/Apply.hs:95:63: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 95 | JustApply atom2, term ~ TermOf atom2, predicate ~ PredOf atom2) => | ^ src/Data/Logic/ATP/Apply.hs:115:54: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 115 | onformula :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom) => | ^ src/Data/Logic/ATP/Apply.hs:115:77: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 115 | onformula :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula, term ~ TermOf atom) => | ^ src/Data/Logic/ATP/Apply.hs:120:49: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 120 | pApp :: (IsFormula formula, HasApply atom, atom ~ AtomOf formula) => PredOf atom -> [TermOf atom] -> formula | ^ [12 of 25] Compiling Data.Logic.ATP.Quantified ( src/Data/Logic/ATP/Quantified.hs, dist/build/Data/Logic/ATP/Quantified.o, dist/build/Data/Logic/ATP/Quantified.dyn_o ) src/Data/Logic/ATP/Quantified.hs:38:6: warning: [-Wunused-imports] The import of <> from module Data.Logic.ATP.Pretty is redundant | 38 | ((<>), Associativity(InfixN, InfixR, InfixA), Doc, HasFixity(precedence, associativity), | ^^^^ src/Data/Logic/ATP/Quantified.hs:77:1: warning: [GHC-64088] [-Wforall-identifier] The use of  as an identifier will become an error in a future GHC release. Suggested fix: Consider using another name, such as forAll, for_all, or forall_. | 77 | () = for_all | ^^^ src/Data/Logic/ATP/Quantified.hs:107:56: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 107 | prettyQuantified :: forall fof v. (IsQuantified fof, v ~ VarOf fof) => | ^ src/Data/Logic/ATP/Quantified.hs:218:44: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 218 | instance (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Pretty (QFormula v atom) where | ^ src/Data/Logic/ATP/Quantified.hs:218:61: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 218 | instance (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Pretty (QFormula v atom) where | ^ src/Data/Logic/ATP/Quantified.hs:222:28: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 222 | instance (HasApply atom, v ~ TVarOf (TermOf atom)) => IsFormula (QFormula v atom) where | ^ src/Data/Logic/ATP/Quantified.hs:233:57: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 233 | instance (IsFormula (QFormula v atom), HasApply atom, v ~ TVarOf (TermOf atom)) => IsPropositional (QFormula v atom) where | ^ src/Data/Logic/ATP/Quantified.hs:271:28: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 271 | instance (HasApply atom, v ~ TVarOf (TermOf atom)) => IsLiteral (QFormula v atom) where | ^ [13 of 25] Compiling Data.Logic.ATP.Equate ( src/Data/Logic/ATP/Equate.hs, dist/build/Data/Logic/ATP/Equate.o, dist/build/Data/Logic/ATP/Equate.dyn_o ) src/Data/Logic/ATP/Equate.hs:35:41: warning: [-Wunused-imports] The import of <> from module Data.Logic.ATP.Pretty is redundant | 35 | import Data.Logic.ATP.Pretty as Pretty ((<>), Associativity(InfixN), atomPrec, Doc, eqPrec, HasFixity(associativity, precedence), pAppPrec, Precedence, text) | ^^^^ src/Data/Logic/ATP/Equate.hs:49:51: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 49 | (.=.) :: (IsFormula formula, HasEquate atom, atom ~ AtomOf formula) => TermOf atom -> TermOf atom -> formula | ^ src/Data/Logic/ATP/Equate.hs:54:63: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 54 | zipEquates :: (HasEquate atom1, HasEquate atom2, PredOf atom1 ~ PredOf atom2) => | ^ [14 of 25] Compiling Data.Logic.ATP.FOL ( src/Data/Logic/ATP/FOL.hs, dist/build/Data/Logic/ATP/FOL.o, dist/build/Data/Logic/ATP/FOL.dyn_o ) src/Data/Logic/ATP/FOL.hs:60:22: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 60 | VarOf formula ~ TVarOf (TermOf (AtomOf formula))) | ^ src/Data/Logic/ATP/FOL.hs:250:20: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 250 | term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) => | ^ src/Data/Logic/ATP/FOL.hs:250:37: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 250 | term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) => | ^ src/Data/Logic/ATP/FOL.hs:250:61: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 250 | term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) => | ^ src/Data/Logic/ATP/FOL.hs:250:85: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 250 | term ~ TermOf atom, v ~ TVarOf term, function ~ FunOf term, predicate ~ PredOf atom) => | ^ src/Data/Logic/ATP/FOL.hs:255:28: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 255 | termval :: (IsTerm term, v ~ TVarOf term, function ~ FunOf term) => Interp function predicate r -> Map v r -> term -> r | ^ src/Data/Logic/ATP/FOL.hs:255:52: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 255 | termval :: (IsTerm term, v ~ TVarOf term, function ~ FunOf term) => Interp function predicate r -> Map v r -> term -> r | ^ src/Data/Logic/ATP/FOL.hs:334:32: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 334 | fv :: (IsFirstOrder formula, v ~ VarOf formula) => formula -> Set v | ^ src/Data/Logic/ATP/FOL.hs:347:14: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 347 | atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/FOL.hs:347:37: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 347 | atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/FOL.hs:347:54: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 347 | atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/FOL.hs:352:42: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 352 | fva :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => atom -> Set v | ^ src/Data/Logic/ATP/FOL.hs:352:59: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 352 | fva :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => atom -> Set v | ^ src/Data/Logic/ATP/FOL.hs:356:24: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 356 | fvt :: (IsTerm term, v ~ TVarOf term) => term -> Set v | ^ src/Data/Logic/ATP/FOL.hs:377:38: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 377 | subst :: (IsFirstOrder formula, term ~ TermOf (AtomOf formula), v ~ VarOf formula) => Map v term -> formula -> formula | ^ src/Data/Logic/ATP/FOL.hs:377:67: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 377 | subst :: (IsFirstOrder formula, term ~ TermOf (AtomOf formula), v ~ VarOf formula) => Map v term -> formula -> formula | ^ src/Data/Logic/ATP/FOL.hs:393:27: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 393 | tsubst :: (IsTerm term, v ~ TVarOf term) => Map v term -> term -> term | ^ src/Data/Logic/ATP/FOL.hs:401:17: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 401 | atom ~ AtomOf lit, | ^ src/Data/Logic/ATP/FOL.hs:402:17: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 402 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/FOL.hs:403:14: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 403 | v ~ TVarOf term) => | ^ src/Data/Logic/ATP/FOL.hs:412:45: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 412 | asubst :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> atom -> atom | ^ src/Data/Logic/ATP/FOL.hs:412:62: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 412 | asubst :: (HasApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => Map v term -> atom -> atom | ^ src/Data/Logic/ATP/FOL.hs:416:36: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 416 | substq :: (IsFirstOrder formula, v ~ VarOf formula, term ~ TermOf (AtomOf formula)) => | ^ src/Data/Logic/ATP/FOL.hs:416:58: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 416 | substq :: (IsFirstOrder formula, v ~ VarOf formula, term ~ TermOf (AtomOf formula)) => | ^ [15 of 25] Compiling Data.Logic.ATP.Skolem ( src/Data/Logic/ATP/Skolem.hs, dist/build/Data/Logic/ATP/Skolem.o, dist/build/Data/Logic/ATP/Skolem.dyn_o ) src/Data/Logic/ATP/Skolem.hs:62:1: warning: [-Wunused-imports] The import of Data.Monoid is redundant except perhaps to import instances from Data.Monoid To import instances alone, use: import Data.Monoid() | 62 | import Data.Monoid ((<>)) | ^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/Skolem.hs:236:35: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 236 | pullq :: (IsFirstOrder formula, v ~ VarOf formula) => | ^ src/Data/Logic/ATP/Skolem.hs:271:18: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 271 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Skolem.hs:272:18: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 272 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Skolem.hs:273:22: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 273 | function ~ FunOf term {-, | ^ src/Data/Logic/ATP/Skolem.hs:288:17: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 288 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Skolem.hs:289:17: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 289 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Skolem.hs:290:21: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 290 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:291:26: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 291 | VarOf formula ~ SVarOf function {-, | ^ src/Data/Logic/ATP/Skolem.hs:310:46: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 310 | newSkolem :: (Monad m, HasSkolem function, v ~ SVarOf function) => v -> SkolemT m function function | ^ src/Data/Logic/ATP/Skolem.hs:317:18: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 317 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Skolem.hs:318:18: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 318 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Skolem.hs:319:22: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 319 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:320:27: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 320 | VarOf formula ~ SVarOf function) => | ^ src/Data/Logic/ATP/Skolem.hs:329:21: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 329 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Skolem.hs:330:21: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 330 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Skolem.hs:331:25: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 331 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:332:30: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 332 | VarOf formula ~ SVarOf function) => | ^ src/Data/Logic/ATP/Skolem.hs:352:20: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 352 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Skolem.hs:353:20: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 353 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Skolem.hs:354:24: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 354 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:355:29: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 355 | VarOf formula ~ SVarOf function) => | ^ src/Data/Logic/ATP/Skolem.hs:374:28: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a lambda abstraction: Patterns of type Function not matched: Skolem _ _ | 374 | pPrint = prettySkolem (\(Fn s) -> text s) | ^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/Skolem.hs:417:19: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 417 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:417:38: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 417 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:417:62: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 417 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:418:16: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 418 | v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Skolem.hs:418:31: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 418 | v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Skolem.hs:441:19: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 441 | simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:441:38: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 441 | simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:441:63: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 441 | simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:441:80: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 441 | simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:441:95: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 441 | simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:441:119: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 441 | simpcnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:451:19: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 451 | purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:451:38: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 451 | purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:451:63: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 451 | purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:451:80: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 451 | purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:451:95: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 451 | purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Skolem.hs:451:119: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 451 | purecnf' :: (atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ [16 of 25] Compiling Data.Logic.ATP.Parser ( src/Data/Logic/ATP/Parser.hs, dist/build/Data/Logic/ATP/Parser.o, dist/build/Data/Logic/ATP/Parser.dyn_o ) src/Data/Logic/ATP/Parser.hs:28:1: warning: [GHC-90177] [-Worphans] Orphan instance: instance Pretty ParseError Suggested fix: Move the instance declaration to the module of the class or of the type, or wrap the type with a newtype and declare the instance on the new type. | 28 | instance Pretty ParseError where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... src/Data/Logic/ATP/Parser.hs:31:1: warning: [GHC-90177] [-Worphans] Orphan instance: instance Pretty Message Suggested fix: Move the instance declaration to the module of the class or of the type, or wrap the type with a newtype and declare the instance on the new type. | 31 | instance Pretty Message where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... [17 of 25] Compiling Data.Logic.ATP.ParserTests ( src/Data/Logic/ATP/ParserTests.hs, dist/build/Data/Logic/ATP/ParserTests.o, dist/build/Data/Logic/ATP/ParserTests.dyn_o ) [18 of 25] Compiling Data.Logic.ATP.Prolog ( src/Data/Logic/ATP/Prolog.hs, dist/build/Data/Logic/ATP/Prolog.o, dist/build/Data/Logic/ATP/Prolog.dyn_o ) src/Data/Logic/ATP/Prolog.hs:30:21: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 30 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Prolog.hs:30:40: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 30 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Prolog.hs:30:57: warning: [GHC-58520] [-Wtype-equality-requires-operators] The use of ~ without TypeOperators will become an error in a future GHC release. Suggested fix: Perhaps you intended to use TypeOperators | 30 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ [20 of 25] Compiling Data.Logic.ATP.Unif ( src/Data/Logic/ATP/Unif.hs, dist/build/Data/Logic/ATP/Unif.o, dist/build/Data/Logic/ATP/Unif.dyn_o ) src/Data/Logic/ATP/Unif.hs:81:16: error: [GHC-39999] " Could not deduce MonadFail m arising from a use of fail from the context: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) bound by the type signature for: unify_term_pair :: forall term v f (m :: * -> *). (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => term -> term -> StateT (Map v term) m () at src/Data/Logic/ATP/Unif.hs:(66,1)-(68,59) Possible fix: add (MonadFail m) to the context of the type signature for: unify_term_pair :: forall term v f (m :: * -> *). (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => term -> term -> StateT (Map v term) m () " In the expression: fail "impossible unification" In the expression: if f == g && length fargs == length gargs then mapM_ (uncurry unify_term_pair) (zip fargs gargs) else fail "impossible unification" In an equation for fn: fn f fargs g gargs = if f == g && length fargs == length gargs then mapM_ (uncurry unify_term_pair) (zip fargs gargs) else fail "impossible unification" | 81 | else fail "impossible unification" | ^^^^ src/Data/Logic/ATP/Unif.hs:92:65: error: [GHC-39999] " Could not deduce MonadFail m arising from a use of fail from the context: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) bound by the type signature for: istriv :: forall term v f (m :: * -> *). (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => v -> term -> StateT (Map v term) m Bool at src/Data/Logic/ATP/Unif.hs:(83,1)-(84,49) Possible fix: add (MonadFail m) to the context of the type signature for: istriv :: forall term v f (m :: * -> *). (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => v -> term -> StateT (Map v term) m Bool " In the second argument of bool, namely (fail "cyclic") In the first argument of (.), namely bool (return False) (fail "cyclic") In the second argument of (>>=), namely bool (return False) (fail "cyclic") . or | 92 | fn _ args = mapM (istriv x) args >>= bool (return False) (fail "cyclic") . or | ^^^^ src/Data/Logic/ATP/Unif.hs:122:16: error: [GHC-39999] " Could not deduce MonadFail m arising from a use of fail from the context: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) bound by the type signature for: unify_literals :: forall lit1 lit2 atom1 atom2 v term (m :: * -> *). (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) m () at src/Data/Logic/ATP/Unif.hs:(116,1)-(120,58) Possible fix: add (MonadFail m) to the context of the type signature for: unify_literals :: forall lit1 lit2 atom1 atom2 v term (m :: * -> *). (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) m () " In the first argument of fromMaybe, namely (fail "Can't unify literals") In the expression: fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2) In an equation for unify_literals: unify_literals f1 f2 = fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2) where ho _ _ = Nothing ne p q = Just $ unify_literals p q tf p q = if p == q then Just (unify_terms ([] :: [(term, term)])) else Nothing at a1 a2 = Just (unify' (a1, a2)) | 122 | fromMaybe (fail "Can't unify literals") (zipLiterals' ho ne tf at f1 f2) | ^^^^ src/Data/Logic/ATP/Unif.hs:135:12: error: [GHC-39999] " Could not deduce MonadFail m arising from a use of fail from the context: (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) bound by the type signature for: unify_atoms :: forall atom1 term atom2 v (m :: * -> *). (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) => (atom1, atom2) -> StateT (Map v term) m () at src/Data/Logic/ATP/Unif.hs:(130,1)-(133,57) Possible fix: add (MonadFail m) to the context of the type signature for: unify_atoms :: forall atom1 term atom2 v (m :: * -> *). (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) => (atom1, atom2) -> StateT (Map v term) m () " In the first argument of maybe, namely (fail "unify_atoms") In the expression: maybe (fail "unify_atoms") id (zipApplys (\ _ tpairs -> Just (unify_terms tpairs)) a1 a2) In an equation for unify_atoms: unify_atoms (a1, a2) = maybe (fail "unify_atoms") id (zipApplys (\ _ tpairs -> Just (unify_terms tpairs)) a1 a2) | 135 | maybe (fail "unify_atoms") id (zipApplys (\_ tpairs -> Just (unify_terms tpairs)) a1 a2) | ^^^^ src/Data/Logic/ATP/Unif.hs:142:12: error: [GHC-39999] " Could not deduce MonadFail m arising from a use of fail from the context: (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) bound by the type signature for: unify_atoms_eq :: forall atom1 term atom2 v (m :: * -> *). (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) => atom1 -> atom2 -> StateT (Map v term) m () at src/Data/Logic/ATP/Unif.hs:(137,1)-(140,60) Possible fix: add (MonadFail m) to the context of the type signature for: unify_atoms_eq :: forall atom1 term atom2 v (m :: * -> *). (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) => atom1 -> atom2 -> StateT (Map v term) m () " In the first argument of maybe, namely (fail "unify_atoms") In the expression: maybe (fail "unify_atoms") id (zipEquates (\ l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)])) (\ _ tpairs -> Just (unify_terms tpairs)) a1 a2) In an equation for unify_atoms_eq: unify_atoms_eq a1 a2 = maybe (fail "unify_atoms") id (zipEquates (\ l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)])) (\ _ tpairs -> Just (unify_terms tpairs)) a1 a2) | 142 | maybe (fail "unify_atoms") id (zipEquates (\l1 r1 l2 r2 -> Just (unify_terms [(l1, l2), (r1, r2)])) | ^^^^ cabal: Leaving directory '/tmp/cabal-tmp-3959456/atp-haskell-1.14.2' Error: cabal: Some packages failed to install: atp-haskell-1.14.2-7D87sioQSAiIoS70WYZm1v failed during the building phase. The exception was: ExitFailure 1