From c3780abfd1c2a3c5ddaef2bcc9d45b12d1879da8 Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Fri, 28 Jan 2022 14:17:10 +0100
Subject: [PATCH] fix issue with let after switching to generation/solver model

---
 src/TC.hs | 19 ++++++++++++++++---
 tst       |  7 ++++++-
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/src/TC.hs b/src/TC.hs
index 62d1fb5..5c9e687 100644
--- a/src/TC.hs
+++ b/src/TC.hs
@@ -14,11 +14,15 @@ import qualified Data.Text as T
 
 import Type
 import Misc
+import Solve
 
 import Prelude hiding (map)
 
 runInfer :: TypeEnv -> Infer a -> Either TypeError (a, [Id], [Constraint])
-runInfer r = runIdentity . runExceptT . (\i -> runRWST i r initialState) . getInfer
+runInfer = runInfer' initialState
+
+runInfer' :: [Id] -> TypeEnv ->  Infer a -> Either TypeError (a, [Id], [Constraint])
+runInfer' s r = runIdentity . runExceptT . (\i -> runRWST i r s) . getInfer
 
 localEnv :: Id -> PolyT -> Infer a -> Infer a
 localEnv i t = local (M.insert i t)
@@ -65,8 +69,17 @@ infer = \case
 
     Let _ [] e            -> infer e
     Let p ((i,e1):ies) e2 -> do
-      t1 <- generalize =<< infer e1
-      localEnv i t1 (infer (Let p ies e2))
+      env <- ask
+      state <- get
+      case runInfer' state env (infer e1) of
+        Left err -> throwError err
+        Right (mt,st,cs) -> case runSolve (emptySubst, cs) of
+            Left err -> throwError err
+            Right su -> do
+              put st
+              local (apply su) $ do
+                pt <- generalize (apply su mt)
+                localEnv i pt (infer (Let p ies e2)) -- should (apply su ies) be used?
 
     Abs _ [] e     -> infer e
     Abs p (i:is) e -> do
diff --git a/tst b/tst
index aa19a4e..908476f 100644
--- a/tst
+++ b/tst
@@ -1 +1,6 @@
-λf g x y z w. f w (g x y z)
+-- λf g x y z w. f w (g x y z)
+let flip  := λf x y. f y x
+    comp  := λf g x. f (g x)
+    const := λx y. x
+    id    := (flip const) comp
+ in id