{-# LANGUAGE GADTs #-}

import Control.Applicative
import Data.Dynamic
import Data.Maybe

type Id = Integer

data Val where
  Var :: Id -> Val
  Val :: (Eq a, Typeable a, Show a) => a -> Val

instance Show Val where
  show (Var x) = "Var " ++ show x
  show (Val x) = show x

instance Eq Val where
  (Var x) == (Var y) = x == y
  (Val x) == (Val y) = fromMaybe False $ (==) x <$> cast y
  _ == _ = False

type Subst = [(Id, Val)]

val :: (Eq a, Typeable a, Show a) => a -> Val
val = Val

var :: Id -> Val
var = Var

gWalk :: Val -> Subst -> Val
gWalk (Var x) s =
    case lookup x s of
      Just v    -> gWalk v s
      otherwise -> var x
gWalk v _ = v

ts :: Subst
ts = [(4, var 2)
     ,(3, val True)
     ,(2, val "hello")
     ,(1, val $ Just "hi")]

gUnify :: Val -> Val -> Subst -> Maybe Subst
gUnify v w s =
    case (gWalk v s, gWalk w s) of
      (v        , w       ) | v == w -> Just s
      (v@(Var x), w       )          -> Just ((x,w):s)
      (v        ,w@(Var x))          -> Just ((x,v):s)
      _                              -> Nothing

tu = do let x = var 0
        s <- gUnify x (val "hello") []
        s' <- gUnify x (val True) s
        return s