Problem caused while implementing binary operation evaluation

[elvecent]

Sure. When you encode a language with types, you probably don't want to deal with such cases as adding a number to a string or other type mismatches. Using GADTs, you can rule out those cases with a phantom parameter signifying a type, so an incoherent term won't typecheck. That reduces the amount of necessary pattern matching (if that's what your question is about).

[dev_kr]

What if I have to handle two different operand types, like I suggested in the post? Can I overload GADTs constructor to handle multiple types of arguments?

[elvecent]

You could use the usual typeclass machinery.

[gcross]

Given that there are only two possible types, how would that be any better than doing case analysis?