[Agda] Question about inequality and absurd patterns

[William Harrison]

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 ]
-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201001/85a72650/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: MinimalExample.agda
Type: application/octet-stream
Size: 385 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201001/85a72650/attachment.obj>