Use CustomBackendError instead of Generic(Doc)Error

Author: jespercockx

src/Agda2Hs/Compile.hs

@@ -106,7 +106,7 @@ compile opts tlm _ def =
         (DefaultPragma _     , Function{}) -> compileFun True def
         (DefaultPragma ds    , Record{}  ) -> pure <$> compileRecord (ToRecord False ds) def
 
-        _ -> genericDocError =<<  text "Don't know how to compile" <+> prettyTCM (defName def)
+        _ -> agda2hsErrorM $ text "Don't know how to compile" <+> prettyTCM (defName def)
 
     postCompile :: C ()
     postCompile = whenM (gets $ lcaseUsed >>> (> 0)) $ tellExtension Hs.LambdaCase
@@ -131,14 +131,14 @@ verifyOutput _ _ _ m ls = do
               Hs.RecDecl _ n _ -> n
           duplicateCons = filter ((> 1) . length) . group . sort  $ allCons
       when (length duplicateCons > 0) $
-        genericDocError =<< vcat (map (\x -> text $ "Cannot generate multiple constructors with the same identifier: " <> Hs.prettyPrint (headWithDefault __IMPOSSIBLE__ x)) duplicateCons)
+        agda2hsErrorM $ vcat (map (\x -> text $ "Cannot generate multiple constructors with the same identifier: " <> Hs.prettyPrint (headWithDefault __IMPOSSIBLE__ x)) duplicateCons)
 
     ensureNoOutputFromHsModules = unless (null $ concat $ map fst ls) $ do
       let hsModName = hsTopLevelModuleName m
       case hsModuleKind hsModName of
         HsModule -> do
           reportSDoc "agda2hs.compile" 10 $ text "Haskell module" <+> prettyTCM m <+> text "has non-null output."
-          genericDocError =<< hsep
+          agda2hsErrorM $ hsep
             (  pwords "The `Haskell.` namespace are reserved for binding existing Haskell modules, so the module"
             ++ [text "`" <> prettyTCM m <> text "`"]
             ++ pwords "should not contain any"

src/Agda2Hs/Compile/ClassInstance.hs

@@ -94,7 +94,7 @@ compileInstance ToDefinition def@Defn{..} =
           text "compileInstance compiled clauses: " :
           map (nest 2 . text . pp) ds
         when (length (nub rs) > 1) $
-          genericDocError =<< fsep (pwords "More than one minimal record used.")
+          agda2hsErrorM $ fsep (pwords "More than one minimal record used.")
         return $ Hs.InstDecl () Nothing ir (Just ds)
     where Function{..} = theDef
 
@@ -138,7 +138,7 @@ compileInstRule cs ty = do
 
 etaExpandClause :: Clause -> C [Clause]
 etaExpandClause cl@Clause{clauseBody = Nothing} =
-  genericError "Instance definition with absurd pattern!"
+  agda2hsError "Instance definition with absurd pattern!"
 etaExpandClause cl@Clause{namedClausePats = ps, clauseBody = Just t} = do
   case t of
     Con c _ _ -> do
@@ -147,7 +147,7 @@ etaExpandClause cl@Clause{namedClausePats = ps, clauseBody = Just t} = do
                       clauseBody      = Just $ t `applyE` [Proj ProjSystem $ unArg f] }
                 | f <- fields ]
       return cls
