fix bug in unification

[fp.git] / src / HM.hs

diff --git a/src/HM.hs b/src/HM.hs
index 9c4aa76..9591706 100644 (file)
--- a/src/HM.hs
+++ b/src/HM.hs
@@ -16,7 +16,6 @@ module HM
   , TypedTerm(..)
     -- * Type inference
   , algW
   , TypedTerm(..)
     -- * Type inference
   , algW

-  , runTI

   ) where
 
 import Control.Monad.Except
   ) where
 
 import Control.Monad.Except


@@ -87,18 +86,25 @@ unify (TypeVar a) t = varBind a t
 unify t (TypeVar a) = varBind a t
 unify (TypeFunction a b) (TypeFunction a' b') = do
   s1 <- unify a a'
 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
 
   return $ s1 `composeSub` s2
 unify (Primitive a) (Primitive b) | a == b = return idSub
 unify a b = fail $ "cannot unify " ++ show a ++ " with " ++ show b
 

+tiLit :: Literal -> TI (Substitution, Type)
+tiLit (LBool _) = return (idSub, Primitive "Bool")
+tiLit (LInt _) = return (idSub, Primitive "Integer")
+tiLit (LFunc If) = do
+  a <- newVar
+  return (idSub, Primitive "Bool" `TypeFunction` (a `TypeFunction` (a `TypeFunction` a)))
+

 ti :: TypeEnv -> TypedTerm -> TI (Substitution, Type)
 ti :: TypeEnv -> TypedTerm -> TI (Substitution, Type)

---ti _ (TTerm (Var v) (TScheme t@(Primitive _))) = return (idSub, t)

 ti e (TTerm tr sch) = do
   (s, t) <- ti e (NTTerm tr)
   sch' <- instantiate sch
   s' <- unify t sch'
   return (s', substituteT s' sch')
 ti e (TTerm tr sch) = do
   (s, t) <- ti e (NTTerm tr)
   sch' <- instantiate sch
   s' <- unify t sch'
   return (s', substituteT s' sch')

+ti _ (NTTerm (Lit l)) = tiLit l

 ti e (NTTerm (Var v)) = case Map.lookup v e of
   Nothing -> fail $ "unbound variable: " ++ v
   Just sigma -> do
 ti e (NTTerm (Var v)) = case Map.lookup v e of
   Nothing -> fail $ "unbound variable: " ++ v
   Just sigma -> do


@@ -121,9 +127,8 @@ ti e (NTTerm (Let x a b)) = do
       e' = Map.insert x t' e
   (s2, t2) <- ti (Map.map (substituteS s1) e') b
   return (s1 `composeSub` s2, t2)
       e' = Map.insert x t' e
   (s2, t2) <- ti (Map.map (substituteS s1) e') b
   return (s1 `composeSub` s2, t2)

-  

  
  

-algW :: TypedTerm -> TI Type
-algW t = do
+algW :: TypedTerm -> Either String Type
+algW t = fst . runTI $ do

   (s, u) <- ti Map.empty t
   return $ substituteT s u
   (s, u) <- ti Map.empty t
   return $ substituteT s u