[Agda] reply to Agda 2.6.3.20230805

[mechvel at scico.botik.ru]

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