subst in result type of let in inference mode

sweirich · Jun 29, 2022 · 5f20e2a · 5f20e2a
1 parent 47a07a5
commit 5f20e2a
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 12 deletions.
diff --git a/full/src/TypeCheck.hs b/full/src/TypeCheck.hs
@@ -135,9 +135,9 @@ tcTerm (Let rhs bnd) mty = do
   aty <- inferType rhs 
   ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $
       tcTerm body mty
-  when (x `elem` Unbound.toListOf Unbound.fv ty) $
-    Env.err [DS "Let bound variable", DD x, DS "escapes in type", DD ty]
-  return ty
+  case mty of 
+    Just _ -> return ty
+    Nothing -> return $ Unbound.subst x rhs ty
 
 -- Type constructor application
 tcTerm (TCon c params) Nothing = do

diff --git a/main/src/TypeCheck.hs b/main/src/TypeCheck.hs
@@ -150,9 +150,9 @@ tcTerm (Let rhs bnd) mty = {- SOLN HW -} do
   aty <- inferType rhs 
   ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $
       tcTerm body mty
-  when (x `elem` Unbound.toListOf Unbound.fv ty) $
-    Env.err [DS "Let bound variable", DD x, DS "escapes in type", DD ty]
-  return ty
+  case mty of 
+    Just _ -> return ty
+    Nothing -> return $ Unbound.subst x rhs ty
 {- STUBWITH   Env.err [DS "unimplemented"] -}
 {- SOLN DATA -}
 -- Type constructor application

diff --git a/version2/src/TypeCheck.hs b/version2/src/TypeCheck.hs
@@ -124,9 +124,9 @@ tcTerm (Let rhs bnd) mty = do
   aty <- inferType rhs 
   ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $
       tcTerm body mty
-  when (x `elem` Unbound.toListOf Unbound.fv ty) $
-    Env.err [DS "Let bound variable", DD x, DS "escapes in type", DD ty]
-  return ty
+  case mty of 
+    Just _ -> return ty
+    Nothing -> return $ Unbound.subst x rhs ty
 
 
 

diff --git a/version3/src/TypeCheck.hs b/version3/src/TypeCheck.hs
@@ -133,9 +133,9 @@ tcTerm (Let rhs bnd) mty = do
   aty <- inferType rhs 
   ty <- Env.extendCtxs [mkSig x aty, Def x rhs] $
       tcTerm body mty
-  when (x `elem` Unbound.toListOf Unbound.fv ty) $
-    Env.err [DS "Let bound variable", DD x, DS "escapes in type", DD ty]
-  return ty
+  case mty of 
+    Just _ -> return ty
+    Nothing -> return $ Unbound.subst x rhs ty