[ new ] comma-separated interface parameters (#682)

src/Idris/Parser.idr

@@ -1215,16 +1215,16 @@ implBinds fname indents
          pure ((n, rig, tm) :: more)
   <|> pure []
 
-ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm)
+ifaceParam : FileName -> IndentInfo -> Rule (List Name, PTerm)
 ifaceParam fname indents
     = do symbol "("
-         n <- name
+         ns <- sepBy1 (symbol ",") name
          symbol ":"
          tm <- expr pdef fname indents
          symbol ")"
-         pure (n, tm)
+         pure (ns, tm)
   <|> do n <- bounds name
-         pure (n.val, PInfer (boundToFC fname n))
+         pure ([n.val], PInfer (boundToFC fname n))
 
 ifaceDecl : FileName -> IndentInfo -> Rule PDecl
 ifaceDecl fname indents
@@ -1235,7 +1235,8 @@ ifaceDecl fname indents
                          commit
                          cons   <- constraints fname indents
                          n      <- name
-                         params <- many (ifaceParam fname indents)
+                         paramss <- many (ifaceParam fname indents)
+                         let params = concatMap (\ (ns, t) => map (\ n => (n, t)) ns) paramss
                          det    <- option []
                                      (do symbol "|"
                                          sepBy (symbol ",") name)

tests/Main.idr

@@ -68,6 +68,7 @@ idrisTests
        "interface005", "interface006", "interface007", "interface008",
        "interface009", "interface010", "interface011", "interface012",
        "interface013", "interface014", "interface015", "interface016",
+       "interface017",
        -- Miscellaneous REPL
        "interpreter001", "interpreter002", "interpreter003",
        -- Implicit laziness, lazy evaluation

tests/idris2/interface017/Tricho.idr

@@ -0,0 +1,10 @@
+module Tricho
+
+data Trichotomy : (eq, lt : a -> a -> Type) -> (a -> a -> Type) where
+  LT : {0 x, y : a} -> lt x y -> Trichotomy eq lt x y
+  EQ : {0 x, y : a} -> eq x y -> Trichotomy eq lt x x
+  GT : {0 x, y : a} -> lt y x -> Trichotomy eq lt x y
+
+interface Trichotomous (a : Type) (eq, lt : a -> a -> Type) where
+
+  trichotomy : (x, y : a) -> Trichotomy eq lt x y

tests/idris2/interface017/expected

@@ -0,0 +1 @@
+1/1: Building Tricho (Tricho.idr)

tests/idris2/interface017/run

@@ -0,0 +1,3 @@
+$1 --no-color --console-width 0 Tricho.idr --check
+
+rm -rf build