# Unification for `unbound-generics`
This package implements (first-order) unification by reusing the framework of [`unbound-generics`](https://hackage.haskell.org/package/unbound-generics).
To use it, declare your data types as usual, including the generically-derived instances for alpha-equivalence (`Alpha`) and substitution (`Subst`) from `unbound-generics`.
In addition to those, ask for a new instance of `Unify` with the same arguments as `Subst`, that is, the type from which we build variables, and the type we want to unify.
The packages provides a function `unify` which works on a `Unification` monad. This monad is parametrized by the type we draw variables from. That means you can have as many types as you want, but there should be a single type of variables. In many cases the compiler fails to infer that argument to the `Unification` monad, so we recommend enabling `TypeApplications` for that matter.
The result of `unify` is either a single value which is an instance of both arguments, or a `UnificationError`. That error explains where the process has failed by a `Path` consisting of constructor, fields, and indices; and a cause.
---
This is an example in which `Type` is the one we draw variables from. Since we also use `TypeConstructor` inside the `TyCon` constructor, we also need to "request" to derive `Unify Type TypeConstructor`.
```haskell
type TypeVar = Name Type
data Type = TyVar { var :: TypeVar }
| TyFun { args :: [Type], ret :: Type }
| TyCon { con :: TypeConstructor, args :: [Type] }
deriving (Eq, Show, Generic, Typeable)
data TypeConstructor = TyConInt | TyConBool deriving (Eq, Show, Generic)
pattern TyInt, TyBool :: Type
pattern TyInt = TyCon TyConInt []
pattern TyBool = TyCon TyConBool []
instance Alpha Type
instance Alpha TypeConstructor
instance Subst Type Type where
isvar (TyVar v) = Just $ SubstName v
isvar _ = Nothing
instance Subst Type TypeConstructor
instance Unify Type Type
instance Unify Type TypeConstructor
```
Here are some example runs, using the explicitly-typed version of `runUnification` to declare that we are using `Type`-variables. To create new variables we use the usual `s2n` function from `unbound-generics`.
```haskell
>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyVar x] (TyVar x))
( Right (TyFun {args = [TyCon {con = TyConInt, args = []}], ret = TyCon {con = TyConInt, args = []}})
, fromList [(x,TyCon {con = TyConInt, args = []})] )
>>> runUnification @Type $ let x = s2n "x" in unify' (TyFun [TyVar x] TyInt) (TyFun [TyBool] (TyVar x))
( Left ([PathConstructor "TyFun", PathSelector "ret", PathConstructor "TyCon", PathSelector "con"], DifferentConstructor)
, fromList [(x,TyCon {con = TyConBool, args = []})] )
```