-    _ -> genericDocError =<< fsep (pwords $
+    _ -> agda2hsErrorM $ fsep (pwords $
       "Type class instances must be defined using copatterns (or top-level" ++
       " records) and cannot be defined using helper functions.")
 
@@ -221,9 +221,9 @@ compileInstanceClause' curModule ty (p:ps) c
     if
       -- Instance field: check canonicity.
       | isInstance arg -> do
-          unless (null ps) $ genericDocError =<< text "not allowed: explicitly giving superclass"
+          unless (null ps) $ agda2hsError "not allowed: explicitly giving superclass"
           body <- case clauseBody c' of
-            Nothing -> genericDocError =<< text "not allowed: absurd clause for superclass"
+            Nothing -> agda2hsError "not allowed: absurd clause for superclass"
             Just b  -> return b
           addContext (clauseTel c) $ do
             liftTCM $ setModuleCheckpoint curModule
@@ -257,7 +257,7 @@ compileInstanceClause' curModule ty (p:ps) c
        -- same (minimal) dictionary as the primitive fields.
       | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c'
       , n .~ q -> do
-        let err = genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
+        let err = agda2hsError $ "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`."
             filterArgs :: Type -> [Term] -> C [Term]
             filterArgs ty [] = return []
             filterArgs ty (v:vs) = do
@@ -308,7 +308,7 @@ fieldArgInfo f = do
     df : _ -> return $ getArgInfo df
     []     -> badness
   where
-    badness = genericDocError =<< text "Not a record field:" <+> prettyTCM f
+    badness = agda2hsErrorM $ text "Not a record field:" <+> prettyTCM f
 
 
 findDefinitions :: (QName -> Definition -> C Bool) -> ModuleName -> C [Definition]
@@ -326,7 +326,7 @@ resolveStringName s = do
   rname  <- liftTCM $ resolveName cqname
   case rname of
     DefinedName _ aname _ -> return $ anameName aname
-    _ -> genericDocError =<< text ("Couldn't find " ++ s)
+    _ -> agda2hsStringError $ "Couldn't find " ++ s
 
 
 lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition]
@@ -339,4 +339,4 @@ classMemberNames :: Definition -> C [Hs.Name ()]
 classMemberNames def =
   case theDef def of
     Record{recFields = fs} -> fmap unQual <$> traverse compileQName (map unDom fs)
-    _ -> genericDocError =<< text "Not a record:" <+> prettyTCM (defName def)
+    _ -> agda2hsErrorM $ text "Not a record:" <+> prettyTCM (defName def)

src/Agda2Hs/Compile/Data.hs

@@ -51,9 +51,9 @@ compileData newtyp ds def = do
     allIndicesErased t = reduce (unEl t) >>= \case
       Pi dom t -> compileDomType (absName t) dom >>= \case
         DomDropped      -> allIndicesErased (unAbs t)
-        DomType{}       -> genericDocError =<< text "Not supported: indexed datatypes"
-        DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types"
-        DomForall{}     -> genericDocError =<< text "Not supported: indexed datatypes"
+        DomType{}       -> agda2hsError "Not supported: indexed datatypes"
+        DomConstraint{} -> agda2hsError "Not supported: constraints in types"
+        DomForall{}     -> agda2hsError "Not supported: indexed datatypes"
       _ -> return ()
 
 compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ())
@@ -74,6 +74,6 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c
   DomType s hsA     -> do
     ty <- addTyBang s hsA
     (ty :) <$> underAbstraction a tel compileConstructorArgs
-  DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints"
+  DomConstraint hsA -> agda2hsError "Not supported: constructors with class constraints"
   DomDropped        -> underAbstraction a tel compileConstructorArgs
   DomForall{}       -> __IMPOSSIBLE__

src/Agda2Hs/Compile/Function.hs

@@ -64,7 +64,7 @@ isSpecialCon qn = case prettyShow qn of
       ]
 
     itsBad :: Type -> NAPs -> C (Hs.Pat ())
-    itsBad _ _ = genericDocError =<< "constructor `" <> prettyTCM qn <> "` not supported in patterns"
+    itsBad _ _ = agda2hsErrorM $ "constructor `" <> prettyTCM qn <> "` not supported in patterns"
 
 -- | Translate Int.pos pattern.
 posIntPat :: Type -> NAPs -> C (Hs.Pat ())
@@ -91,7 +91,7 @@ compileLitNatPat = \case
     | prettyShow (conName ch) == "Agda.Builtin.Nat.Nat.zero" -> return 0
     | prettyShow (conName ch) == "Agda.Builtin.Nat.Nat.suc"
     , [p] <- ps -> (1+) <$> compileLitNatPat (namedArg p)
-  p -> genericDocError =<< "not a literal natural number pattern:" <?> prettyTCM p
+  p -> agda2hsErrorM $ "not a literal natural number pattern:" <?> prettyTCM p
 
 
 compileFun, compileFun'
