[ fix ] Backticked names cannot be used as prefix operators

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
 

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

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)

src/Parser/Support.idr

@@ -24,20 +24,29 @@ 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
 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

tests/idris2/error/error035/Issue3550.idr

@@ -0,0 +1,3 @@
+CharacterExcept : Type
+CharacterExcept = `Elem` _ . fst
+

tests/idris2/error/error035/Issue3739.idr

@@ -0,0 +1,2 @@
+foo : Nat -> Nat
+foo = `minus` 5

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

tests/idris2/error/error035/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+check Issue3550.idr
+check Issue3739.idr

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 |