An implementation of McBride's structural first-order unification algorithm in Haskell. Tested on GHC 8.4.4

Unification.hs

{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE TypeInType , ScopedTypeVariables , TypeFamilies, TypeOperators #-} 
{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE Safe #-}

module Unification where

import Data.Kind
import Prelude hiding ((++))

data Nat = Z | S Nat deriving (Show, Read, Eq)

data Natty :: Nat -> Type where
  Zy :: Natty Z
  Sy :: Natty n -> Natty (S n)

deriving instance Show (Natty n)

type family (+) (n :: Nat) (m :: Nat) :: Nat where
  Z   + m = m
  S n + m = S (n + m)

data Fin :: Nat -> Type where
  FZ :: Fin (S n)
  FS :: Fin n -> Fin (S n)

deriving instance Show (Fin n)

data Term :: Nat -> Type where
  Var  :: Fin n -> Term n
  Leaf :: Term n
  Fork :: Term n -> Term n -> Term n

deriving instance Show (Term n)

(<|) :: (Fin m -> Term n) -> Term m -> Term n
f <| (Var x)      = f x
f <| Leaf         = Leaf
f <| (s `Fork` t) = (f <| s) `Fork` (f <| t)

so :: (Fin m -> Term n) -> (Fin l -> Term m) -> Fin l -> Term n
f `so` g = (f <|) . g

thin :: Fin (S n) -> Fin n -> Fin (S n)
thin FZ     y         = FS y
thin (FS x) FZ     = FZ 
thin (FS x) (FS y) = FS (thin x y)

thick :: forall n. Fin (S n) -> Fin (S n) -> Maybe (Fin n)
thick FZ FZ     = Nothing 
thick FZ (FS y) = Just y
thick (FS FZ) FZ     = Just FZ
thick (FS (FS _)) FZ = Just FZ
thick (FS FZ) (FS y)       = FS <$> thick FZ y
thick (FS x@(FS _)) (FS y) = FS <$> thick x y

check :: Fin (S n) -> Term (S n) -> Maybe (Term n)
check x (Var y) = Var <$> thick x y
check x Leaf    = Just Leaf
check x (s `Fork` t) = Fork <$> check x s <*> check x t 

for :: Term n -> Fin (S n) -> Fin (S n) -> Term n
(t' `for` x) y = case thick x y of
  Just y' -> Var y'
  Nothing -> t'

data AList :: Nat -> Nat -> Type where
  ANil  :: AList n n
  ASnoc :: AList m n -> Term m -> Fin (S m) -> AList (S m) n

sub :: AList m n -> Fin m -> Term n
sub ANil           = Var
sub (ASnoc s t' x) = sub s `so` (t' `for` x)

(++) :: AList m n -> AList l m -> AList l n
s ++ ANil           = s
s ++ (ASnoc s' t x) = (s ++ s') `ASnoc` t $ x

data Ex (t :: Nat -> Type) where
  Ex :: Natty m -> t m -> Ex t

asnoc :: Ex (AList m) -> Term m -> Fin (S m) -> Ex (AList (S m))
asnoc (Ex n s) t' x = Ex n (ASnoc s t' x)

mgu :: Natty m -> Term m -> Term m -> Maybe (Ex (AList m)) 
mgu m s t = amgu s t (Ex m ANil)

amgu :: Term m -> Term m -> Ex (AList m) -> Maybe (Ex (AList m))
amgu Leaf Leaf           acc = Just acc
amgu Leaf (t1 `Fork` t2) acc = Nothing
amgu (s1 `Fork` s2) Leaf acc = Nothing 
amgu (s1 `Fork` s2) (t1 `Fork` t2) acc = do
  acc' <- amgu s1 t1 acc
  amgu t1 t2 acc'
amgu (Var x) (Var y) (Ex m ANil) = Just (flexFlex m x y)
amgu (Var x) t (Ex m ANil) = flexRigid m x t 
amgu t (Var x) (Ex m ANil) = flexRigid m x t
amgu s       t (Ex n (ASnoc sig r z)) = do
  (Ex n sig) <- amgu (r `for` z <| s) (r `for` z <| t) (Ex n sig)
  return (Ex n (ASnoc sig r z))

flexFlex :: Natty m -> Fin m -> Fin m -> Ex (AList m)
flexFlex (Sy m) x y = case thick x y of 
                      Just y' -> Ex m (ASnoc ANil (Var y') x)
                      Nothing -> Ex (Sy m) ANil

flexRigid :: Natty m -> Fin m -> Term m -> Maybe (Ex (AList m))
flexRigid (Sy m) x t = case check x t of 
                       Just t' -> Just (Ex m (ASnoc ANil t' x))
                       Nothing -> Nothing

Hell yeah just flexing. Y’all doing ok