@@ -110,7 +110,7 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
   reportSDoc "agda2hs.compile" 6 $ "Compiling function: " <+> prettyTCM defName
 
   whenM ((withSig &&) <$> inRecordMod defName) $
-    genericDocError =<< text "not supported by agda2hs: functions inside a record module"
+    agda2hsError "not supported: functions inside a record module"
 
   ifM (endsInSort defType)
     -- if the function type ends in Sort, it's a type alias!
@@ -154,8 +154,8 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
       cs  <- map (addPats paramPats) <$>
         mapMaybeM (compileClause m (Just defName) x typ) clauses
 
-      when (null cs) $ genericDocError
-        =<< text "Functions defined with absurd patterns exclusively are not supported."
+      when (null cs) $ agda2hsErrorM $
+            text "Functions defined with absurd patterns exclusively are not supported."
         <+> text "Use function `error` from the Haskell.Prelude instead."
 
       return $ sig ++ [Hs.FunBind () cs]
@@ -259,7 +259,7 @@ compilePats _ [] = pure []
 compilePats ty ((namedArg -> ProjP po pn):ps) = do
   reportSDoc "agda2hs.compile" 10 $ "compiling copattern: " <+> text (prettyShow pn)
   unlessM (asks copatternsEnabled `or2M` (isJust <$> isUnboxProjection pn)) $
-    genericDocError =<< "not supported in Haskell: copatterns"
+    agda2hsError "not supported in Haskell: copatterns"
 
   ty     <- fromMaybe __IMPOSSIBLE__ <$> getDefType pn ty
   (a, b) <- mustBePi ty
@@ -278,7 +278,7 @@ compilePats ty ((namedArg -> pat):ps) = do
     DOTerm     -> do
       checkNoAsPatterns pat
       (:) <$> compilePat (unDom a) pat <*> rest
-  where checkForced  = when (isForcedPat pat) $ genericDocError =<< "not supported by agda2hs: forced (dot) patterns in non-erased positions"
+  where checkForced  = when (isForcedPat pat) $ agda2hsError "not supported: forced (dot) patterns in non-erased positions"
 
 
 compilePat :: Type -> DeBruijnPattern -> C (Hs.Pat ())
@@ -308,7 +308,7 @@ compilePat ty (LitP _ l) = compileLitPat l
 
 
 -- nothing else is supported
-compilePat _ p = genericDocError =<< "bad pattern:" <?> prettyTCM p
+compilePat _ p = agda2hsErrorM $ "bad pattern:" <?> prettyTCM p
 
 
 compileErasedConP :: Type -> Strictness -> NAPs -> C (Hs.Pat ())
@@ -319,7 +319,7 @@ compileErasedConP ty s ps = compilePats ty ps >>= \case
 compileLitPat :: Literal -> C (Hs.Pat ())
 compileLitPat = \case
   LitChar c -> return $ Hs.charP c
-  l -> genericDocError =<< "bad literal pattern:" <?> prettyTCM l
+  l -> agda2hsErrorM $ "bad literal pattern:" <?> prettyTCM l
 
 compileTupleConP :: Type -> Hs.Boxed -> NAPs -> C (Hs.Pat ())
 compileTupleConP ty b ps = do
@@ -388,7 +388,7 @@ checkTransparentPragma def = compileFun False def >>= \case
     checkTransparentTypeDef (Hs.DHApp _ _ (Hs.UnkindedVar _ x)) (Hs.TyVar _ y) | x == y = return ()
     checkTransparentTypeDef _ _ = errNotTransparent
 
-    errNotTransparent = genericDocError =<<
+    errNotTransparent = agda2hsErrorM $
       "Cannot make function" <+> prettyTCM (defName def) <+> "transparent." <+>
       "A transparent function must have exactly one non-erased argument and return it unchanged."
 
@@ -399,11 +399,11 @@ checkInlinePragma def@Defn{defName = f} = do
   let Function{funClauses = cs} = theDef def
   case filter (isJust . clauseBody) cs of
     [c] ->
-      unlessM (allowedPats (namedClausePats c)) $ genericDocError =<<
+      unlessM (allowedPats (namedClausePats c)) $ agda2hsErrorM $
         "Cannot make function" <+> prettyTCM (defName def) <+> "inlinable." <+>
         "Inline functions can only use variable patterns or transparent record constructor patterns."
     _ ->
