[Agda] ≡ → ≈

[Matus Tejiscak]

Quoting Sergei Meshveliani <mechvel at botik.ru>:
> The checker sees that  PE.refl  is the only value in  x ≡ y,
> so it needs to put  PE.refl  for `_'.
> Why does not it?

I don't know the exact fundamental reasons but there is at least one  
technical reason that this is not as simple. Consider the following  
program:

> f : {A B : Set} {x : A} {f g : A → B} → f x ≡ g x → f x ≡ g x
> f eq = eq
>
> g : {A B : Set} {x : A} {f g : A → B} → f x ≡ g x → f x ≡ g x
> g refl = refl

While the function f typechecks, the function g does not. The reason  
is that when pattern-matching on the refl, Agda would have to unify (f  
x) with (g x), which is impossible because neither is a variable.

Best regards,
Matus
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: PGP Digital Signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20131017/5c792674/attachment.bin