Error ProjectionIsIrrelevant instead of GenericError

src/full/Agda/TypeChecking/Errors.hs

@@ -262,6 +262,7 @@ errorString = \case
   SplitInProp{}                            -> "SplitInProp"
   DefinitionIsIrrelevant{}                 -> "DefinitionIsIrrelevant"
   DefinitionIsErased{}                     -> "DefinitionIsErased"
+  ProjectionIsIrrelevant{}                 -> "ProjectionIsIrrelevant"
   VariableIsIrrelevant{}                   -> "VariableIsIrrelevant"
   VariableIsErased{}                       -> "VariableIsErased"
   VariableIsOfUnusableCohesion{}           -> "VariableIsOfUnusableCohesion"
@@ -674,6 +675,11 @@ instance PrettyTCM TypeError where
     DefinitionIsErased x -> fsep $
       "Identifier" : prettyTCM x : pwords "is declared erased, so it cannot be used here"
 
+    ProjectionIsIrrelevant x -> vcat
+      [ fsep [ "Projection " , prettyTCM x, " is irrelevant." ]
+      , "Turn on option --irrelevant-projections to use it (unsafe)"
+      ]
+
     VariableIsIrrelevant x -> fsep $
       "Variable" : prettyTCM (nameConcrete x) : pwords "is declared irrelevant, so it cannot be used here"
 

src/full/Agda/TypeChecking/Modalities.hs

@@ -47,10 +47,7 @@ checkRelevance' x def = do
           ]
         return $ boolToMaybe (not $ drel `moreRelevant` rel) $ DefinitionIsIrrelevant x
   where
-  needIrrProj = Just . GenericDocError <$> do
-    sep [ "Projection " , prettyTCM x, " is irrelevant."
-        , " Turn on option --irrelevant-projections to use it (unsafe)."
-        ]
+  needIrrProj = return $ Just $ ProjectionIsIrrelevant x
 
 -- | The second argument is the definition of the first.
 --   Returns 'Nothing' if ok, otherwise the error message.

src/full/Agda/TypeChecking/Monad/Base.hs

@@ -4669,6 +4669,7 @@ data TypeError
         | SplitInProp DataOrRecordE
         | DefinitionIsIrrelevant QName
         | DefinitionIsErased QName
+        | ProjectionIsIrrelevant QName
         | VariableIsIrrelevant Name
         | VariableIsErased Name
         | VariableIsOfUnusableCohesion Name Cohesion

test/Fail/Issue7193.err

@@ -1,6 +1,4 @@
 Issue7193.agda:12,11-18
-Projection 
-extract
- is irrelevant.
- Turn on option --irrelevant-projections to use it (unsafe).
+Projection  extract  is irrelevant.
+Turn on option --irrelevant-projections to use it (unsafe)
 when checking that the expression extract has type ⊤ → A

test/Fail/ScopeIrrelevantRecordField.err

@@ -1,6 +1,4 @@
 ScopeIrrelevantRecordField.agda:11,9-17
-Projection 
-Bla.bla0
- is irrelevant.
- Turn on option --irrelevant-projections to use it (unsafe).
+Projection  Bla.bla0  is irrelevant.
+Turn on option --irrelevant-projections to use it (unsafe)
 when checking that the expression Bla.bla0 has type Bla → Set

test/Fail/ShapeIrrelevantField.err

@@ -1,6 +1,4 @@
 ShapeIrrelevantField.agda:8,10-17
-Projection 
-Foo.foo
- is irrelevant.
- Turn on option --irrelevant-projections to use it (unsafe).
+Projection  Foo.foo  is irrelevant.
+Turn on option --irrelevant-projections to use it (unsafe)
 when checking that the expression Foo.foo has type Foo A → A