-      genericDocError =<<
+      agda2hsErrorM $
         "Cannot make function" <+> prettyTCM f <+> "inlinable." <+>
         "An inline function must have exactly one clause."
 

src/Agda2Hs/Compile/Imports.hs

@@ -81,7 +81,7 @@ compileImports top is0 = do
     checkClashingImports [] = return ()
     checkClashingImports (Import mod as p q _ : is) =
       case filter isClashing is of
-        (i : _) -> genericDocError =<< text (mkErrorMsg i)
+        (i : _) -> agda2hsStringError $ mkErrorMsg i
         []      -> checkClashingImports is
      where
         isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q)

src/Agda2Hs/Compile/Record.hs

@@ -86,7 +86,7 @@ compileMinRecords def sls = do
   -- 2. assert that all default implementations are the same (for a certain field)
   let getUnique f (x :| xs)
         | all (x ==) xs = return x
-        | otherwise     = genericDocError =<< do
+        | otherwise     = agda2hsErrorM $ do
           text ("Conflicting default implementations for " ++ pp f ++ ":") $$
             vcat [ text "-" <+> multilineText (pp d) | d <- nub (x : xs) ]
   decls <- Map.traverseWithKey getUnique
@@ -129,10 +129,10 @@ compileRecord target def = do
     -- record module has been opened.
     checkFieldInScope f = isInScopeUnqualified f >>= \case
       True  -> return ()
-      False -> setCurrentRangeQ f $ genericError $
-        "Record projections (`" ++ prettyShow (qnameName f) ++
-        "` in this case) must be brought into scope when compiling to Haskell record types. " ++
-        "Add `open " ++ Hs.prettyPrint rName ++ " public` after the record declaration to fix this."
+      False -> setCurrentRangeQ f $ agda2hsErrorM $
+        ("Record projections (`" <> prettyTCM (qnameName f) <>"` in this case)") <+>
+        "must be brought into scope when compiling to Haskell record types." <+>
+        "Add `open" <+> text (Hs.prettyPrint rName) <+> "public` after the record declaration to fix this."
 
     Record{..} = theDef def
 
@@ -157,7 +157,7 @@ compileRecord target def = do
             return (hsAssts, decl fieldName fieldType : hsFields)
           DomConstraint hsA -> case target of
             ToClass{} -> return (hsA : hsAssts , hsFields)
-            ToRecord{} -> genericError $
+            ToRecord{} -> agda2hsError $
               "Not supported: record/class with constraint fields"
           DomDropped -> return (hsAssts , hsFields)
           DomForall{} -> __IMPOSSIBLE__
@@ -182,24 +182,24 @@ checkUnboxPragma def = do
 
   -- recRecursive can be used again after agda 2.6.4.2 is released
   -- see agda/agda#7042
-  unless (all null recMutual) $ genericDocError
-    =<< text "Unboxed record" <+> prettyTCM (defName def)
+  unless (all null recMutual) $ agda2hsErrorM $
+        text "Unboxed record" <+> prettyTCM (defName def)
     <+> text "cannot be recursive"
 
   TelV tel _ <- telViewUpTo recPars (defType def)
   addContext tel $ do
     pars <- getContextArgs
     let fieldTel = recTel `apply` pars
     fields <- nonErasedFields fieldTel
-    unless (length fields == 1) $ genericDocError
-      =<< text "Unboxed record" <+> prettyTCM (defName def)
+    unless (length fields == 1) $ agda2hsErrorM $
+          text "Unboxed record" <+> prettyTCM (defName def)
       <+> text "should have exactly one non-erased field"
 
   where
     nonErasedFields :: Telescope -> C [String]
     nonErasedFields EmptyTel = return []
     nonErasedFields (ExtendTel a tel) = compileDom a >>= \case
       DODropped  -> underAbstraction a tel nonErasedFields
-      DOType -> genericDocError =<< text "Type field in unboxed record not supported"
-      DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported"
+      DOType -> agda2hsError "Type field in unboxed record not supported"
+      DOInstance -> agda2hsError "Instance field in unboxed record not supported"
       DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields