From f58e2a6af1bc4e0443efc8975ce65d731b0d0cf1 Mon Sep 17 00:00:00 2001
From: Brent Yorgey <byorgey@gmail.com>
Date: Sat, 9 Sep 2023 12:08:34 -0500
Subject: [PATCH] also generalize local binds

---
 src/Swarm/Language/Typecheck.hs   | 9 ++-------
 test/unit/TestLanguagePipeline.hs | 3 +++
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/Swarm/Language/Typecheck.hs b/src/Swarm/Language/Typecheck.hs
index 1ffbaec84..954544325 100644
--- a/src/Swarm/Language/Typecheck.hs
+++ b/src/Swarm/Language/Typecheck.hs
@@ -680,14 +680,9 @@ infer s@(Syntax l t) = addLocToTypeErr l $ case t of
   SBind mx c1 c2 -> do
     c1' <- withFrame l TCBindL $ infer c1
     a <- decomposeCmdTy c1 (Actual, c1' ^. sType)
-    -- We do not need to generalize the type 'a' here (unlike
-    -- top-level binds) because a variable bound here (mx) can only
-    -- have local scope.  In other words, when we generalize at the
-    -- very end, the variable will no longer be in the context, so we
-    -- will be able to safely generalize over any unification
-    -- variables that occurred in its type.
+    genA <- generalize a
     c2' <-
-      maybe id ((`withBinding` Forall [] a) . lvVar) mx
+      maybe id ((`withBinding` genA) . lvVar) mx
         . withFrame l TCBindR
         $ infer c2
     _ <- decomposeCmdTy c2 (Actual, c2' ^. sType)
diff --git a/test/unit/TestLanguagePipeline.hs b/test/unit/TestLanguagePipeline.hs
index 94d1069d9..204e4b9a0 100644
--- a/test/unit/TestLanguagePipeline.hs
+++ b/test/unit/TestLanguagePipeline.hs
@@ -389,6 +389,9 @@ testLanguagePipeline =
         , testCase
             "top-level bind is polymorphic"
             (valid "f <- return (\\x.x); return (f 3, f \"hi\")")
+        , testCase
+            "local bind is polymorphic"
+            (valid "def foo : cmd (int * text) = f <- return (\\x.x); return (f 3, f \"hi\") end")
         ]
     ]
  where