Typecheck.hs

import Data.Map (Map)
import qualified Data.Map as Map

import Data.Composition
import Data.Monoid

data Type
  = Type :$ Type
  | TVar Name
  | TConst Name Kind

data Kind = Star | Kind :-> Kind | KVar Name

type Name = String

type SubstitutionOf = Map Name

data TCError s = Cycle Name s | Distinct s s

class Substitutable s where
    unify :: s -> s -> Either (TCError s) (SubstitutionOf s)
    subst :: Name -> s -> s -> s
    occurs :: Name -> s -> Bool

massUnify :: Substitutable s => [(s, s)] -> Either (TCError s) (SubstitutionOf s)
massUnify [] = do
    return Map.empty

massUnify ((s, t) : rest) = do
    subs <- unify s t
    let rest' = Map.foldrWithKey' ((map . both) .: subst) rest subs
    others <- massUnify rest'
    return (subs <> others)

both f (a, b) = (f a, f b)

instance Substitutable Kind where
    unify (KVar k) other@(KVar k2)
        | k == k2        = Right (Map.empty)
        | otherwise      = Right (Map.singleton k other)

    unify (KVar k) other
        | occurs k other = Left (Cycle k other)
        | otherwise      = Right (Map.singleton k other)

    unify other (KVar k) = unify (KVar k) other

    unify (a :-> b) (c :-> d) = do
        s <- unify a c 
        u <- unify b d
        return (s <> u)

    unify Star Star = Right Map.empty

    subst name k src @ (KVar k1)
        | name == k1       = k
        | otherwise        = src
    subst name k (a :-> b) = subst name k a :-> subst name k b
    subst _    _  Star     = Star

    occurs name (KVar name1) = name == name1
    occurs name (a :-> b)    = occurs name a || occurs name b
    occurs _     Star        = False