fix issue with let after switching to generation/solver model

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

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