Why does the Eq instance of Map involve comparing the key?

[jchia]

The key has no run-time representation. If two Map values can be used as arguments to ==, they must have the same type so their keys (KnownSymbol) must be the same. Consequently, the k == k' in the Eq instance seems unnecessary. Another way to put it is that for any k, Var k has only one value (Var), so equality is always trivially true. Am I missing something?

[jmorag]

Looks like in the latest version on hackage (0.8.9.0) the instance no longer relies on comparing Var for equality, which as you correctly point out is unnecessary.

instance Eq (Map '[]) where
    Empty == Empty = True

instance (Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) where
    (Ext Var v m) == (Ext Var v' m') = v == v' && m == m'
    -- could also be
    -- (Ext _ v m) == (Ext _ v' m') = ...

[dorchard]

Okay great- so... I think I can close this then!