From 10301084f50ec685082c959c9010b84a93c83bd9 Mon Sep 17 00:00:00 2001
From: 4ever2 <3417013+4ever2@users.noreply.github.com>
Date: Mon, 31 Mar 2025 12:04:38 +0200
Subject: [PATCH] Compile function parameter types to TInd instead of TConst

---
 src/Agda2Lambox/Compile/Type.hs | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Agda2Lambox/Compile/Type.hs b/src/Agda2Lambox/Compile/Type.hs
index a649cab..42d6ff8 100644
--- a/src/Agda2Lambox/Compile/Type.hs
+++ b/src/Agda2Lambox/Compile/Type.hs
@@ -22,7 +22,7 @@ import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Utils.Monad (ifM)
 
 import qualified LambdaBox as LBox
-import Agda2Lambox.Compile.Utils ( qnameToKName, isLogical )
+import Agda2Lambox.Compile.Utils ( qnameToKName, isLogical, toInductive )
 import Agda2Lambox.Compile.Monad
 import Agda.Compiler.Backend (HasConstInfo(getConstInfo), Definition(Defn), AddContext (addContext))
 import Agda.Utils (isDataOrRecDef, getInductiveParams, isArity, maybeUnfoldCopy)
@@ -142,8 +142,9 @@ compileTypeTerm = \case
     if isLogicalDef then pure ([], LBox.TBox)
 
     -- if it's an inductive, we only apply the parameters
-    else if isDataOrRecDef def then
-      ([],) . foldl' LBox.TApp (LBox.TConst $ qnameToKName q) 
+    else if isDataOrRecDef def then do
+      ind <- liftTCM $ toInductive q
+      ([],) . foldl' LBox.TApp (LBox.TInd ind)
         <$> compileElims (take (getInductiveParams def) es)
 
     -- TODO: check if it is a type alias