[Agda] ANNOUNCE: Agda 2.4.2.4 release candidate

[Sergei Meshveliani]

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

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