Resolving dependencies... Build profile: -w ghc-9.6.3 -O0 In order, the following will be built (use -v for more details): - applicative-extras-0.1.8 (lib:applicative-extras) (requires build) - atp-haskell-1.14.3 (first run) Starting applicative-extras-0.1.8 (all, legacy fallback) Building applicative-extras-0.1.8 (all, legacy fallback) Installing applicative-extras-0.1.8 (all, legacy fallback) Completed applicative-extras-0.1.8 (all, legacy fallback) Configuring atp-haskell-1.14.3... Preprocessing library for atp-haskell-1.14.3.. Building library for atp-haskell-1.14.3.. [ 1 of 25] Compiling Data.Logic.ATP.Lib ( src/Data/Logic/ATP/Lib.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Lib.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Pretty.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Formulas.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Formulas.dyn_o ) [ 4 of 25] Compiling Data.Logic.ATP.Lit ( src/Data/Logic/ATP/Lit.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Lit.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/LitWrapper.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/LitWrapper.dyn_o ) [ 6 of 25] Compiling Data.Logic.ATP.Prop ( src/Data/Logic/ATP/Prop.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Prop.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/DefCNF.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/PropExamples.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/PropExamples.dyn_o ) src/Data/Logic/ATP/PropExamples.hs:33: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 | 33 | ramsey :: (IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) => | ^ src/Data/Logic/ATP/PropExamples.hs:39:18: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [a] not matched: [] [_] (_:_:_:_) | 39 | let e xs = let [a, b] = Set.toAscList xs in atomic (K "p" a (Just b)) in | ^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:66:1: warning: [-Wunused-top-binds] Defined but not used: halfcarry | 66 | halfcarry x y = x .&. y | ^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:69:1: warning: [-Wunused-top-binds] Defined but not used: ha | 69 | ha x y s c = (s .<=>. halfsum x y) .&. (c .<=>. halfcarry x y) | ^^ src/Data/Logic/ATP/PropExamples.hs:96: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 | 96 | mk_knows :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> formula | ^ src/Data/Logic/ATP/PropExamples.hs:98:55: 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 | 98 | mk_knows2 :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> a -> formula | ^ src/Data/Logic/ATP/PropExamples.hs:103:9: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [Integer -> PFormula (Knows Integer)] not matched: [] [_] [_, _] [_, _, _] ... | 103 | let [x, y, out, c] = List.map mk_knows ["X", "Y", "OUT", "C"] :: [Integer -> PFormula (Knows Integer)] in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:129:1: warning: [-Wunused-top-binds] Defined but not used: ripplecarry1 | 129 | ripplecarry1 x y c out n = | ^^^^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:134:1: warning: [-Wunused-top-binds] Defined but not used: mux | 134 | mux sel in0 in1 = (((.~.) sel) .&. in0) .|. (sel .&. in1) | ^^^ src/Data/Logic/ATP/PropExamples.hs:137:1: warning: [-Wunused-top-binds] Defined but not used: offset | 137 | offset n x i = x (n + i) | ^^^^^^ src/Data/Logic/ATP/PropExamples.hs:149:1: warning: [-Wunused-top-binds] Defined but not used: carryselect | 149 | carryselect x y c0 c1 s0 s1 c s n k = | ^^^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:162:72: 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 | 162 | mk_adder_test :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a, Show a) => | ^ src/Data/Logic/ATP/PropExamples.hs:164:1: warning: [-Wunused-top-binds] Defined but not used: mk_adder_test | 164 | mk_adder_test n k = | ^^^^^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:165:7: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [a -> formula] not matched: [] [_] [_, _] [_, _, _] ... | 165 | let [x, y, c, s, c0, s0, c1, s1, c2, s2] = | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... src/Data/Logic/ATP/PropExamples.hs:226:64: 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 | 226 | prime :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows Integer) => Integer -> formula | ^ src/Data/Logic/ATP/PropExamples.hs:228:7: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [Integer -> formula] not matched: [] [_] [_, _] (_:_:_:_:_) | 228 | let [x, y, out] = List.map mk_knows ["x", "y", "out"] in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/PropExamples.hs:230:7: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [Integer -> Integer -> formula] not matched: [] [_] (_:_:_:_) | 230 | [u, v] = List.map mk_knows2 ["u", "v"] in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [ 9 of 25] Compiling Data.Logic.ATP.DP ( src/Data/Logic/ATP/DP.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/DP.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/DP.dyn_o ) src/Data/Logic/ATP/DP.hs:30:1: warning: [GHC-90177] [-Worphans] Orphan instance: instance NumAtom (Knows Integer) 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. | 30 | instance NumAtom (Knows Integer) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^... src/Data/Logic/ATP/DP.hs:89:7: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type Maybe lit not matched: Nothing | 89 | Just p = minimize (resolution_blowup clauses) pvs | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/DP.hs:114:5: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type Maybe lit not matched: Nothing | 114 | Just p = maximize (posneg_count clauses) pvs | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/DP.hs:142:53: 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 | 142 | dpllsat :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool | ^ src/Data/Logic/ATP/DP.hs:145: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 | 145 | dplltaut :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool | ^ src/Data/Logic/ATP/DP.hs:163:19: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type Maybe formula not matched: Nothing | 163 | ps -> let Just p = maximize (posneg_count cls') ps in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/DP.hs:224:17: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type Maybe formula not matched: Nothing | 224 | ps -> let Just p = maximize (posneg_count cls') ps in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [10 of 25] Compiling Data.Logic.ATP.Term ( src/Data/Logic/ATP/Term.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Term.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Apply.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Quantified.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Equate.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/FOL.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Skolem.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Parser.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/ParserTests.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/ParserTests.dyn_o ) [18 of 25] Compiling Data.Logic.ATP.Prolog ( src/Data/Logic/ATP/Prolog.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Prolog.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/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) => | ^ [19 of 25] Compiling Data.Logic.ATP.Herbrand ( src/Data/Logic/ATP/Herbrand.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Herbrand.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Herbrand.dyn_o ) src/Data/Logic/ATP/Herbrand.hs:38: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 | 38 | herbfuns :: (atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, IsFormula fof, HasApply atom, Ord function) => fof -> (Set (function, Arity), Set (function, Arity)) | ^ src/Data/Logic/ATP/Herbrand.hs:38: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 | 38 | herbfuns :: (atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, IsFormula fof, HasApply atom, Ord function) => fof -> (Set (function, Arity), Set (function, Arity)) | ^ src/Data/Logic/ATP/Herbrand.hs:38: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 | 38 | herbfuns :: (atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, IsFormula fof, HasApply atom, Ord function) => fof -> (Set (function, Arity), Set (function, Arity)) | ^ src/Data/Logic/ATP/Herbrand.hs:44: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 | 44 | groundterms :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Arity) -> Int -> Set term | ^ src/Data/Logic/ATP/Herbrand.hs:44: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 | 44 | groundterms :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Arity) -> Int -> Set term | ^ src/Data/Logic/ATP/Herbrand.hs:51: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 | 51 | groundtuples :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Int) -> Int -> Int -> Set [term] | ^ src/Data/Logic/ATP/Herbrand.hs:51: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 | 51 | groundtuples :: (v ~ TVarOf term, f ~ FunOf term, IsTerm term) => Set term -> Set (f, Int) -> Int -> Int -> Set [term] | ^ src/Data/Logic/ATP/Herbrand.hs:61: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 | 61 | (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:61: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 | 61 | (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:61: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 | 61 | (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:61:78: 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 | 61 | (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:61: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 | 61 | (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:89:23: 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 | 89 | gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:89: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 | 89 | gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:89:66: 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 | 89 | gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:89:82: 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 | 89 | gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:89:99: 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 | 89 | gilmore_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:109: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 | 109 | atom ~ AtomOf fof, | ^ src/Data/Logic/ATP/Herbrand.hs:110: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 | 110 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Herbrand.hs:111: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 | 111 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:112:15: 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 | 112 | v ~ TVarOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:113:15: 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 | 113 | v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Herbrand.hs:205: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 | 205 | dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:205: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 | 205 | dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:205: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 | 205 | dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:205: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 | 205 | dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:205:94: 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 | 205 | dp_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:222: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 | 222 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Herbrand.hs:223: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 | 223 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Herbrand.hs:224: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 | 224 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:225: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 | 225 | v ~ TVarOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:226: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 | 226 | v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Herbrand.hs:247:23: 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 | 247 | atom ~ AtomOf formula, | ^ src/Data/Logic/ATP/Herbrand.hs:248:23: 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 | 248 | term ~ TermOf atom, | ^ src/Data/Logic/ATP/Herbrand.hs:249: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 | 249 | function ~ FunOf term, | ^ src/Data/Logic/ATP/Herbrand.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 | v ~ TVarOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:251: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 | 251 | v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Herbrand.hs:264: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 | 264 | dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:264: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 | 264 | dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:264:68: 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 | 264 | dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:264:84: 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 | 264 | dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:264:101: 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 | 264 | dp_refine_loop :: (atom ~ AtomOf lit, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function, | ^ src/Data/Logic/ATP/Herbrand.hs:281: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 | 281 | dp_refine :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:281: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 | 281 | dp_refine :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Herbrand.hs:281: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 | 281 | dp_refine :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ [20 of 25] Compiling Data.Logic.ATP.Unif ( src/Data/Logic/ATP/Unif.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Unif.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Unif.dyn_o ) src/Data/Logic/ATP/Unif.hs:27:1: warning: [-Wdodgy-imports] Module Control.Monad.State does not export fail | 27 | import Control.Monad.State hiding (fail) -- (evalStateT, runStateT, State, StateT, get) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/Unif.hs:64: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 | 64 | unify_terms :: (IsTerm term, v ~ TVarOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:69: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 | 69 | (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:69:53: 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 | (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:85: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 | 85 | istriv :: forall term v f m. (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:85: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 | 85 | istriv :: forall term v f m. (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:97: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 | 97 | solve :: (IsTerm term, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Unif.hs:104: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 | 104 | fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:104:47: 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 | 104 | fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:109: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 | 109 | unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:109:53: 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 | 109 | unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:119: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 | 119 | (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, | ^ src/Data/Logic/ATP/Unif.hs:119:78: 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 | 119 | (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, | ^ src/Data/Logic/ATP/Unif.hs:120:60: 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 | JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, | ^ src/Data/Logic/ATP/Unif.hs:120: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 | 120 | JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, | ^ src/Data/Logic/ATP/Unif.hs:121: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 | 121 | Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, | ^ src/Data/Logic/ATP/Unif.hs:121: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 | 121 | Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, | ^ src/Data/Logic/ATP/Unif.hs:133: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 | 133 | unify_atoms :: (JustApply atom1, term ~ TermOf atom1, | ^ src/Data/Logic/ATP/Unif.hs:134: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 | 134 | JustApply atom2, term ~ TermOf atom2, | ^ src/Data/Logic/ATP/Unif.hs:135: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 | 135 | v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:135:47: 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 | 135 | v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:140: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 | 140 | unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1, | ^ src/Data/Logic/ATP/Unif.hs:141: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 | 141 | HasEquate atom2, term ~ TermOf atom2, | ^ src/Data/Logic/ATP/Unif.hs:142:33: 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 | 142 | PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, MonadFail m) => | ^ src/Data/Logic/ATP/Unif.hs:142: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 | 142 | PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, MonadFail m) => | ^ [21 of 25] Compiling Data.Logic.ATP.Tableaux ( src/Data/Logic/ATP/Tableaux.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Tableaux.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Tableaux.dyn_o ) src/Data/Logic/ATP/Tableaux.hs:50: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 | 50 | Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:50: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 | 50 | Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:51: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 | 51 | atom1 ~ AtomOf lit1, term ~ TermOf atom1, | ^ src/Data/Logic/ATP/Tableaux.hs:51: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 | 51 | atom1 ~ AtomOf lit1, term ~ TermOf atom1, | ^ src/Data/Logic/ATP/Tableaux.hs:52: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 | 52 | atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) => | ^ src/Data/Logic/ATP/Tableaux.hs:52: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 | 52 | atom2 ~ AtomOf lit2, term ~ TermOf atom2, MonadFail m) => | ^ src/Data/Logic/ATP/Tableaux.hs:58: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 | 58 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:58: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 | 58 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), v ~ TVarOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:59:23: 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 | 59 | atom ~ AtomOf lit, term ~ TermOf atom) => | ^ src/Data/Logic/ATP/Tableaux.hs:59: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 | 59 | atom ~ AtomOf lit, term ~ TermOf atom) => | ^ src/Data/Logic/ATP/Tableaux.hs:72:92: 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 | 72 | (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Tableaux.hs:73:23: 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 | 73 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:73: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 | 73 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:73: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 | 73 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:85:81: 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 | 85 | (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, | ^ src/Data/Logic/ATP/Tableaux.hs:86: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 | 86 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:86:41: 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 | 86 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:86:65: 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 | 86 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:87:15: 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 | 87 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:87: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 | 87 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:114:81: 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 | 114 | compare :: (IsFirstOrder formula, Ord formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Show formula, | ^ src/Data/Logic/ATP/Tableaux.hs:115: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 | 115 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:115:41: 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 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:115:65: 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 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:116:15: 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 | 116 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:116: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 | 116 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:182:68: 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 | 182 | (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Tableaux.hs:183: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 | 183 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:183:41: 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 | 183 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:183:65: 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 | 183 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:183:81: 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 | 183 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:218:70: 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 | tabrefute :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Tableaux.hs:219: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 | 219 | atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:219:43: 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 | 219 | atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:219:60: 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 | 219 | atom ~ AtomOf formula, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Tableaux.hs:225:64: 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 | 225 | tab :: (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Pretty formula, HasSkolem function, | ^ src/Data/Logic/ATP/Tableaux.hs:226: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 | 226 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:226: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 | 226 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:226: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 | 226 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:227:11: 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 | 227 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:227: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 | 227 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:292:69: 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 | 292 | (IsFirstOrder formula, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord formula, Pretty formula, HasSkolem function, | ^ src/Data/Logic/ATP/Tableaux.hs:293: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 | 293 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:293: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 | 293 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:293:66: 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 | 293 | atom ~ AtomOf formula, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Tableaux.hs:294: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 | 294 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:294:33: 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 | 294 | v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Tableaux.hs:296:1: warning: [-Wunused-top-binds] Defined but not used: splittab | 296 | splittab fm = | ^^^^^^^^ [22 of 25] Compiling Data.Logic.ATP.Resolution ( src/Data/Logic/ATP/Resolution.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Resolution.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Resolution.dyn_o ) src/Data/Logic/ATP/Resolution.hs:71:74: 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 | (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, | ^ src/Data/Logic/ATP/Resolution.hs:72: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 | 72 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:72:33: 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 | 72 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:72:50: 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 | 72 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:83:93: 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 | 83 | (JustLiteral lit, IsTerm term, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Resolution.hs:84: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 | 84 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:84: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 | 84 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:84: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 | 84 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:93: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 | 93 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:93: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 | 93 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:93:53: 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 | 93 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:104:90: 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 | 104 | resolvents :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, | ^ src/Data/Logic/ATP/Resolution.hs:105: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 | 105 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:105: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 | 105 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:105: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 | 105 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:121: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 | 121 | resolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, | ^ src/Data/Logic/ATP/Resolution.hs:122: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 | 122 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:122: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 | 122 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:122: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 | 122 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:133:101: 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 | 133 | resloop1 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Resolution.hs:134: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 | 134 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:134: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 | 134 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:134:55: 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 | 134 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:147: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 | 147 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:147: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 | 147 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:147: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 | 147 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:149:55: 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 | 149 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Resolution.hs:155:68: 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 | 155 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, | ^ src/Data/Logic/ATP/Resolution.hs:156: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 | 156 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:156:41: 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 | 156 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:156:65: 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 | 156 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:156:81: 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 | 156 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:156:98: 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 | 156 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:184:47: 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 | 184 | match_terms :: forall term v. (IsTerm term, v ~ TVarOf term) => Map v term -> [(term, term)] -> Failing (Map v term) | ^ src/Data/Logic/ATP/Resolution.hs:199: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 | 199 | match_atoms :: (JustApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:199:68: 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 | 199 | match_atoms :: (JustApply atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:204: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 | 204 | match_atoms_eq :: (HasEquate atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:204:71: 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 | 204 | match_atoms_eq :: (HasEquate atom, IsTerm term, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:212: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 | 212 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:212: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 | 212 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:212: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 | 212 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:224:68: 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 | 224 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, | ^ src/Data/Logic/ATP/Resolution.hs:225: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 | 225 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:225:41: 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 | 225 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:225:65: 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 | 225 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:225:81: 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 | 225 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:225:98: 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 | 225 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ TVarOf term, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:232:55: 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 | 232 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, | ^ src/Data/Logic/ATP/Resolution.hs:233: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 | 233 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:233: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 | 233 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:233: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 | 233 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:238:47: 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 | 238 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, | ^ src/Data/Logic/ATP/Resolution.hs:239: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 | 239 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:239: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 | 239 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:239:55: 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 | 239 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:251: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 | 251 | incorporate :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:251:41: 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 | 251 | incorporate :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:251: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 | 251 | incorporate :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:264: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 | 264 | replace :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:264: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 | 264 | replace :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:264: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 | 264 | replace :: (atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:280: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 | 280 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:280: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 | 280 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:280: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 | 280 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:299:68: 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 | 299 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, Pretty fof, | ^ src/Data/Logic/ATP/Resolution.hs:300: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 | 300 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:300:41: 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 | 300 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:300:65: 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 | 300 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:300:81: 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 | 300 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:300:96: 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 | 300 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:306:73: 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 | 306 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, Ord fof, Pretty fof, | ^ src/Data/Logic/ATP/Resolution.hs:307: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 | 307 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:307: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 | 307 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:307: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 | 307 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:307:78: 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 | 307 | atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:312:74: 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 | 312 | Match (atom, atom) v term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Resolution.hs:313: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 | 313 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:313: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 | 313 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:313:55: 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 | 313 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:327:109: 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 | 327 | presolve_clauses :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Resolution.hs:328: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 | 328 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:328: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 | 328 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:328: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 | 328 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Resolution.hs:337:68: 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 | 337 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Match (atom, atom) v term, HasSkolem function, Monad m, Ord fof, | ^ src/Data/Logic/ATP/Resolution.hs:338: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 | 338 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:338:41: 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 | 338 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:338:65: 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 | 338 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:338:81: 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 | 338 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:338:96: 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 | 338 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Resolution.hs:344: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 | 344 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:344: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 | 344 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:344: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 | 344 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:344:78: 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 | 344 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Resolution.hs:346:55: 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 | 346 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Resolution.hs:1104:9: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [SkTerm] not matched: [] [_] [_, _] (_:_:_:_:_) | 1104 | let [x, y, z] = List.map (vt :: V -> SkTerm) ["x", "y", "z"] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ src/Data/Logic/ATP/Resolution.hs:1105:9: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [[SkTerm] -> Formula] not matched: [] [_] (_:_:_:_) | 1105 | [p, q] = List.map pApp ["P", "Q"] :: [[SkTerm] -> Formula] | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [23 of 25] Compiling Data.Logic.ATP.Meson ( src/Data/Logic/ATP/Meson.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Meson.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Meson.dyn_o ) src/Data/Logic/ATP/Meson.hs:179:75: 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 | 179 | HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Meson.hs:180: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 | 180 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:180: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 | 180 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:180:55: 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 | 180 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:209: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 | 209 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, | ^ src/Data/Logic/ATP/Meson.hs:210: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 | 210 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Meson.hs:210: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 | 210 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Meson.hs:210:64: 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 | 210 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, | ^ src/Data/Logic/ATP/Meson.hs:211: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 | 211 | v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:211:33: 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 | 211 | v ~ VarOf fof, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:222: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 | 222 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, HasSkolem function, Monad m, | ^ src/Data/Logic/ATP/Meson.hs:223: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 | 223 | atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:223: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 | 223 | atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:223: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 | 223 | atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:223: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 | 223 | atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:223:101: 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 | 223 | atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:223:116: 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 | 223 | atom ~ AtomOf fof, term ~ TermOf atom, predicate ~ PredOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:233:76: 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 | equal :: (JustLiteral lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, | ^ src/Data/Logic/ATP/Meson.hs:234: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 | 234 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:234: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 | 234 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:234: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 | 234 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:260:101: 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 | 260 | mexpand2 :: (JustLiteral lit, Ord lit, HasApply atom, IsTerm term, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), | ^ src/Data/Logic/ATP/Meson.hs:261: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 | 261 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:261: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 | 261 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:261:55: 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 | 261 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:287:88: 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 | 287 | mexpands :: (JustLiteral lit, Ord lit, HasApply atom, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), IsTerm term, | ^ src/Data/Logic/ATP/Meson.hs:288: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 | 288 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:288: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 | 288 | atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:288:55: 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 lit, term ~ TermOf atom, v ~ TVarOf term) => | ^ src/Data/Logic/ATP/Meson.hs:318: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 | 318 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Meson.hs:318: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 | 318 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Meson.hs:318: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 | 318 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Meson.hs:318:71: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Meson.hs:320:48: 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 | Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof | ^ src/Data/Logic/ATP/Meson.hs:331: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 | 331 | (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), Ord fof, | ^ src/Data/Logic/ATP/Meson.hs:333: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 | 333 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:333: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 | 333 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:333:60: 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 | 333 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:333:76: 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 | 333 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:333:91: 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 | 333 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:339: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 | 339 | meson :: (IsFirstOrder fof, Unify Failing (atom, atom), term ~ UTermOf (atom, atom), HasSkolem function, Monad m, Ord fof, | ^ src/Data/Logic/ATP/Meson.hs:340: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 | 340 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:340: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 | 340 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:340: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 | 340 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:340:75: 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 | 340 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ src/Data/Logic/ATP/Meson.hs:340:90: 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 | 340 | atom ~ AtomOf fof, term ~ TermOf atom, function ~ FunOf term, v ~ VarOf fof, v ~ SVarOf function) => | ^ [24 of 25] Compiling Data.Logic.ATP.Equal ( src/Data/Logic/ATP/Equal.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Equal.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP/Equal.dyn_o ) src/Data/Logic/ATP/Equal.hs:60: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 | 60 | (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:60: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 | 60 | (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:60:66: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:60:83: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:60:98: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:60:122: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, p ~ PredOf atom, v ~ VarOf fof, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:77: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 | 77 | predicate_congruence :: (atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Equal.hs:77:55: 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 | 77 | predicate_congruence :: (atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Equal.hs:77:75: 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 | 77 | predicate_congruence :: (atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Equal.hs:77:92: 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 | 77 | predicate_congruence :: (atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Equal.hs:77:107: 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 | 77 | predicate_congruence :: (atom ~ AtomOf fof, predicate ~ PredOf atom, term ~ TermOf atom, v ~ VarOf fof, v ~ TVarOf term, | ^ src/Data/Logic/ATP/Equal.hs:95: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 | 95 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, | ^ src/Data/Logic/ATP/Equal.hs:95:48: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, | ^ src/Data/Logic/ATP/Equal.hs:95:65: 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 | (atom ~ AtomOf fof, term ~ TermOf atom, v ~ VarOf fof, | ^ src/Data/Logic/ATP/Equal.hs:110: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 | 110 | (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:110: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 | 110 | (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:110: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 | 110 | (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:110: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 | 110 | (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:110:104: 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 | 110 | (atom ~ AtomOf formula, term ~ TermOf atom, v ~ VarOf formula, v ~ TVarOf term, function ~ FunOf term, | ^ src/Data/Logic/ATP/Equal.hs:229:1: warning: [-Wunused-top-binds] Defined but not used: testEqual04 | 229 | testEqual04 = TestLabel "equalitize 3 (p. 248)" $ TestCase $ | ^^^^^^^^^^^ [25 of 25] Compiling Data.Logic.ATP ( src/Data/Logic/ATP.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP.o, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/Data/Logic/ATP.dyn_o ) Preprocessing test suite 'atp-haskell-tests' for atp-haskell-1.14.3.. Building test suite 'atp-haskell-tests' for atp-haskell-1.14.3.. [1 of 2] Compiling Extra ( tests/Extra.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/atp-haskell-tests/atp-haskell-tests-tmp/Extra.o ) tests/Extra.hs:95:13: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [SkTerm] not matched: [] [_] (_:_:_:_) | 95 | fms = [ let [x, y] = [vt "x", vt "y"] :: [SkTerm] in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ tests/Extra.hs:100:13: warning: [GHC-62161] [-Wincomplete-uni-patterns] Pattern match(es) are non-exhaustive In a pattern binding: Patterns of type [[SkTerm] -> Formula] not matched: [] [_] [_, _] (_:_:_:_:_) | 100 | [s, h, m] = [pApp "S", pApp "H", pApp "M"] :: [[SkTerm] -> Formula] in | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ [2 of 2] Compiling Main ( tests/Main.hs, /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/atp-haskell-tests/atp-haskell-tests-tmp/Main.o ) [3 of 3] Linking /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/build/atp-haskell-tests/atp-haskell-tests Running 1 test suites... Test suite atp-haskell-tests: RUNNING... Test suite atp-haskell-tests: PASS Test suite logged to: /home/builder/builder-dir/build-cache/tmp-install/reports/atp-haskell-1.14.3.test Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.LitWrapper.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Equal.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Meson.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Prolog.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Resolution.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Tableaux.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Unif.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Herbrand.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Skolem.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.ParserTests.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.FOL.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Parser.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Quantified.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.DP.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.DefCNF.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.PropExamples.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Prop.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Lit.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Equate.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Apply.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Term.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Formulas.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Pretty.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Lib.hs.html Writing: hpc_index.html Writing: hpc_index_fun.html Writing: hpc_index_alt.html Writing: hpc_index_exp.html Test coverage report written to /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/hpc/vanilla/html/atp-haskell-tests/hpc_index.html 1 of 1 test suites (1 of 1 test cases) passed. Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.LitWrapper.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Equal.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Meson.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Prolog.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Resolution.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Tableaux.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Unif.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Herbrand.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Skolem.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.ParserTests.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.FOL.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Parser.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Quantified.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.DP.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.DefCNF.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.PropExamples.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Prop.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Lit.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Equate.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Apply.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Term.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Formulas.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Pretty.hs.html Writing: atp-haskell-1.14.3-inplace/Data.Logic.ATP.Lib.hs.html Writing: hpc_index.html Writing: hpc_index_fun.html Writing: hpc_index_alt.html Writing: hpc_index_exp.html Package coverage report written to /home/builder/builder-dir/build-cache/tmp-install/dist-newstyle/build/x86_64-linux/ghc-9.6.3/atp-haskell-1.14.3/noopt/hpc/vanilla/html/atp-haskell-1.14.3/hpc_index.html