diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs
index f76cc499..d98bbd4b 100644
--- a/src/Agda2Hs/Compile.hs
+++ b/src/Agda2Hs/Compile.hs
@@ -117,7 +117,8 @@ compile genv tlm _ def =
 
       case (p , theDef def) of
         (NoPragma            , _         ) -> return []
-        (ExistingClassPragma , _         ) -> return []
+        (ExistingPragma      , _         ) -> return []
+        (ExistingClassPragma , Record{}  ) -> return []
         (UnboxPragma s       , Record{}  ) -> [] <$ checkUnboxPragma def
         (TransparentPragma   , Function{}) -> [] <$ checkTransparentPragma def
         (InlinePragma        , Function{}) -> [] <$ checkInlinePragma def
diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs
index b228d0be..24fffec4 100644
--- a/src/Agda2Hs/Compile/Utils.hs
+++ b/src/Agda2Hs/Compile/Utils.hs
@@ -195,6 +195,7 @@ hasCompilePragma q = processPragma q <&> \case
   InlinePragma{} -> True
   DefaultPragma{} -> True
   ClassPragma{} -> True
+  ExistingPragma{} -> True
   ExistingClassPragma{} -> True
   UnboxPragma{} -> True
   TransparentPragma{} -> True
diff --git a/src/Agda2Hs/Pragma.hs b/src/Agda2Hs/Pragma.hs
index 1f6a5822..d8f42235 100644
--- a/src/Agda2Hs/Pragma.hs
+++ b/src/Agda2Hs/Pragma.hs
@@ -51,6 +51,7 @@ data ParsedPragma
   | InlinePragma
   | DefaultPragma [Hs.Deriving ()]
   | ClassPragma [String]
+  | ExistingPragma
   | ExistingClassPragma
   | UnboxPragma Strictness
   | TransparentPragma
@@ -89,6 +90,7 @@ processPragma qn = liftTCM (getUniqueCompilerPragma pragmaName qn) >>= \case
   Just (CompilerPragma r s)
     | "class" `isPrefixOf` s      -> return $ ClassPragma (words $ drop 5 s)
     | s == "inline"               -> return InlinePragma
+    | s == "existing"             -> return ExistingPragma
     | s == "existing-class"       -> return ExistingClassPragma
     | s == "unboxed"              -> return $ UnboxPragma Lazy
     | s == "unboxed-strict"       -> return $ UnboxPragma Strict