Okay, some background... The builtins have a notion of equality, but only for primitive atomic types.
I'm reasonably certain it's not an oversight to not have a stronger notion of equality at this layer. It could be defined in general... The first step would be to fully evaluate both items (which has to be defined carefully in a separate section, anyway). That would result in two trees of nodes, each describing a rooted object graph via the usual substitutions of backreferences. The notional object graphs would then be compared structurally, by unification without an occurs check; the omission of the occurs check means that cyclic structures are allowed.
But, I don't think that stronger notion is useful! For data-like values, it's not bad, but for function-like values, and type-like values which include functions, structural equality has the benefit of being easily computable, but is not actually anything anyone cares about. :) And besides, the ability to compare types needs to be hidden somehow so that it can be used in situations where macro-like stuff is useful, but not in situations where parametricity is desirable, which are the majority...
That is, you can no longer infer that "a -> a" is actually the identity function if it's possible that it could switch on "a" and treat "int8" differently from "int16". Which I'm pretty sure it can, at present, via the type-manipulation builtins... But you (maybe, it needs thought) still want to be able to write functions that transform types, because those can be useful! So there probably needs to be a notion of "inspectable type", which wouldn't be the default.
Okay, some background... The builtins have a notion of equality, but only for primitive atomic types.
I'm reasonably certain it's not an oversight to not have a stronger notion of equality at this layer. It could be defined in general... The first step would be to fully evaluate both items (which has to be defined carefully in a separate section, anyway). That would result in two trees of nodes, each describing a rooted object graph via the usual substitutions of backreferences. The notional object graphs would then be compared structurally, by unification without an occurs check; the omission of the occurs check means that cyclic structures are allowed.
But, I don't think that stronger notion is useful! For data-like values, it's not bad, but for function-like values, and type-like values which include functions, structural equality has the benefit of being easily computable, but is not actually anything anyone cares about. :) And besides, the ability to compare types needs to be hidden somehow so that it can be used in situations where macro-like stuff is useful, but not in situations where parametricity is desirable, which are the majority...
That is, you can no longer infer that "a -> a" is actually the identity function if it's possible that it could switch on "a" and treat "int8" differently from "int16". Which I'm pretty sure it can, at present, via the type-manipulation builtins... But you (maybe, it needs thought) still want to be able to write functions that transform types, because those can be useful! So there probably needs to be a notion of "inspectable type", which wouldn't be the default.