[Agda] Question about inequality and absurd patterns

[mechvel at scico.botik.ru]

On 2020-10-01 23:19, William Harrison wrote:
> Hi-
> 
>      I have a question about proving inequalities (≢) in Agda. It's
> probably such a stupid question that I should be embarrassed for
> asking it, but, fortunately, I lost my capacity to feel embarrassment
> years ago.
> 
> In the following Agda code, the "good" definition works, but the "bad"
> one does not and yields the commented complaint. I assume that (≢)
> insists on literal term equality and that is the source of the
> different responses from Agda. Is there any way of evaluating under
> the (≢)? I'm formulating a typed language using strings for
> variables, and so this sort of inequality calculation is involving in
> variable dereference. I've attached a minimal example. Thanks in
> advance.
> 
>> good : "x" ≢ "y"
>> 
>> good ()
>> 
>> bad : "x" ≢ Data.Vec.head ("y" ∷ "y" ∷ [])
>> 
>> bad ()
>> 
>> {-
>> 
>> Failed to solve the following constraints:
>> 
>> Is empty: "x" ≡ head ("y" ∷ "y" ∷ [])
>> 
>> [ at <...snip...>/MinimalExample.agda:11,5-7 ]
>> 
>> -}

And
     bad = good

is type-checked (in Agda 2.6.1).
I do not guess what is the matter.

--
SM