Correct typing of container extensions.

1 files changed, 14 insertions, 7 deletions

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)
+    }