[ cubical ] re HCompU: dealing with possibly missing prims

4 files changed, 10 insertions, 7 deletions

diff --git a/src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda b/src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda
index 2d9fd1f..410f71e 100644
--- a/src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda
+++ b/src/data/lib/prim/Agda/Builtin/Cubical/Glue.agda
@@ -64,8 +64,6 @@ primitive
       → {T : Partial φ (Set ℓ')} → {e : PartialP φ (λ o → T o ≃ A)}
       → primGlue A T e → A
 
-    -- Needed for transp in Glue.
-    primFaceForall : (I → I) → I
 
 
 module _ {ℓ : I → Level} (P : (i : I) → Set (ℓ i)) where
diff --git a/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda b/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda
index b46cffa..d960ef4 100644
--- a/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda
+++ b/src/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda
@@ -60,6 +60,8 @@ primitive
   prim^unglueU : {la : Level} {φ : I} {T : I → Partial φ (Set la)}
                    {A : Set la [ φ ↦ T i0 ]} →
                    hcomp T (outS A) → outS A
+  -- Needed for transp.
+  primFaceForall : (I → I) → I
 
 transpProof : ∀ {l} → (e : I → Set l) → (φ : I) → (a : Partial φ (e i0)) → (b : e i1 [ φ ↦ (\ o → transp e i0 (a o)) ] ) → fiber (transp e i0) (outS b)
 transpProof e φ a b = f , \ j → comp e (\ i → \ { (φ = i1) → transp (\ j → e (j ∧ i)) (~ i) (a 1=1)
diff --git a/src/full/Agda/TypeChecking/Conversion.hs b/src/full/Agda/TypeChecking/Conversion.hs
index 8587fee..7e6520c 100644
--- a/src/full/Agda/TypeChecking/Conversion.hs
+++ b/src/full/Agda/TypeChecking/Conversion.hs
@@ -341,6 +341,8 @@ compareTerm' cmp a m n =
        mGlue  <- getPrimitiveName' builtinGlue
        mHComp <- getPrimitiveName' builtinHComp
        mSub   <- getBuiltinName' builtinSub
+       mUnglueU <- getPrimitiveTerm' builtin_unglueU
+       mSubIn   <- getPrimitiveTerm' builtinSubIn
        case ty of
          Def q es | Just q == mIsOne -> return ()
          Def q es | Just q == mGlue, Just args@(l:_:a:phi:_) <- allApplyElims es -> do
@@ -351,11 +353,11 @@ compareTerm' cmp a m n =
               compareTermOnFace cmp (unArg phi) ty m n
               compareTerm cmp ty (mkUnglue m) (mkUnglue n)
          Def q es | Just q == mHComp, Just (sl:s:args@[phi,u,u0]) <- allApplyElims es
-                  , Sort (Type lvl) <- unArg s -> do
+                  , Sort (Type lvl) <- unArg s
+                  , Just unglueU <- mUnglueU, Just subIn <- mSubIn
+                  -> do
               let l = Level lvl
               ty <- el' (pure $ l) (pure $ unArg u0)
-              unglueU <- prim_unglueU
-              subIn <- primSubIn
               let bA = subIn `apply` [sl,s,phi,u0]
               let mkUnglue m = apply unglueU $ [argH l] ++ map (setHiding Hidden) [phi,u]  ++ [argH bA,argN m]
               reportSDoc "conv.hcompU" 20 $ prettyTCM (ty,mkUnglue m,mkUnglue n)
diff --git a/src/full/Agda/Utils/Impossible.hs b/src/full/Agda/Utils/Impossible.hs
index f256912..3b01991 100644
--- a/src/full/Agda/Utils/Impossible.hs
+++ b/src/full/Agda/Utils/Impossible.hs
@@ -38,8 +38,9 @@ instance Show Impossible where
     , "Location of the error: " ++ file ++ ":" ++ show line
     ]
   show (ImpMissingDefinitions needed forthis) = unlines
-    [ "The following builtins or primitives need to be bound to use " ++ forthis ++ ":"]
-    ++ unwords needed
+    [ "The following builtins or primitives need to be bound to use " ++ forthis ++ ":"
+    , unwords needed
+    ]
 
 instance Exception Impossible