varBind :: TypeVarName -> Type -> TI Substitution
varBind v t | t == TypeVar v = return idSub
- | v `Set.member` freeVarsT t = fail $ "occur check failed: " ++ v ++ " in " ++ show t
+ | v `Set.member` freeVarsT t = fail $ "occur check failed: " ++ v ++ " ~ " ++ show t
| otherwise = return $ Map.singleton v t
instantiate :: TypeScheme -> TI Type
unify t (TypeVar a) = varBind a t
unify (TypeFunction a b) (TypeFunction a' b') = do
s1 <- unify a a'
- s2 <- unify b b'
+ s2 <- unify (substituteT s1 b) (substituteT s1 b')
return $ s1 `composeSub` s2
unify (Primitive a) (Primitive b) | a == b = return idSub
unify a b = fail $ "cannot unify " ++ show a ++ " with " ++ show b
e' = Map.insert x t' e
(s2, t2) <- ti (Map.map (substituteS s1) e') b
return (s1 `composeSub` s2, t2)
-
algW :: TypedTerm -> Either String Type
algW t = fst . runTI $ do