[Agda] Re: Do we really want special case casts?

[Samuel Gélineau]

On Sun, Oct 18, 2009 at 5:30 PM, Nils Anders Danielsson
<nad at cs.nott.ac.uk> wrote:
>> I don't know what is the cause of this ordering restriction, but I'll
>> make sure to remember it now.
>
> http://wiki.portal.chalmers.se/agda/agda.php?n=ReferenceManual.PatternMatching

Thanks, but that page is explaining why the top-to-bottom ordering of
the patterns matters, isn't it?

Here it is the left-to-right ordering which confused me, and the only
mention of this I can see in that page is "For each clause the
arguments will be matched against the corresponding patterns from left
to right. If there is a mismatch the next clause is tried". But in
this case, there is no mismatch: the runtime value of y₁ ≅ y₂ is refl
(what else could it be?), which I expected would convince Agda that
the types of y₁ and y₂ were the same.

I am now very confused. On one hand, the implementation of ≅⇒≡₁ shows
that if the runtime value of y₁ ≅ y₂ is refl, then on the right-hand
side the types of y₁ and y₂ are considered the same. On the other
hand, the error raised by the implementation of fail shows that even
if the runtime value of y₁ ≅ y₂ is refl, then Agda still can't accept
this as a correct pattern because x₁ and x₂ could be different, so
Agda isn't convinced yet that the types B x₁ and B x₂ are the same.
Why is it that in one case, Agda concludes that the types are the
same, while in the other, Agda requires to know that already?

I find it especially weird that giving dependency information to Agda
can impede its ability to conclude things. Consider the following
implementation:

pass2 : {A : Set}{B : A → Set}
      → {x₁ : A}{y₁ : B x₁}
      → {x₂ : A}{y₂ : B x₂}
      → y₁ ≅ y₂
      → x₁ ≅ x₂
      → y₁ ≅ y₂
pass2 prf₁ prf₂ = lemma prf₁ prf₂ where
  lemma : ∀ {A B₁ B₂}
        → {x₁ : A}{y₁ : B₁}
        → {x₂ : A}{y₂ : B₂}
        → y₁ ≅ y₂
        → x₁ ≅ x₂
        → y₁ ≅ y₂
  lemma refl refl = refl


pass2 is a version of fail which explicitly drops dependency
information in order to accept the refl proofs in the "wrong" order.
how can having less information be better than having more?

– Samuel