Consider
data Tag a where
TagInt :: Tag Int
TagBool :: Tag Bool
then we can implement a function of type
geqEx :: Product Tag [] a -> Product Tag b -> Maybe (a :~: b)
working as geq. But that Product doesn't have GEq instance.
We can either document this, or remove the instance for the same reason as there isn't TestEquality (Product f g) as in "we don't want to chose which way to bias the instance.
Consider
then we can implement a function of type
working as
geq. But thatProductdoesn't haveGEqinstance.We can either document this, or remove the instance for the same reason as there isn't
TestEquality (Product f g)as in "we don't want to chose which way to bias the instance.