https://stackoverflow.com/questions/60600587/implicit-static-type-cast-coercion-in-haskell

E.hs

{-# LANGUAGE RankNTypes #-}

module E where

data Variable
data Expression

class HasVar e where
  fromVar :: Variable -> e

instance HasVar Variable
instance HasVar Expression

instance Num Expression

data Solver a

instance Functor Solver
instance Applicative Solver
instance Monad Solver

newtype V = V (forall e. HasVar e => e)

variable :: Solver V
variable = undefined

data Definition = (:=) Variable Expression

register :: Definition -> Solver ()
register = undefined

(|:=|) :: Variable -> Expression -> Solver ()
v |:=| e = register (v := e)

infix 1 :=, |:=|

data Equation

(|==|) :: Expression -> Expression -> Equation
(|==|) = undefined

solve :: Equation -> Solver ()
solve = undefined

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