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