[ fix ] Ability for data types to be operators was restored

src/Idris/Parser.idr

@@ -979,7 +979,7 @@ dataDeclBody : FileName -> IndentInfo -> Rule PDataDecl
 dataDeclBody fname indents
     = do b <- bounds (do col <- column
                          keyword "data"
-                         n <- mustWork capitalisedName
+                         n <- mustWork dataTypeName
                          pure (col, n))
          (col, n) <- pure b.val
          simpleData fname b n indents <|> gadtData fname col b n indents
@@ -1378,7 +1378,7 @@ recordDecl fname indents
                          vis   <- visibility
                          col   <- column
                          keyword "record"
-                         n       <- mustWork capitalisedName
+                         n       <- mustWork dataTypeName
                          paramss <- many (recordParam fname indents)
                          let params = concat paramss
                          keyword "where"

src/Parser/Rule/Source.idr

@@ -304,6 +304,10 @@ export
 dataConstructorName : Rule Name
 dataConstructorName = opNonNS <|> capitalisedName
 
+export %inline
+dataTypeName : Rule Name
+dataTypeName = dataConstructorName
+
 export
 IndentInfo : Type
 IndentInfo = Int

tests/Main.idr

@@ -47,7 +47,7 @@ idrisTestsBasic = MkTestPool []
        "basic041", "basic042", "basic043", "basic044", "basic045",
        "basic046", "basic047", "basic048", "basic049", "basic050",
        "basic051", "basic052", "basic053", "basic054", "basic055",
-       "basic056", "basic057"]
+       "basic056", "basic057", "basic058"]
 
 idrisTestsCoverage : TestPool
 idrisTestsCoverage = MkTestPool []

tests/idris2/basic058/DataTypeOp.idr

@@ -0,0 +1,30 @@
+--- Data declarations ---
+
+infix 0 =%=
+
+public export
+data (=%=) : (a -> b) -> (a -> b) -> Type where
+  ExtEq : {0 f, g : a -> b} -> ((x : a) -> f x = g x) -> f =%= g
+
+infix 0 %%
+
+public export
+data (%%) a b = Equs (a = b) (b = a)
+
+--- Records ---
+
+infix 0 =%%=
+
+public export
+record (=%%=) {a : Type} {b : Type} (f : a -> b) (g : a -> b) where
+  constructor ExtEqR
+  fa : (x : a) -> f x = g x
+
+--- Interfaces ---
+
+infix 0 =%%%=
+
+public export
+interface (=%%%=) (x : a) (y : a) (b : Type) (i : Type) where
+  idx : a -> i -> b
+  eq : (ix : i) -> idx x ix = idx y ix

tests/idris2/basic058/DataTypeProj.idr

@@ -0,0 +1,26 @@
+--- Data declarations ---
+
+data (.ah) a = Ah (List a)
+
+g : Int .ah -> Int
+g (Ah xs) = sum xs
+
+--- Records ---
+
+record (.aah) a where
+  constructor Aah
+  unaah : List a
+
+h : Num a => a.aah -> a
+h = sum . unaah
+
+--- Interfaces ---
+
+interface (.defaultable) a where
+  defa : a
+
+(.defaultable) Int where
+  defa = 0
+
+f : Num a => a.defaultable => a -> a
+f x = x + defa

tests/idris2/basic058/expected

@@ -0,0 +1,2 @@
+1/1: Building DataTypeOp (DataTypeOp.idr)
+1/1: Building DataTypeProj (DataTypeProj.idr)

tests/idris2/basic058/run

@@ -0,0 +1,4 @@
+$1 --no-banner --no-color --console-width 0 --check DataTypeOp.idr
+$1 --no-banner --no-color --console-width 0 --check DataTypeProj.idr
+
+rm -rf build