diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs
index 85474e57a..bef693fa6 100644
--- a/rzk/src/Rzk/Main.hs
+++ b/rzk/src/Rzk/Main.hs
@@ -89,7 +89,7 @@ parseRzkFilesOrStdin = \case
 typecheckString :: String -> Either String String
 typecheckString moduleString = do
   rzkModule <- Rzk.parseModule moduleString
-  case defaultTypeCheck (typecheckModule Nothing rzkModule) of
+  case defaultTypeCheck (typecheckModules [rzkModule]) of
     Left err -> Left $ unlines
       [ "An error occurred when typechecking!"
       , "Rendering type error... (this may take a few seconds)"
diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs
index 2792bec4d..d3acc07e4 100644
--- a/rzk/src/Rzk/TypeCheck.hs
+++ b/rzk/src/Rzk/TypeCheck.hs
@@ -88,12 +88,12 @@ typecheckModules = \case
   [] -> return []
   m : ms -> do
     (decls, errs) <- typecheckModule Nothing m
-    if null errs
-      then
+    case errs of
+      err : _ -> do
+        throwError err
+      _ -> do
         localDeclsPrepared decls $
           (decls <>) <$> typecheckModules ms
-      else
-        return decls
 
 typecheckModuleWithLocation :: (FilePath, Rzk.Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
 typecheckModuleWithLocation (path, module_) = do
@@ -1938,14 +1938,23 @@ unifyInCurrentContext mterm expected actual = performing action $
                     switchVariance $  -- unifying in the negative position!
                       unifyTerms cube cube' -- FIXME: unifyCubes
                     enterScope orig' cube $ do
-                      case (mtope, mtope') of
-                        (Just tope, Just tope') -> do
-                          topeNF <- nfT tope
-                          topeNF' <- nfT tope'
-                          unifyTopes topeNF topeNF'
-                        (Nothing, Nothing)      -> return ()
-                        (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
-                        (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
+                      case ret' of
+                        -- UniverseTopeT{} ->
+                        --   (Just tope, Just tope') -> do
+                        --     topeNF <- nfT tope
+                        --     topeNF' <- nfT tope'
+                        --     unifyTopes topeNF topeNF'
+                        --   (Nothing, Nothing)      -> return ()
+                        --   (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
+                        --   (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
+                        _ -> case (mtope, mtope') of
+                          (Just tope, Just tope') -> do
+                            topeNF <- nfT tope
+                            topeNF' <- nfT tope'
+                            unifyTopes topeNF topeNF'
+                          (Nothing, Nothing)      -> return ()
+                          (Just tope, Nothing)    -> nfT tope >>= (`unifyTopes` topeTopT)
+                          (Nothing, Just tope)    -> nfT tope >>= unifyTopes topeTopT
                       case mterm of
                         Nothing -> unifyTerms ret ret'
                         Just term -> unifyTypes (appT ret' (S <$> term) (Pure Z)) ret ret'