agda · andreasabel · Aug 31, 2024 · Aug 29, 2024
diff --git a/src/full/Agda/Interaction/Options/Errors.hs b/src/full/Agda/Interaction/Options/Errors.hs
@@ -128,6 +128,7 @@ data ErrorName
   | GeneralizeNotSupportedHere_
   | GeneralizedVarInLetOpenedModule_
   | HidingMismatch_
+  | IdiomBracketError_
   | IllTypedPatternAfterWithAbstraction_
   | IllegalDeclarationInDataDefinition_
   | IllegalHidingInPostfixProjection_

diff --git a/src/full/Agda/Syntax/IdiomBrackets.hs b/src/full/Agda/Syntax/IdiomBrackets.hs
@@ -50,17 +50,20 @@ appViewM = \case
   where
    onlyVisible a
       | defaultNamedArg () == fmap (() <$) a = return $ namedArg a
-      | otherwise = genericError "Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)"
-    noPlaceholder Placeholder{}       = genericError "Naked sections are not allowed in idiom brackets"
+      | otherwise = idiomBracketError "Only regular arguments are allowed in idiom brackets (no implicit or instance arguments)"
+    noPlaceholder Placeholder{}       = idiomBracketError "Naked sections are not allowed in idiom brackets"
     noPlaceholder (NoPlaceholder _ x) = return x
 
     ordinary (Ordinary a) = return a
-    ordinary _ = genericError "Binding syntax is not allowed in idiom brackets"
+    ordinary _ = idiomBracketError "Binding syntax is not allowed in idiom brackets"
 
 ensureInScope :: QName -> ScopeM ()
 ensureInScope q = do
   r <- resolveName q
   case r of
-    UnknownName -> genericError $
+    UnknownName -> idiomBracketError $
       prettyShow q ++ " needs to be in scope to use idiom brackets " ++ prettyShow leftIdiomBrkt ++ " ... " ++ prettyShow rightIdiomBrkt
     _ -> return ()
+
+idiomBracketError :: String -> ScopeM a
+idiomBracketError = typeError . IdiomBracketError
diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs
@@ -211,6 +211,8 @@ instance PrettyTCM TypeError where
 
     SyntaxError s -> fwords $ "Syntax error: "  ++ s
 
+    IdiomBracketError err -> fwords err
+
     NoKnownRecordWithSuchFields fields -> fsep $
       case fields of
         []  -> pwords "There are no records in scope"

diff --git a/src/full/Agda/TypeChecking/Errors/Names.hs b/src/full/Agda/TypeChecking/Errors/Names.hs
@@ -97,6 +97,7 @@ typeErrorName = \case
   GeneralizeNotSupportedHere                                 {} -> GeneralizeNotSupportedHere_
   GeneralizedVarInLetOpenedModule                            {} -> GeneralizedVarInLetOpenedModule_
   HidingMismatch                                             {} -> HidingMismatch_
+  IdiomBracketError                                          {} -> IdiomBracketError_
   IllTypedPatternAfterWithAbstraction                        {} -> IllTypedPatternAfterWithAbstraction_
   IllegalDeclarationInDataDefinition                         {} -> IllegalDeclarationInDataDefinition_
   IllegalHidingInPostfixProjection                           {} -> IllegalHidingInPostfixProjection_

diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs
@@ -4724,6 +4724,9 @@ data TypeError
              -- ^ Error thrown by the option parser.
         | NicifierError DeclarationException'
              -- ^ Error thrown in the nicifier phase 'Agda.Syntax.Concrete.Definitions'.
+        | IdiomBracketError String
+             -- ^ Error during (operator) parsing and interpreting the contents of idiom brackets.
+             --   Error message in 'String'.
         | NoKnownRecordWithSuchFields [C.Name]
             -- ^ The user has given a record expression with the given fields,
             --   but no record type known to type inference has all these fields.

diff --git a/test/Fail/BindingsInIdiomBrackets.agda b/test/Fail/BindingsInIdiomBrackets.agda
@@ -0,0 +1,16 @@
+-- Andreas, 2024-08-29
+-- Trigger error "Binding syntax is not allowed in idiom brackets"
+
+postulate
+  F     : Set → Set
+  pure  : ∀ {A} → A → F A
+  _<*>_ : ∀ {A B} → F (A → B) → F A → F B
+
+      bind  : ∀ {A B} → F A → (A → F B) → F B
+
+syntax bind m (λ x → k) = x ← m then k
+
+_ = (| _ ← _ then _ |)
+
+-- Expected error:
+-- Binding syntax is not allowed in idiom brackets
diff --git a/test/Fail/BindingsInIdiomBrackets.err b/test/Fail/BindingsInIdiomBrackets.err
@@ -0,0 +1,3 @@
+BindingsInIdiomBrackets.agda:13,5-23: error: [IdiomBracketError]
+Binding syntax is not allowed in idiom brackets
+when scope checking ⦇ _ ← _ then _ ⦈
diff --git a/test/Fail/IdiomBracketsImplicit.err b/test/Fail/IdiomBracketsImplicit.err
@@ -1,4 +1,4 @@
-IdiomBracketsImplicit.agda:22,15-37: error: [GenericError]
+IdiomBracketsImplicit.agda:22,15-37: error: [IdiomBracketError]
 Only regular arguments are allowed in idiom brackets (no implicit
 or instance arguments)
 when scope checking ⦇ _∷_ {n = n} a as ⦈
diff --git a/test/Fail/IdiomBracketsNotInScope.err b/test/Fail/IdiomBracketsNotInScope.err
@@ -1,3 +1,3 @@
-IdiomBracketsNotInScope.agda:12,10-21: error: [GenericError]
+IdiomBracketsNotInScope.agda:12,10-21: error: [IdiomBracketError]
 _<*>_ needs to be in scope to use idiom brackets ⦇ ... ⦈
 when scope checking ⦇ suc a ⦈
diff --git a/test/Fail/SectionsInIdiomBrackets.agda b/test/Fail/SectionsInIdiomBrackets.agda
@@ -0,0 +1,38 @@
+-- Andreas, 2024-08-29
+-- Sections not allowed in idiom brackets
+
+postulate
+  F     : Set → Set
+  pure  : ∀ {A} → A → F A
+  _<*>_ : ∀ {A B} → F (A → B) → F A → F B

+postulate
+  A     : Set
+  _⊕_   : A → A → A
+  a b c : F A
+  f     : A → A → A
+
+infixl 5 _⊕_
+
+-- Various experiments:
+
+_ = (| f |)
+_ = (| f a |)
+_ = (| f a b |)
+_ = (| λ x y → f x y |)  -- same as (| f |)
+-- _ = (| λ x → f a x |) -- (F A) !=< A
+-- _ = (| (f a) b |) -- (F A) !=< A
+
+_ = (| (| a ⊕ b |) ⊕ c |)  -- Accepted
+-- _ = (| a ⊕ b ⊕ c |)  -- Ill-typed
+
+accepted0 = (| _⊕_ |)
+accepted2 = (| a ⊕ b |)
+
+-- Trigger error:
+
+-- rejected1 = (| λ x → a ⊕ x |)
+-- rejected1 = (|  a ⊕_ |)
+rejected1 = (|  _⊕ b |)
+
+-- Error: Naked sections are not allowed in idiom brackets
diff --git a/test/Fail/SectionsInIdiomBrackets.err b/test/Fail/SectionsInIdiomBrackets.err
@@ -0,0 +1,3 @@
+SectionsInIdiomBrackets.agda:36,13-24: error: [IdiomBracketError]
+Naked sections are not allowed in idiom brackets
+when scope checking ⦇ _⊕ b ⦈