[Agda] reply to Agda 2.6.3.20230805

[Shu-Hung You]

>From what I found in the Agda repository, plt-amy discovered that not
counting the level of certain indices opens the door to falsity,
therefore additional checks are added (back).

The counterexample: https://github.com/agda/agda/issues/6654
The fix: https://github.com/agda/agda/pull/6661

On Thu, Aug 24, 2023 at 4:05 PM <mechvel at scico.botik.ru> wrote:
>
> I am trying Agda version 2.6.3.20230805
>
> Built with flags (cabal -f)
>   - optimise-heavily: extra optimizations
>
> with ghc 9.2.7 under Ubuntu Linux 18.04.
>
>
> 1) When installing, it warns
> ...
> src/Development/GitRev.hs:109:6: warning: [-Wincomplete-patterns]
>      Pattern match(es) are non-exhaustive
> ...
> src/Data/Hashable/Generic/Instances.hs:5:14: warning:
> [-Wtrustworthy-safe]
>      ‘Data.Hashable.Generic.Instances’ is marked as Trustworthy but has
> been inferred as safe!
> ...
>
> and many other warnings issued.
>
>
> 2) Type checking my library in Agda.
>
> The command is
> > agda $agdaLibOpt --auto-inline --guardedness List/I.agda,
>
> The message is
>
> "Set α is not less or equal than Set
> when checking that the type A of an argument to the constructor
> hasHead fits in the sort Set of the datatype.
> Note: this argument is forced by the indices of hasHead, so this
> definition would be allowed under --large-indices.
> "
> This is about
>
> --------------------------------------------
> module _ {A : Set α}
>    where
>    ...
>    ...
>    data HasHead : Pred (List A) 0ℓ
>         where
>         hasHead : (x : A) {xs : List A} → HasHead (x ∷ xs)       -- HERE
>
>    ¬HasHead : Pred (List A) 0ℓ
>    ¬HasHead = ¬_ ∘ HasHead
> -------------------------------------------
>
> Was Agda 2.6.3 wrong when allowed  0ℓ  here?
> I set the minimal level which is allowed by the type checker.
> On the other hand, as A : Set α, probably Pred (List A)  has to require
> α  for the level
> -- ?
>
> Regards,
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda