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/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 3ac9110487a..8d29c750691 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 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" @@ -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/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/error035/Issue3550.idr b/tests/idris2/error/error035/Issue3550.idr new file mode 100644 index 00000000000..819548efbe4 --- /dev/null +++ b/tests/idris2/error/error035/Issue3550.idr @@ -0,0 +1,3 @@ +CharacterExcept : Type +CharacterExcept = `Elem` _ . fst + diff --git a/tests/idris2/error/error035/Issue3739.idr b/tests/idris2/error/error035/Issue3739.idr new file mode 100644 index 00000000000..b0b5d7b6d8e --- /dev/null +++ b/tests/idris2/error/error035/Issue3739.idr @@ -0,0 +1,2 @@ +foo : Nat -> Nat +foo = `minus` 5 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/error035/run b/tests/idris2/error/error035/run new file mode 100755 index 00000000000..4f956ca180b --- /dev/null +++ b/tests/idris2/error/error035/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +check Issue3550.idr +check Issue3739.idr 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 |