Add a typing rule for dataToTag#
Because of parametricity, every polymorphic function a -> Int#
should be constant (disregarding _|_
).
However, dataToTag# :: a -> Int#
breaks this: dataToTag# False
is 0#
, dataToTag# True
is 1#
.
I think dataToTag#
should have a special typing rule, just like tagToEnum#
.
Possible ideas:
-
The type should be a statically known algebraic data type. Currently
dataToTag#
returns0#
for functions - I think that should be a type error. It can be used on newtypes - we can either continue allowing this, or reject and requirecoerce
. -
Perhaps require that the constructors of the datatype are in scope
-
Perhaps
dataToTag#
could be levity-polymorphic so that it works with UnliftedDatatypes
In GHC.Base
, there's a wrapper getTag x = dataToTag# x
. It can now be deprecated: it's no longer needed since ac977688.
Low priority: this function is rather obscure and mostly meant for deriving
. This is probably best done after predicates #20000.