[ fix #710 ] Enforce assumptions about capitalised idents (#1207)

Given we keep getting tripped up by this, here we go:

* Namespaces
* Data names
* Record names
* Data constructor names (except for operators)
* Record constructor names (except for operators)
* Interface constructor names (except for operators)

src/Idris/Parser.idr

@@ -833,10 +833,10 @@ visibility
     = visOption
   <|> pure Private
 
-tyDecl : String -> FileName -> IndentInfo -> Rule PTypeDecl
-tyDecl predoc fname indents
+tyDecl : Rule Name -> String -> FileName -> IndentInfo -> Rule PTypeDecl
+tyDecl declName predoc fname indents
     = do b <- bounds (do doc   <- option "" documentation
-                         n     <- bounds name
+                         n     <- bounds declName
                          symbol ":"
                          mustWork $
                             do ty  <- expr pdef fname indents
@@ -918,7 +918,7 @@ mkDataConType _ _ _ -- with and named applications not allowed in simple ADTs
 simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
 simpleCon fname ret indents
     = do b <- bounds (do cdoc   <- option "" documentation
-                         cname  <- bounds name
+                         cname  <- bounds dataConstructorName
                          params <- many (argExpr plhs fname indents)
                          pure (cdoc, cname.val, boundToFC fname cname, params))
          atEnd indents
@@ -959,7 +959,7 @@ dataBody fname mincol start n indents ty
                                                dopts <- sepBy1 (symbol ",") dataOpt
                                                symbol "]"
                                                pure $ forget dopts)
-                         cs <- blockAfter mincol (tyDecl "" fname)
+                         cs <- blockAfter mincol (tyDecl (mustWork dataConstructorName) "" fname)
                          pure (opts, cs))
          (opts, cs) <- pure b.val
          pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs)
@@ -975,7 +975,7 @@ dataDeclBody : FileName -> IndentInfo -> Rule PDataDecl
 dataDeclBody fname indents
     = do b <- bounds (do col <- column
                          keyword "data"
-                         n <- name
+                         n <- mustWork capitalisedName
                          pure (col, n))
          (col, n) <- pure b.val
          simpleData fname b n indents <|> gadtData fname col b n indents
@@ -1111,7 +1111,7 @@ fix
   <|> (keyword "prefix" *> pure Prefix)
 
 namespaceHead : Rule Namespace
-namespaceHead = keyword "namespace" *> commit *> namespaceId
+namespaceHead = keyword "namespace" *> mustWork namespaceId
 
 namespaceDecl : FileName -> IndentInfo -> Rule PDecl
 namespaceDecl fname indents
@@ -1166,10 +1166,10 @@ usingDecls fname indents
                          commit
                          symbol "("
                          us <- sepBy (symbol ",")
-                                     (do n <- option Nothing
+                                     (do n <- optional
                                                 (do x <- unqualifiedName
                                                     symbol ":"
-                                                    pure (Just (UN x)))
+                                                    pure (UN x))
                                          ty <- typeExpr pdef fname indents
                                          pure (n, ty))
                          symbol ")"
@@ -1225,6 +1225,12 @@ getVisibility (Just vis) (Left x :: xs)
    = fatalError "Multiple visibility modifiers"
 getVisibility v (_ :: xs) = getVisibility v xs
 
+recordConstructor : Rule Name
+recordConstructor
+  = do exactIdent "constructor"
+       n <- mustWork dataConstructorName
+       pure n
+
 constraints : FileName -> IndentInfo -> SourceEmptyRule (List (Maybe Name, PTerm))
 constraints fname indents
     = do tm <- appExpr pdef fname indents
@@ -1283,10 +1289,7 @@ ifaceDecl fname indents
                                      (do symbol "|"
                                          sepBy (symbol ",") name)
                          keyword "where"
-                         dc <- option Nothing
-                                 (do exactIdent "constructor"
-                                     n <- name
-                                     pure (Just n))
+                         dc <- optional recordConstructor
                          body <- assert_total (blockAfter col (topDecl fname))
                          pure (\fc : FC => PInterface fc
                                       vis cons n doc params det dc (collectDefs (concat body))))
@@ -1300,10 +1303,10 @@ implDecl fname indents
                          let opts = mapMaybe getRight visOpts
                          col <- column
                          option () (keyword "implementation")
-                         iname <- option Nothing (do symbol "["
-                                                     iname <- name
-                                                     symbol "]"
-                                                     pure (Just iname))
+                         iname <- optional (do symbol "["
+                                               iname <- name
+                                               symbol "]"
+                                               pure iname)
                          impls  <- implBinds fname indents
                          cons   <- constraints fname indents
                          n      <- name
