fix translation of pi

jespercockx · Jan 17, 2024 · b4d42a9 · b4d42a9
1 parent e4dfeb5
commit b4d42a9
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/app/Agda/Core/ToCore.hs b/app/Agda/Core/ToCore.hs
@@ -122,10 +122,11 @@ instance ToCore I.Term where
 
   toCore I.Con{} = throwError "cubical endpoint application to constructors not supported"
 
-  toCore (I.Pi dom codom) = TPi <$> toCore dom <*> toCore codom
-        -- NOTE(flupe): we will need the sorts in the core syntax soon
-        -- <$> toCore (dom   .^ lensSort)
-        -- <*> toCore (codom .^ lensSort)
+  toCore (I.Pi dom codom) =
+    TPi <$> toCore (dom           ^. lensSort)
+        <*> toCore (absBody codom ^. lensSort)
+        <*> toCore dom
+        <*> toCore codom
 
   toCore (I.Sort s) = TSort <$> toCore s