From d9ed763acec45d3c0c064341ffe04101a5461231 Mon Sep 17 00:00:00 2001
From: Eve <phanta@phanta.pl>
Date: Sun, 26 Jan 2025 01:13:58 +0100
Subject: [PATCH] Fix tcApp on pi types, split check/infer into variants inside
 and outside EvalM

---
 .../api/GF/Compile/TypeCheck/ConcreteNew.hs         | 13 +++++++++----
 src/compiler/api/GF/Term.hs                         |  2 +-
 2 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
index a314aed49..345326d7e 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE RankNTypes, CPP #-}
-module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where
+module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where
 
 -- The code here is based on the paper:
 -- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich.
@@ -24,14 +24,20 @@ import Data.Maybe(fromMaybe,isNothing)
 import qualified Control.Monad.Fail as Fail
 
 checkLType :: Globals -> Term -> Type -> Check (Term, Type)
-checkLType globals t ty = runEvalOneM globals $ do
+checkLType globals t ty = runEvalOneM globals (checkLType' t ty)
+
+checkLType' :: Term -> Type -> EvalM s (Term, Type)
+checkLType' t ty = do
   vty <- eval [] ty []
   (t,_) <- tcRho [] t (Just vty)
   t <- zonkTerm [] t
   return (t,ty)
 
 inferLType :: Globals -> Term -> Check (Term, Type)
-inferLType globals t = runEvalOneM globals $ do
+inferLType globals t = runEvalOneM globals (inferLType' t)
+
+inferLType' :: Term -> EvalM s (Term, Type)
+inferLType' t = do
   (t,ty) <- inferSigma [] t
   t  <- zonkTerm [] t
   ty <- value2term False [] ty
@@ -105,7 +111,6 @@ tcRho scope (Abs bt var body) Nothing = do                   -- ABS1
                              v2 <- eval ((x,tnk):env) t []
                              check m (n+1) (b,x:xs) v2
         v2             -> check m n st v2
-      check m (n+1) (b,x:xs) v2
     check m n st (VRecType as)     = foldM (\st (l,v) -> check m n st v) st as
     check m n st (VR as)           =
       foldM (\st (lbl,tnk) -> follow m n st tnk) st as
diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs
index d9ffc9538..410360ea8 100644
--- a/src/compiler/api/GF/Term.hs
+++ b/src/compiler/api/GF/Term.hs
@@ -2,7 +2,7 @@ module GF.Term (renameSourceTerm,
                 Globals(..), ConstValue(..), EvalM, stdPredef,
                 Value(..), showValue, Thunk, newThunk, newEvaluatedThunk,
                 evalError, evalWarn,
-                inferLType, checkLType,
+                inferLType, inferLType', checkLType, checkLType',
                 normalForm, normalFlatForm, normalStringForm,
                 unsafeIOToEvalM, force
                ) where