@@ -1371,19 +1374,15 @@ recordDecl fname indents
                          vis   <- visibility
                          col   <- column
                          keyword "record"
-                         n       <- name
+                         n       <- mustWork capitalisedName
                          paramss <- many (recordParam fname indents)
                          let params = concat paramss
                          keyword "where"
-                         dcflds <- blockWithOptHeaderAfter col ctor (fieldDecl fname)
+                         dcflds <- blockWithOptHeaderAfter col
+                                      (\ idt => recordConstructor <* atEnd idt)
+                                      (fieldDecl fname)
                          pure (\fc : FC => PRecord fc doc vis n params (fst dcflds) (concat (snd dcflds))))
          pure (b.val (boundToFC fname b))
-  where
-  ctor : IndentInfo -> Rule Name
-  ctor idt = do exactIdent "constructor"
-                n <- name
-                atEnd idt
-                pure n
 
 claim : FileName -> IndentInfo -> Rule PDecl
 claim fname indents
@@ -1393,7 +1392,7 @@ claim fname indents
                          let opts = mapMaybe getRight visOpts
                          m   <- multiplicity
                          rig <- getMult m
-                         cl  <- tyDecl doc fname indents
+                         cl  <- tyDecl name doc fname indents
                          pure (doc, vis, opts, rig, cl))
          (doc, vis, opts, rig, cl) <- pure b.val
          pure (PClaim (boundToFC fname b) rig vis opts cl)
@@ -1496,7 +1495,7 @@ import_ fname indents
                          ns <- moduleIdent
                          nsAs <- option (miAsNamespace ns)
                                         (do exactIdent "as"
-                                            namespaceId)
+                                            mustWork namespaceId)
                          pure (reexp, ns, nsAs))
          atEnd indents
          (reexp, ns, nsAs) <- pure b.val

src/Libraries/Text/Parser/Core.idr

@@ -213,6 +213,11 @@ export %inline
 fail : String -> Grammar tok c ty
 fail = Fail Nothing False
 
+||| Always fail with a message and a location
+export %inline
+failLoc : Bounds -> String -> Grammar tok c ty
+failLoc b = Fail (Just b) False
+
 export %inline
 fatalError : String -> Grammar tok c ty
 fatalError = Fail Nothing True

src/Parser/Rule/Source.idr

@@ -214,9 +214,23 @@ namespacedIdent
             Ident i => Just (Nothing, i)
             _ => Nothing)
 
+isCapitalisedIdent : WithBounds String -> SourceEmptyRule ()
+isCapitalisedIdent str =
+  let val = str.val
+      loc = str.bounds
+      err : SourceEmptyRule ()
+          = failLoc loc ("Expected a capitalised identifier, got: " ++ val)
+  in case strM val of
+       StrNil => err
+       StrCons c _ => if (isUpper c || c > chr 160) then pure () else err
+
+
 export
 namespaceId : Rule Namespace
-namespaceId = map (uncurry mkNestedNamespace) namespacedIdent
+namespaceId = do
+  nsid <- bounds namespacedIdent
+  isCapitalisedIdent (snd <$> nsid)
+  pure (uncurry mkNestedNamespace nsid.val)
 
 export
 moduleIdent : Rule ModuleIdent
@@ -244,28 +258,32 @@ reservedNames
     = ["Type", "Int", "Integer", "Bits8", "Bits16", "Bits32", "Bits64",
        "String", "Char", "Double", "Lazy", "Inf", "Force", "Delay"]
 
+isNotReserved : WithBounds String -> SourceEmptyRule ()
+isNotReserved x
+    = if x.val `elem` reservedNames
+      then failLoc x.bounds $ "can't use reserved name " ++ x.val
+      else pure ()
+
+export
+opNonNS : Rule Name
+opNonNS = symbol "(" *> (operator <|> postfixProj) <* symbol ")"
+
 export
 name : Rule Name
 name = opNonNS <|> do
-  nsx <- namespacedIdent
+  nsx <- bounds namespacedIdent
   -- writing (ns, x) <- namespacedIdent leads to an unsoled constraint.
   -- I tried to write a minimised test case but could not reproduce the error
   -- on a simplified example.
-  let ns = fst nsx
-  let x = snd nsx
-  opNS (mkNestedNamespace ns x) <|> nameNS ns x
+  let ns = fst nsx.val
+  let x = snd <$> nsx
+  opNS (mkNestedNamespace ns x.val) <|> nameNS ns x
  where
-  reserved : String -> Bool
-  reserved n = n `elem` reservedNames
 
