Forward allowTC state in lambda body

Co-authored-by: Niki Vazou <niki.vazou@imdea.org>
AlecsFerra · Dec 13, 2024 · 221f527 · 221f527
1 parent b83678e
commit 221f527
Showing 1 changed file with 3 additions and 5 deletions.
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs
@@ -289,11 +289,9 @@ coreToLg allowTC (C.Cast e c)          = do (s, t) <- coerceToLg c
                                             return (ECoerc s t e')
 -- elaboration reuses coretologic
 -- TODO: fix this
-coreToLg _    (C.Lam x e) = do p     <- coreToLg True e
-                               tce   <- lsEmb <$> getState
-                               return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
--- coreToLg _ e@(C.Lam _ _)        = throw ("Cannot transform lambda abstraction to Logic:\t" ++ GM.showPpr e ++
---                                             "\n\n Try using a helper function to remove the lambda.")
+coreToLg allowTC    (C.Lam x e) = do p     <- coreToLg allowTC e
+                                     tce   <- lsEmb <$> getState
+                                     return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
 coreToLg _ e                     = throw ("Cannot transform to Logic:\t" ++ GM.showPpr e)