[Agda] ANNOUNCE: Agda 2.4.2.4 release candidate

[Sergei Meshveliani]

On Tue, 2015-09-15 at 00:01 +0400, Sergei Meshveliani wrote:
> On Mon, 2015-09-14 at 09:19 -0500, Andrés Sicard-Ramírez wrote:
> > Hi,
> > 
> > We would like to announce a release candidate for Agda 2.4.2.4 available at
> > 
> >   http://www1.eafit.edu.co/asr/tmp/Agda-2.4.2.3.20150913.tar.gz
> > 
> > [..]
> 
> 
> It has type-checked almost all my DoCon-A.
> And in the end, it shows a difference to  Agda-2.4.2.3
> 
> when type-checking the equality proof of
> 
>     e00 : Π' (map asd (map (pairValue ∘ pairFromAsd) ps')) ='           
>           Π' (map (asd ∘ (pairValue ∘ pairFromAsd)) ps')
> 
>     e00 = =asdReflexive $ PE.cong Π' $ PE.sym $ map-compose ps'
> 
> It reports
> 
> Expected a visible argument, but found a hidden argument
> when checking that the expression
> =asdReflexive $ PE.cong Π' $ PE.sym $ map-compose ps' 
> has type
> Π' (map asd (map ((λ {.x} → pairValue) ∘ pairFromAsd) ps')) ='
> Π' (map ((λ {.x} → asd) ∘ (λ {.x} → pairValue) ∘ pairFromAsd) ps')
> 
> Agda-2.4.2.3 type-checked this.
> 
> May this be due to some syntax change in the language?
> 
> The matter is in  "=asdReflexive $".
> If it is removed, and  ='  replaced with  ≡,  then it is type-checked.
> PE is the PropositioanlEquality name.
> 
> =asdReflexive  is defined in another module as
> 
>   =asdRefl : Reflexive _='_
>   =asdRefl = ~asd-refl
> 
>   =asdReflexive : _≡_ ⇒ _='_  =asdRefl : Reflexive _='_
>   =asdRefl = ~asd-refl


Sorry, the last  two lines  is a typo (by copy-paste). It needs to be

    =asdReflexive : _≡_ ⇒ _='_
    =asdReflexive {x} PE.refl =  =asdRefl {x}




> May be Agda has changed treating of hidden arguments?
> 
> I can provide a self-contained code. But it is large. 
> So that if you just guess what is it, we could save effort.
> 
> Regards,
> 
> ------
> Sergei 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>