Tried fixing bug. Failed.

src/TypeChecker/HM.hs

@@ -3,11 +3,11 @@
 {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
 {-# HLINT ignore "Use traverse_" #-}
 
-module TypeChecker.HM (typecheck) where
+module TypeChecker.HM  where
 
 import           Control.Monad.Except
 import           Control.Monad.State
-import           Data.Bifunctor        (second)
+import           Data.Bifunctor        (bimap, second)
 import           Data.Functor.Identity (Identity, runIdentity)
 import           Data.Map              (Map)
 import qualified Data.Map              as M
@@ -25,16 +25,14 @@ data Ctx = Ctx { constr :: Map Type Type
                , frsh   :: Char }
     deriving Show
 
-run :: Infer a -> Either String a
+run :: Infer a -> Either String (a, Ctx)
-run = runIdentity . runExceptT . flip evalStateT initC
+run = runIdentity . runExceptT . flip runStateT initC
-
-int = TMono "Int"
 
 initC :: Ctx
 initC = Ctx M.empty M.empty M.empty 'a'
 
 typecheck :: Program -> Either Error T.Program
-typecheck = run . inferPrg
+typecheck = undefined . run . inferPrg
 
 inferPrg :: Program -> Infer T.Program
 inferPrg (Program bs) = do
@@ -61,10 +59,8 @@ inferExp = \case
     EInt i -> return (int, T.EInt int i)
     EId i -> (\t -> (t, T.EId t i)) <$> lookupVar i
     EAdd e1 e2 -> do
-        (t1, e1') <- inferExp e1
+        insertSig "+" (TArr int (TArr int int))
-        (t2, e2') <- inferExp e2
+        inferExp (EApp (EApp (EId "+") e1) e2)
-        unless (isInt t1 && isInt t2) (throwError "Can not add non-ints")
-        return (int,T.EAdd int e1' e2')
     EApp e1 e2 -> do
         (t1, e1') <- inferExp e1
         (t2, e2') <- inferExp e2
@@ -77,13 +73,7 @@ inferExp = \case
         (ret_t,e') <- inferExp e
         t <- solveConstraints (TArr fr ret_t)
         return (t, T.EAbs t name e')
-    ELet name e1 e2 -> do
+    ELet name e1 e2 -> error "Let expression not implemented yet"
-        fr <- fresh
-        insertVar name fr
-        (t1, e1') <- inferExp e1
-        (t2, e2') <- inferExp e2
-        ret_t <- solveConstraints t1
-        return (ret_t, T.ELet ret_t name e1' e2')
 
 
 isInt :: Type -> Bool
@@ -112,6 +102,8 @@ fresh = do
     modify (\st -> st { frsh = succ chr })
     return $ TPol (Ident [chr])
 
+-- Constraint solving is wrong. (\x. x) 3 is inferred with the type 'a'
+
 addConstraint :: Type -> Type -> Infer ()
 addConstraint t1 t2 = do
     when (t2 `contains` t1) (throwError $ "Can't match type " ++ printTree t1 ++ " with " ++ printTree t2)
@@ -126,13 +118,16 @@ solveConstraints :: Type -> Infer Type
 solveConstraints t = do
     c <- gets constr
     v <- gets vars
-    subst t <$> solveAll (M.toList c)
+    xs <- solveAll (M.toList c)
+    modify (\st -> st { constr = M.fromList xs })
+    return $ subst t xs
 
 subst :: Type -> [(Type, Type)] -> Type
 subst t []                = t
 subst (TArr t1 t2) (x:xs) = subst (TArr (replace x t1) (replace x t2)) xs
 subst t (x:xs)            = subst (replace x t) xs
 
+-- Annoying fucking bug here
 solveAll :: [(Type, Type)] -> Infer [(Type, Type)]
 solveAll [] = return []
 solveAll (x:xs) = case x of
@@ -140,16 +135,37 @@ solveAll (x:xs) = case x of
     (TArr t1 t2, b)          -> fmap ((b, TArr t1 t2) :) $ solveAll $ solve (b, TArr t1 t2) xs
     (a, TArr t1 t2)          -> fmap ((a, TArr t1 t2) :) $ solveAll $ solve (a, TArr t1 t2) xs
     (TMono a, TPol b)        -> fmap ((TPol b, TMono a) :) $ solveAll $ solve (TPol b, TMono a) xs
-    (TPol a, TMono b)        -> fmap ((TPol a, TMono a) :) $ solveAll $ solve (TPol a, TMono b) xs
+    (TPol a, TMono b)        -> fmap ((TPol a, TMono b) :) $ solveAll $ solve (TPol a, TMono b) xs
     (TMono a, TMono b)       -> if a == b then solveAll xs else throwError "Can't unify types"
     (TPol a, TPol b)         -> fmap ((TPol a, TPol b) :) $ solveAll $ solve (TPol a, TPol b) xs
 
 solve :: (Type, Type) -> [(Type, Type)] -> [(Type, Type)]
-solve x = map (second (replace x))
+solve x = map (both (replace x))
 
 replace :: (Type, Type) -> Type -> Type
 replace a (TArr t1 t2) = TArr (replace a t1) (replace a t2)
 replace (a,b) c        = if a==c then b else c
 
+both :: (a -> b) -> (a,a) -> (b,b)
+both f = bimap f f
+
+int = TMono "Int"
+a = TPol "a"
+b = TPol "b"
+c = TPol "c"
+d = TPol "d"
+e = TPol "e"
+arr = TArr
+
+set = [(a, arr d e), (c, arr int d), (arr int (arr int int), arr b c)]
+
+prg = EAbs "f" (EAbs "x" (EApp (EId "f") (EAdd (EId "x") (EInt 1))))
+
+bug = EApp (EAbs "x" (EAdd (EAnn (EId "x") a) (EInt 3))) (EInt 2)
+
+-- (\x. \y. x + y + 1)
+prg2 = EApp (EAbs "x" (EId "x")) (EInt 1)
+
+--
 -- Known bugs
 -- (x : a) + 3 type checks

src/TypeChecker/HMIr.hs

@@ -20,7 +20,15 @@ data Exp
     | EApp Type Exp Exp
     | EAdd Type Exp Exp
     | EAbs Type Ident Exp
-      deriving (C.Eq, C.Ord, C.Show, C.Read)
+      deriving (C.Eq, C.Ord, C.Read)
+
+instance Show Exp where
+    show (EId t (Ident i))    = i ++ " : " ++ show t
+    show (EInt _ i)           = show i
+    show (ELet t i e1 e2)     = error "Show for let not implemented"
+    show (EApp t e1 e2)       = show e1 ++ " " ++ show e2 ++ " : " ++ show t
+    show (EAdd _ e1 e2)       = show e1 ++ " + " ++ show e2
+    show (EAbs t (Ident i) e) = "\\ " ++ i ++ ". " ++ show e ++ " : " ++ show t
 
 type Id = (Type, Ident)
 

test_program

@@ -1,4 +1,5 @@
-main : Mono Int ;
+id : Mono Int -> Mono Int ;
-main = let f = \x. x in f 5 ;
+id = \x. x ;
-
 
+main : Poly a ;
+main = id 3 ;