From 47a8f5d43b56b8a897ce89c2581891edcd7eccf5 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 16 Feb 2026 21:38:54 +0300 Subject: [PATCH 1/3] [ fix ] Backticked names cannot be used as prefix operators --- CHANGELOG_NEXT.md | 3 +++ src/Idris/Parser.idr | 24 +++++++++++-------- tests/cli/exec003/expected | 2 +- tests/idris2/error/perror007/expected | 6 ++--- tests/idris2/error/perror014/expected | 2 +- tests/idris2/error/perror037/Issue3550.idr | 3 +++ tests/idris2/error/perror037/Issue3739.idr | 2 ++ tests/idris2/error/perror037/expected | 18 ++++++++++++++ tests/idris2/error/perror037/run | 4 ++++ .../interactive/interactive028/expected | 2 +- 10 files changed, 50 insertions(+), 16 deletions(-) create mode 100644 tests/idris2/error/perror037/Issue3550.idr create mode 100644 tests/idris2/error/perror037/Issue3739.idr create mode 100644 tests/idris2/error/perror037/expected create mode 100755 tests/idris2/error/perror037/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 75d6684aa15..3f7b73afb7f 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -68,6 +68,9 @@ should target this file (`CHANGELOG_NEXT`). * Fixed coverage checker issues (#1800, #1998, #2318, #2822, #3679). * Fixed totality checking in namespace and mutual blocks (#2868, #3692). * Fixed incorrect argument multiplicity when using an as-pattern (#3687). +* Fixed an internal error + caused by using backticked names + as prefix operators (#3550). ### Building/Packaging changes diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 3ac9110487a..98796be3045 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -172,10 +172,14 @@ continueWith : IndentInfo -> String -> Rule () continueWith indents req = mustContinue indents (Just req) *> symbol req -iOperator : Rule OpStr -iOperator - = OpSymbols <$> operator - <|> Backticked <$> (symbol "`" *> name <* symbol "`") +symOperator : Rule OpStr +symOperator = OpSymbols <$> operator + +backtickedOperator : Rule OpStr +backtickedOperator = Backticked <$> (symbol "`" *> name <* symbol "`") + +generalOperator : Rule OpStr +generalOperator = symOperator <|> backtickedOperator data ArgType = UnnamedExpArg PTerm @@ -232,7 +236,7 @@ mutual <|> do b <- bounds (MkPair <$> simpleExpr fname indents <*> many (argExpr q fname indents)) (f, args) <- pure b.val pure (applyExpImp (start b) (end b) f (concat args)) - <|> do b <- fcBounds (MkPair <$> fcBounds iOperator <*> expr pdef fname indents) + <|> do b <- fcBounds (MkPair <$> fcBounds symOperator <*> expr pdef fname indents) (op, arg) <- pure b.val pure (PPrefixOp b.fc op arg) <|> fail "Expected 'case', 'if', 'do', application or operator expression" @@ -348,7 +352,7 @@ mutual = do b <- fcBounds $ do binder <- fcBounds $ parens fname (opBinder fname indents) continue indents - op <- fcBounds iOperator + op <- fcBounds generalOperator commit e <- expr q fname indents pure (binder, op, e) @@ -371,7 +375,7 @@ mutual <|> (do b <- bounds $ do continue indents - op <- fcBounds iOperator + op <- fcBounds generalOperator e <- case op.val of OpSymbols (UN (Basic "$")) => typeExpr q fname indents _ => expr q fname indents @@ -417,7 +421,7 @@ mutual -- left section. This may also be a prefix operator, but we'll sort -- that out when desugaring: if the operator is infix, treat it as a -- section otherwise treat it as prefix - = do b <- bounds (do op <- fcBounds iOperator + = do b <- bounds (do op <- fcBounds generalOperator e <- expr pdef fname indents continueWithDecorated fname indents ")" pure (op, e)) @@ -447,7 +451,7 @@ mutual (PImplicit (boundToFC fname (mergeBounds s rest))) rest.val)) <|> -- right sections - ((do op <- bounds (fcBounds iOperator <* decoratedSymbol fname ")") + ((do op <- bounds (fcBounds generalOperator <* decoratedSymbol fname ")") actD (toNonEmptyFC $ boundToFC fname s, Keyword, Nothing) let fc = boundToFC fname (mergeBounds s op) pure (PSectionR fc e.val op.val) @@ -1901,7 +1905,7 @@ parameters {auto fname : OriginDesc} {auto indents : IndentInfo} b <- fcBounds (do fixity <- decorate fname Keyword $ fix commit prec <- decorate fname Keyword $ intLit - ops <- sepBy1 (decoratedSymbol fname ",") iOperator + ops <- sepBy1 (decoratedSymbol fname ",") generalOperator pure (MkPFixityData vis binding fixity (fromInteger prec) ops) ) pure (map PFixity b) diff --git a/tests/cli/exec003/expected b/tests/cli/exec003/expected index be8013ddfd4..2b857234aa2 100644 --- a/tests/cli/exec003/expected +++ b/tests/cli/exec003/expected @@ -21,7 +21,7 @@ Error: Couldn't parse any alternatives: (Interactive):1:1--1:3 1 | !! ^^ -... (84 others) +... (83 others) ------ Hello! Error: Undefined name undefined. diff --git a/tests/idris2/error/perror007/expected b/tests/idris2/error/perror007/expected index e7cefb32c1f..6ebf5a5ea7e 100644 --- a/tests/idris2/error/perror007/expected +++ b/tests/idris2/error/perror007/expected @@ -6,7 +6,7 @@ StrError1:2:24--2:25 1 | foo : String 2 | foo = "empty interp: \{}" ^ -... (42 others) +... (41 others) 1/1: Building StrError2 (StrError2.idr) Error: Couldn't parse any alternatives: 1: Expected 'case', 'if', 'do', application or operator expression. @@ -15,7 +15,7 @@ StrError2:2:19--2:20 1 | foo : String 2 | foo = "nested: \{ " \{ 1 + } " }" ^ -... (31 others) +... (30 others) 1/1: Building StrError3 (StrError3.idr) Error: Couldn't parse any alternatives: 1: Expected 'case', 'if', 'do', application or operator expression. @@ -24,7 +24,7 @@ StrError3:2:7--2:8 1 | foo : String 2 | foo = "incomplete: \{ a <+> }" ^ -... (32 others) +... (31 others) 1/1: Building StrError4 (StrError4.idr) Error: Bracket is not properly closed. diff --git a/tests/idris2/error/perror014/expected b/tests/idris2/error/perror014/expected index 0bf8c4db76b..3c2b13bd1b1 100644 --- a/tests/idris2/error/perror014/expected +++ b/tests/idris2/error/perror014/expected @@ -9,4 +9,4 @@ ParseList:8:5--8:6 7 | , 4, 8 | , 5 ^ -... (42 others) +... (41 others) diff --git a/tests/idris2/error/perror037/Issue3550.idr b/tests/idris2/error/perror037/Issue3550.idr new file mode 100644 index 00000000000..819548efbe4 --- /dev/null +++ b/tests/idris2/error/perror037/Issue3550.idr @@ -0,0 +1,3 @@ +CharacterExcept : Type +CharacterExcept = `Elem` _ . fst + diff --git a/tests/idris2/error/perror037/Issue3739.idr b/tests/idris2/error/perror037/Issue3739.idr new file mode 100644 index 00000000000..b0b5d7b6d8e --- /dev/null +++ b/tests/idris2/error/perror037/Issue3739.idr @@ -0,0 +1,2 @@ +foo : Nat -> Nat +foo = `minus` 5 diff --git a/tests/idris2/error/perror037/expected b/tests/idris2/error/perror037/expected new file mode 100644 index 00000000000..947037bc6fa --- /dev/null +++ b/tests/idris2/error/perror037/expected @@ -0,0 +1,18 @@ +1/1: Building Issue3550 (Issue3550.idr) +Error: Couldn't parse any alternatives: +1: Expected 'case', 'if', 'do', application or operator expression. + +Issue3550:2:19--2:20 + 1 | CharacterExcept : Type + 2 | CharacterExcept = `Elem` _ . fst + ^ +... (42 others) +1/1: Building Issue3739 (Issue3739.idr) +Error: Couldn't parse any alternatives: +1: Expected 'case', 'if', 'do', application or operator expression. + +Issue3739:2:7--2:8 + 1 | foo : Nat -> Nat + 2 | foo = `minus` 5 + ^ +... (42 others) diff --git a/tests/idris2/error/perror037/run b/tests/idris2/error/perror037/run new file mode 100755 index 00000000000..4f956ca180b --- /dev/null +++ b/tests/idris2/error/perror037/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +check Issue3550.idr +check Issue3739.idr diff --git a/tests/idris2/interactive/interactive028/expected b/tests/idris2/interactive/interactive028/expected index 6b78dac3eed..48113de0b7d 100644 --- a/tests/idris2/interactive/interactive028/expected +++ b/tests/idris2/interactive/interactive028/expected @@ -4,7 +4,7 @@ Main> Couldn't parse any alternatives: (Interactive):1:4--1:5 1 | :t (3 : Nat) ^ -... (56 others) +... (55 others) Main> Expected string begin. (Interactive):1:5--1:7 From 64a3408f4227fe2fa2f74bb5114c1916d22428f8 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Tue, 17 Feb 2026 19:02:58 +0300 Subject: [PATCH 2/3] [ fix ] Do not add dot after `?` --- src/Parser/Support.idr | 13 +++++++++++-- tests/idris2/error/perror028/expected | 2 +- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index bbe07e92390..2892d518de7 100644 --- a/src/Parser/Support.idr +++ b/src/Parser/Support.idr @@ -24,6 +24,15 @@ fromLexError origin (ComposeNotClosing begin end, _, _, _) fromLexError origin (_, l, c, _) = LexFail (MkFC origin (l, c) (l, c + 1)) "Can't recognise token." +addDot : String -> String +addDot msg + = case strUncons $ reverse msg of + Nothing => msg + Just (c, _) => if isPunct c then msg else msg +> '.' + where + isPunct : Char -> Bool + isPunct c = c == '.' || c == '?' || c == '!' + export fromParsingErrors : (Show token, Pretty ann token) => OriginDesc -> List1 (ParsingError token) -> Error @@ -31,13 +40,13 @@ fromParsingErrors origin = ParseFail . (map fromError) where fromError : ParsingError token -> (FC, String) fromError (Error msg Nothing) - = (MkFC origin (0, 0) (0, 0), msg +> '.') + = (MkFC origin (0, 0) (0, 0), addDot msg) fromError (Error msg (Just t)) = let start = startBounds t; end = endBounds t in let fc = if start == end then MkFC origin start (mapSnd (+1) start) else MkFC origin start end - in (fc, msg +> '.') + in (fc, addDot msg) export getCharLit : String -> Maybe Char diff --git a/tests/idris2/error/perror028/expected b/tests/idris2/error/perror028/expected index 9c534c3b09e..c4ba7739a46 100644 --- a/tests/idris2/error/perror028/expected +++ b/tests/idris2/error/perror028/expected @@ -1,5 +1,5 @@ 1/1: Building LetInDo (LetInDo.idr) -Error: Let-in not supported in do block. Did you mean (let ... in ...)?. +Error: Let-in not supported in do block. Did you mean (let ... in ...)? LetInDo:6:13--6:15 2 | From bd4f63dcfb1566389347ff2e7ef26f4059ed1c35 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Wed, 18 Feb 2026 17:18:59 +0300 Subject: [PATCH 3/3] [ fix ] Better error message for backticked names as prefix operators --- src/Idris/Desugar.idr | 15 ++++++++++--- src/Idris/Parser.idr | 2 +- tests/cli/exec003/expected | 2 +- .../{perror037 => error035}/Issue3550.idr | 0 .../{perror037 => error035}/Issue3739.idr | 0 tests/idris2/error/error035/expected | 22 +++++++++++++++++++ .../idris2/error/{perror037 => error035}/run | 0 tests/idris2/error/perror007/expected | 6 ++--- tests/idris2/error/perror014/expected | 2 +- tests/idris2/error/perror037/expected | 18 --------------- .../interactive/interactive028/expected | 2 +- 11 files changed, 41 insertions(+), 28 deletions(-) rename tests/idris2/error/{perror037 => error035}/Issue3550.idr (100%) rename tests/idris2/error/{perror037 => error035}/Issue3739.idr (100%) create mode 100644 tests/idris2/error/error035/expected rename tests/idris2/error/{perror037 => error035}/run (100%) delete mode 100644 tests/idris2/error/perror037/expected diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index b3b92526e51..f64c46beb88 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -230,9 +230,18 @@ parameters (side : Side) rtoks <- toTokList r pure (Expr l.getLhs :: Op fc opn.fc ((opn.val, fixInfo), Just l) precInfo :: rtoks) toTokList (PPrefixOp fc opn arg) - = do (precInfo, fixInfo) <- checkConflictingFixities True opn - rtoks <- toTokList arg - pure (Op fc opn.fc ((opn.val, fixInfo), Nothing) precInfo :: rtoks) + = case opn.val of + Backticked nm + => throw $ GenericMsgSol opn.fc + "Cannot use backticked name as a prefix operator" + "Possible solutions" + [ "Use section: " ++ show (PSectionL fc opn arg) + , "Use application: " ++ show (PApp fc (PRef opn.fc nm) arg) + ] + OpSymbols {} + => do (precInfo, fixInfo) <- checkConflictingFixities True opn + rtoks <- toTokList arg + pure (Op fc opn.fc ((opn.val, fixInfo), Nothing) precInfo :: rtoks) toTokList t = pure [Expr t] record BangData where diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 98796be3045..8d29c750691 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -236,7 +236,7 @@ mutual <|> do b <- bounds (MkPair <$> simpleExpr fname indents <*> many (argExpr q fname indents)) (f, args) <- pure b.val pure (applyExpImp (start b) (end b) f (concat args)) - <|> do b <- fcBounds (MkPair <$> fcBounds symOperator <*> expr pdef fname indents) + <|> do b <- fcBounds (MkPair <$> fcBounds generalOperator <*> expr pdef fname indents) (op, arg) <- pure b.val pure (PPrefixOp b.fc op arg) <|> fail "Expected 'case', 'if', 'do', application or operator expression" diff --git a/tests/cli/exec003/expected b/tests/cli/exec003/expected index 2b857234aa2..be8013ddfd4 100644 --- a/tests/cli/exec003/expected +++ b/tests/cli/exec003/expected @@ -21,7 +21,7 @@ Error: Couldn't parse any alternatives: (Interactive):1:1--1:3 1 | !! ^^ -... (83 others) +... (84 others) ------ Hello! Error: Undefined name undefined. diff --git a/tests/idris2/error/perror037/Issue3550.idr b/tests/idris2/error/error035/Issue3550.idr similarity index 100% rename from tests/idris2/error/perror037/Issue3550.idr rename to tests/idris2/error/error035/Issue3550.idr diff --git a/tests/idris2/error/perror037/Issue3739.idr b/tests/idris2/error/error035/Issue3739.idr similarity index 100% rename from tests/idris2/error/perror037/Issue3739.idr rename to tests/idris2/error/error035/Issue3739.idr diff --git a/tests/idris2/error/error035/expected b/tests/idris2/error/error035/expected new file mode 100644 index 00000000000..63dc1643417 --- /dev/null +++ b/tests/idris2/error/error035/expected @@ -0,0 +1,22 @@ +1/1: Building Issue3550 (Issue3550.idr) +Error: Cannot use backticked name as a prefix operator + +Issue3550:2:19--2:25 + 1 | CharacterExcept : Type + 2 | CharacterExcept = `Elem` _ . fst + ^^^^^^ + +Possible solutions: + - Use section: (`Elem` _ . fst) + - Use application: Elem _ . fst +1/1: Building Issue3739 (Issue3739.idr) +Error: Cannot use backticked name as a prefix operator + +Issue3739:2:7--2:14 + 1 | foo : Nat -> Nat + 2 | foo = `minus` 5 + ^^^^^^^ + +Possible solutions: + - Use section: (`minus` 5) + - Use application: minus 5 diff --git a/tests/idris2/error/perror037/run b/tests/idris2/error/error035/run similarity index 100% rename from tests/idris2/error/perror037/run rename to tests/idris2/error/error035/run diff --git a/tests/idris2/error/perror007/expected b/tests/idris2/error/perror007/expected index 6ebf5a5ea7e..e7cefb32c1f 100644 --- a/tests/idris2/error/perror007/expected +++ b/tests/idris2/error/perror007/expected @@ -6,7 +6,7 @@ StrError1:2:24--2:25 1 | foo : String 2 | foo = "empty interp: \{}" ^ -... (41 others) +... (42 others) 1/1: Building StrError2 (StrError2.idr) Error: Couldn't parse any alternatives: 1: Expected 'case', 'if', 'do', application or operator expression. @@ -15,7 +15,7 @@ StrError2:2:19--2:20 1 | foo : String 2 | foo = "nested: \{ " \{ 1 + } " }" ^ -... (30 others) +... (31 others) 1/1: Building StrError3 (StrError3.idr) Error: Couldn't parse any alternatives: 1: Expected 'case', 'if', 'do', application or operator expression. @@ -24,7 +24,7 @@ StrError3:2:7--2:8 1 | foo : String 2 | foo = "incomplete: \{ a <+> }" ^ -... (31 others) +... (32 others) 1/1: Building StrError4 (StrError4.idr) Error: Bracket is not properly closed. diff --git a/tests/idris2/error/perror014/expected b/tests/idris2/error/perror014/expected index 3c2b13bd1b1..0bf8c4db76b 100644 --- a/tests/idris2/error/perror014/expected +++ b/tests/idris2/error/perror014/expected @@ -9,4 +9,4 @@ ParseList:8:5--8:6 7 | , 4, 8 | , 5 ^ -... (41 others) +... (42 others) diff --git a/tests/idris2/error/perror037/expected b/tests/idris2/error/perror037/expected deleted file mode 100644 index 947037bc6fa..00000000000 --- a/tests/idris2/error/perror037/expected +++ /dev/null @@ -1,18 +0,0 @@ -1/1: Building Issue3550 (Issue3550.idr) -Error: Couldn't parse any alternatives: -1: Expected 'case', 'if', 'do', application or operator expression. - -Issue3550:2:19--2:20 - 1 | CharacterExcept : Type - 2 | CharacterExcept = `Elem` _ . fst - ^ -... (42 others) -1/1: Building Issue3739 (Issue3739.idr) -Error: Couldn't parse any alternatives: -1: Expected 'case', 'if', 'do', application or operator expression. - -Issue3739:2:7--2:8 - 1 | foo : Nat -> Nat - 2 | foo = `minus` 5 - ^ -... (42 others) diff --git a/tests/idris2/interactive/interactive028/expected b/tests/idris2/interactive/interactive028/expected index 48113de0b7d..6b78dac3eed 100644 --- a/tests/idris2/interactive/interactive028/expected +++ b/tests/idris2/interactive/interactive028/expected @@ -4,7 +4,7 @@ Main> Couldn't parse any alternatives: (Interactive):1:4--1:5 1 | :t (3 : Nat) ^ -... (55 others) +... (56 others) Main> Expected string begin. (Interactive):1:5--1:7