This is on agda-2.6.4.2 built by
$ cabal install -foptimise-heavily -j1,
used with stdlib-2.0,
ghc-9.0.2, under Linux Debian 12, x86_64 machine.
The below module fragment is type-checked by agda-2.6.4.1 but not by agda-2.6.4.2 :
private
-- This is the internal loop in compose-reduceMutually
--
aux-I : ℕ → List Pol → List Pol → List Pol
aux-I 0 _ fs = fs
aux-I (suc cnt) fs' fs with any? lmOrdPair? (zip fs' fs)
... | no _ = fs
... | yes _ = aux-I cnt (reduceMutually fs') fs'
compose-reduceMutually : ℕ → List Pol → List Pol
compose-reduceMutually m fs = unzero (aux-I m (reduceMutually fs) fs)
private
-- We do not see how to avoid using these "-base" and "-step" functions.
--
aux-I-base : ∀ m fs' fs → ¬ Any LmOrdPair (zip fs' fs) → aux-I m fs' fs ≡ fs
aux-I-base 0 _ _ _ = PE.refl
aux-I-base (suc m) fs' fs ¬anyOrd with any? lmOrdPair? (zip fs' fs)
... | no _ = PE.refl -- this is the point, line 245 ***
... | yes anyOrd = contradiction anyOrd ¬anyOrd
The command is
$ agda $agdaLibOpt $agdaFlags GBasis/OverEuclidean/I.agda +RTS -M7G
where $agdaFlags = --auto-inline --guardedness.
The report is
home/mechvel/inAgda/doconA/3.2/source/GBasis/OverEuclidean/I.agda:245,51-58
aux-I E vars ppo (suc m) fs' fs
| any? lmOrdPair? (Data.List.zipWith _,_ fs' fs) != fs of type
List
(Pol.OverDecComMonoid.Pol (OfMonoids.mkDecComMonoid
...
(EuclideanDomain.decIntegralDomain E)))))) _≟_)
(Data.List.foldr (λ _ → suc) 0 vars) ppo)
when checking that the expression PE.refl has type
(aux-I E vars ppo (suc m) fs' fs | any? lmOrdPair? (Data.List.zipWith _,_ fs' fs)) ≡ fs
Which Agda is more correct in this case: 2.6.4.1 or 2.6.4.2 ?
Is this fragment sufficient to guess of the source?
It not, may be I would try to simplify the example, (which is a very complex code, using many modules).
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4