From 028685cef60b5d32e42a0951856e78f39165635a Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown01@ed.ac.uk>
Date: Sat, 7 Jan 2023 23:42:14 +0000
Subject: Correct typing of container extensions.

---
 src/Obs/NormalForm/Normalise.idr | 21 ++++++++++++++-------
 1 file changed, 14 insertions(+), 7 deletions(-)

(limited to 'src/Obs/NormalForm/Normalise.idr')

diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index e36e57c..a95e725 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -251,8 +251,6 @@ doSem {container, predSort, pred, arg} = do
   let shapeVar = Nothing
   let positionVar = Nothing
 
-  let inputDomain = MkDecl inputVar container.input
-
   shape <- doShape {inputRel = relevance container.inputSort, arg}
   let shape = Sorted.weaken [_] shape
 
@@ -286,11 +284,10 @@ doSem {container, predSort, pred, arg} = do
   let f = add (LogNormalForm' ann) (Left $ pure next) (Right . There . There . There)
   codomain <- subst' pred f
 
-  pure $ Cnstr $ Pi
-    { domainSort = container.inputSort
-    , codomainSort = max container.shapeSort (container.positionSort ~> predSort)
-    , domain = inputDomain
-    , codomain = Cnstr $ Sigma
+  pure $ MkLambda
+    { var = inputVar
+    , domainRel = relevance container.inputSort
+    , body = Cnstr $ Sigma
       { indexSort = container.shapeSort
       , elementSort = container.positionSort ~> predSort
       , index = shapeIndex
@@ -903,3 +900,13 @@ containerNextType container shape position =
         }
       }
     }
+
+export
+containerSemType : (container : ContainerTy ctx) -> (predSort : Universe) -> TypeNormalForm ctx
+containerSemType container predSort =
+  Cnstr $ Pi
+    { domainSort = container.inputSort
+    , codomainSort = succ (max container.shapeSort (container.positionSort ~> predSort))
+    , domain = MkDecl Nothing container.input
+    , codomain = cast $ max container.shapeSort (container.positionSort ~> predSort)
+    }
-- 
cgit v1.2.3