Remove use of unsafeCoerce in ExprMappable

[danmatichuk]

The function ExprMappable.symExprMappable uses unsafeCoerce as a workaround to define an ad-hoc ExprMappable instance for SymExpr, which is otherwise not possible in the Haskell type system since SymExpr is defined as a type family.
Although this coercion is currently not problematic, future changes to the run-time representation of ToExprMappable would introduce a run-time error if not handled correctly.

There are two solutions to avoid this:

1. Add the explicit constraint that the sym parameter for mapExpr is an ExprBuilder. This would avoid the need for reasoning about the SymExpr type family and instead allow reasoning about What4.Expr directly, which we can define instances for normally. This has the downside of requiring some refactoring to carry around this constraint in more places, since it is not necessarily available in every place mapExpr is used.

2. Use unsafeDerive provided by Data.Constraint.Unsafe, which is still unsafe but in a much more constrained way than unsafeCoerce (and generally makes it more clear exactly what is being coerced). This change would be entirely confined to the ExprMappable module (and so would be a straightforward change), but still admits the possibility of allowing run-time errors.

   • In general unsafeDerive can let you prove nonsense type constraints like 1 ~ 2, as well as create contexts where multiple class instances are in scope for the same type.