Implicit, static type cast (coercion) in Haskell

Question

Problem

Consider the following design problem in Haskell. I have a simple, symbolic EDSL in which I want to express variables and general expressions (multivariate polynomials) such as x^2 * y + 2*z + 1. In addition, I want to express certain symbolic equations over expressions, say x^2 + 1 = 1, as well as definitions, like x := 2*y - 2.

The goal is to:

1. Have a separate type for variables and general expressions - certain functions might be applied to variables and not complex expressions. For instance, a definition operator := might be of type (:=) :: Variable -> Expression -> Definition and it should not be possible to pass a complex expression as its left-hand side parameter (though it should be possible to pass a variable as its right-hand side parameter, without explicit casting).
2. Have expressions an instance of Num, so that it's possible to promote integer literals to expressions and use a convenient notation for common algebraic operations like addition or multiplication without introducing some auxiliary wrapper operators.

In other words, I would like to have an implicit and static type cast (coercion) of variables to expressions. Now, I know that as such, there are no implicit type casts in Haskell. Nevertheless, certain object-oriented programming concepts (simple inheritance, in this case) are expressible in Haskell's type system, either with or without language extensions. How could I satisfy both above points while keeping a lightweight syntax? Is it even possible?

Discussion

It is clear that the main problem here is Num's type restriction, e.g.

(+) :: Num a => a -> a -> a

In principle, it's possible to write a single (generalised) algebraic data type for both variables and expressions. Then, one could write := in such a way, that the left-hand side expression is discriminated and only a variable constructor is accepted, with a run-time error otherwise. That's however not a clean, static (i.e. compile-time) solution...

Example

Ideally, I would like to achieve a lightweight syntax such as

computation = do
  x <- variable
  t <- variable

  t |:=| x^2 - 1
  solve (t |==| 0)

In particular, I want to forbid notation like t + 1 |:=| x^2 - 1 since := should give a definition of a variable and not an entire left-hand side expression.

Answer 1

To leverage polymorphism rather than subtyping (because that's all you have in Haskell), don't think "a variable is an expression", but "both variables and expressions have some operations in common". Those operations can be put in a type class:

class HasVar e where fromVar :: Variable -> e

instance HasVar Variable where fromVar = id
instance HasVar Expression where ...

Then, rather than casting things, make things polymorphic. If you have v :: forall e. HasVar e => e, it can be used both as an expression and as a variable.

example :: (forall e. HasVar e => e) -> Definition
example v = (v := v)  -- v can be used as both Variable and Expression

 where

  (:=) :: Variable -> Expression -> Definition

Skeleton to make the code below typecheck: https://gist.github.com/Lysxia/da30abac357deb7981412f1faf0d2103

computation :: Solver ()
computation = do
  V x <- variable
  V t <- variable
  t |:=| x^2 - 1
  solve (t |==| 0)