[Agda] reply to Agda 2.6.3.20230805

[mechvel at scico.botik.ru]

On 2023-08-25 19:54, Shu-Hung You wrote:
> 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


So, it looks like Agda-2.6.4-rc1  is more correct.
Thank you.

------
Sergei



> 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