-  nameNS : Maybe Namespace -> String -> SourceEmptyRule Name
-  nameNS ns x =
-    if reserved x
-      then fail $ "can't use reserved name " ++ x
-      else pure $ mkNamespacedName ns x
-
-  opNonNS : Rule Name
-  opNonNS = symbol "(" *> (operator <|> postfixProj) <* symbol ")"
+  nameNS : Maybe Namespace -> WithBounds String -> SourceEmptyRule Name
+  nameNS ns x = do
+    isNotReserved x
+    pure $ mkNamespacedName ns x.val
 
   opNS : Namespace -> Rule Name
   opNS ns = do
@@ -274,6 +292,18 @@ name = opNonNS <|> do
     symbol ")"
     pure (NS ns n)
 
+export
+capitalisedName : Rule Name
+capitalisedName = do
+  id <- bounds identPart
+  isCapitalisedIdent id
+  isNotReserved id
+  pure (UN id.val)
+
+export
+dataConstructorName : Rule Name
+dataConstructorName = opNonNS <|> capitalisedName
+
 export
 IndentInfo : Type
 IndentInfo = Int

tests/Main.idr

@@ -70,7 +70,7 @@ idrisTestsError = MkTestPool []
        "error011", "error012", "error013", "error014", "error015",
        -- Parse errors
        "perror001", "perror002", "perror003", "perror004", "perror005",
-       "perror006", "perror007"]
+       "perror006", "perror007", "perror008"]
 
 idrisTestsInteractive : TestPool
 idrisTestsInteractive = MkTestPool []

tests/idris2/perror008/Issue710a.idr

@@ -0,0 +1,4 @@
+module Issue710a
+
+record r where
+  constructor MkR

tests/idris2/perror008/Issue710b.idr

@@ -0,0 +1,3 @@
+module Issue710b
+
+data r : Type where

tests/idris2/perror008/Issue710c.idr

@@ -0,0 +1,5 @@
+infix 3 #
+
+data T : Type where
+  (#) : T -> T -> T
+  leaf : T

tests/idris2/perror008/Issue710d.idr

@@ -0,0 +1,2 @@
+record T where
+  constructor mkT

tests/idris2/perror008/Issue710e.idr

@@ -0,0 +1,3 @@
+%default total
+
+namespace a

tests/idris2/perror008/Issue710f.idr

@@ -0,0 +1,3 @@
+interface Lalala where
+  constructor cons
+  x : Int -> Int

tests/idris2/perror008/expected

@@ -0,0 +1,54 @@
+1/1: Building Issue710a (Issue710a.idr)
+Error: Expected a capitalised identifier, got: r.
+
+Issue710a.idr:3:8--3:9
+ 1 | module Issue710a
+ 2 | 
+ 3 | record r where
+            ^
+
+1/1: Building Issue710b (Issue710b.idr)
+Error: Expected a capitalised identifier, got: r.
+
+Issue710b.idr:3:6--3:7
+ 1 | module Issue710b
+ 2 | 
+ 3 | data r : Type where
+          ^
+
+1/1: Building Issue710c (Issue710c.idr)
+Error: Expected a capitalised identifier, got: leaf.
+
+Issue710c.idr:5:3--5:4
+ 1 | infix 3 #
+ 2 | 
+ 3 | data T : Type where
+ 4 |   (#) : T -> T -> T
+ 5 |   leaf : T
+       ^
+
+1/1: Building Issue710d (Issue710d.idr)
+Error: Expected a capitalised identifier, got: mkT.
+
+Issue710d.idr:2:15--2:16
+ 1 | record T where
+ 2 |   constructor mkT
+                   ^
+
+1/1: Building Issue710e (Issue710e.idr)
+Error: Expected a capitalised identifier, got: a.
+
+Issue710e.idr:3:11--3:12
+ 1 | %default total
+ 2 | 
+ 3 | namespace a
+               ^
+
+1/1: Building Issue710f (Issue710f.idr)
+Error: Expected a capitalised identifier, got: cons.
+
+Issue710f.idr:2:15--2:16
+ 1 | interface Lalala where
+ 2 |   constructor cons
+                   ^
+

tests/idris2/perror008/run

@@ -0,0 +1,8 @@
+$1 --no-color --console-width 0 --check Issue710a.idr || true
+$1 --no-color --console-width 0 --check Issue710b.idr || true
+$1 --no-color --console-width 0 --check Issue710c.idr || true
+$1 --no-color --console-width 0 --check Issue710d.idr || true
+$1 --no-color --console-width 0 --check Issue710e.idr || true
+$1 --no-color --console-width 0 --check Issue710f.idr || true
+
+rm -rf build