Well, not to overly nitpick what is otherwise a lot of good sense coming out of you, but in Haskell at least instances of Eq are strongly encouraged to satisfy reflexivity and extensionality, which for instance Eq Type rule out eq _ _ = False and eq _ _ = True respectively (the latter case assuming we get Π-functions to discriminate between types). instance Eq Empty trivially satisfies both.