Cast implícito, tipo estático (coerción) en Haskell

Problema

Considere el siguiente problema de diseño en Haskell. Tengo un EDSL simple y simbólico en el que quiero expresar variables y expresiones generales (polinomios multivariados) como x^2 * y + 2*z + 1. Además, quiero expresar ciertas ecuaciones simbólicas sobre expresiones, digamos x^2 + 1 = 1, así como definiciones , como x := 2*y - 2.

La meta es:

1. Tenga un tipo separado para variables y expresiones generales: ciertas funciones pueden aplicarse a variables y no a expresiones complejas. Por ejemplo, un operador de definición:= podría ser de tipo (:=) :: Variable -> Expression -> Definitiony no debería ser posible pasar una expresión compleja como su parámetro del lado izquierdo (aunque debería ser posible pasar una variable como su parámetro del lado derecho, sin conversión explícita ) .
2. Tenga una instancia de expresiones Num, de modo que sea posible promover literales enteros a expresiones y usar una notación conveniente para operaciones algebraicas comunes como la suma o la multiplicación sin introducir algunos operadores auxiliares de envoltura.

En otras palabras, me gustaría tener un tipo de conversión implícita y estática (coerción) de variables a expresiones. Ahora, sé que, como tal, no hay tipos implícitos en Haskell. Sin embargo, ciertos conceptos de programación orientada a objetos (herencia simple, en este caso) se pueden expresar en el sistema de tipos de Haskell, con o sin extensiones de lenguaje. ¿Cómo podría satisfacer los dos puntos anteriores manteniendo una sintaxis ligera? ¿Es posible?

Discusión

Está claro que el principal problema aquí es Numla restricción de tipo, por ejemplo

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

En principio, es posible escribir un solo tipo de datos algebraicos (generalizados) para variables y expresiones. Entonces, se podría escribir :=de tal manera, que la expresión del lado izquierdo se discrimina y solo se acepta un constructor de variables, de lo contrario, con un error de tiempo de ejecución. Sin embargo, esa no es una solución limpia y estática (es decir, tiempo de compilación) ...

Ejemplo

Idealmente, me gustaría lograr una sintaxis ligera como

computation = do
  x <- variable
  t <- variable

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

En particular, quiero prohibir la notación como t + 1 |:=| x^2 - 1ya que :=debería dar una definición de una variable y no una expresión completa del lado izquierdo.

Para aprovechar el polimorfismo en lugar de subtipar (porque eso es todo lo que tiene en Haskell), no piense que "una variable es una expresión", sino que "ambas variables y expresiones tienen algunas operaciones en común". Esas operaciones se pueden poner en una clase de tipo:

class HasVar e where fromVar :: Variable -> e

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

Luego, en lugar de lanzar cosas, haga las cosas polimórficas. Si es así v :: forall e. HasVar e => e, se puede usar como expresión y como 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

Esqueleto para hacer que el siguiente código escriba: https://gist.github.com/Lysxia/da30abac357deb7981412f1faf0d2103

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