From 68fe10afb4c685a090f3faa15fd267412b21576a Mon Sep 17 00:00:00 2001
From: Ewen Broudin-Caradec <Ewen Broudin-Caradec>
Date: Thu, 26 Sep 2024 11:22:57 +0200
Subject: [PATCH] Simplify typing rule for App

---
 src/Agda/Core/Typechecker.agda | 6 +++---
 src/Agda/Core/Typing.agda      | 3 +--
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Agda/Core/Typechecker.agda b/src/Agda/Core/Typechecker.agda
index bb4e188..d001fe5 100644
--- a/src/Agda/Core/Typechecker.agda
+++ b/src/Agda/Core/Typechecker.agda
@@ -101,10 +101,10 @@ inferApp ctx u v = do
   ⟨ x ⟩ (at , rt) ⟨ rtp ⟩ ← reduceToPi r (unType tu)
     "couldn't reduce term to a pi type"
   gtv ← checkType ctx v at
-  let sf = piSort (typeSort at) (typeSort rt)
+  let tytype = substTop r v rt
       gc = CRedL rtp CRefl
-      tytype = substTop r v rt
-  return (tytype , TyApp gtu gc gtv)
+      gtu' =  TyConv {b = El (typeSort tu) (TPi x at rt)} gtu gc
+  return (tytype , TyApp gtu' gtv)
 {-# COMPILE AGDA2HS inferApp #-}
 
 inferCase : ∀ {@0 cs} Γ d r u bs rt → TCM (Σ[ t ∈ Type α ] Γ ⊢ TCase {x = x} d r u bs rt ∶ t)
diff --git a/src/Agda/Core/Typing.agda b/src/Agda/Core/Typing.agda
index 782a02e..6fb119e 100644
--- a/src/Agda/Core/Typing.agda
+++ b/src/Agda/Core/Typing.agda
@@ -105,8 +105,7 @@ data TyTerm {α} Γ where
 
   TyApp
     : {b : Type α} {@0 r : Rezz α}
-    → Γ ⊢ u ∶ a
-    → (unType a) ≅ TPi x b c
+    → Γ ⊢ u ∶ El k (TPi x b c)
     → Γ ⊢ v ∶ b
     ------------------------------------
     → Γ ⊢ TApp u v ∶ substTop r v c