do not allow multiple alternatives for 0 arity functions

5 files changed, 22 insertions, 13 deletions

diff --git a/src/LambdaCube/Compiler/Infer.hs b/src/LambdaCube/Compiler/Infer.hs
index c3b13b82..00106612 100644
--- a/src/LambdaCube/Compiler/Infer.hs
+++ b/src/LambdaCube/Compiler/Infer.hs
@@ -1853,19 +1853,21 @@ compileFunAlts par ulend lend ge ds = \case
         [] -> return tf    -- builtin type family
         alts -> compileFunAlts True id SLabelEnd ge [TypeAnn n $ addParamsS ps t] alts
     [p@PrecDef{}] -> return [p]
-    fs@((FunAlt n vs _): _)
-      | ls@(_:_:_) <- map head $ group [length vs | FunAlt _ vs _ <- fs] -> fail $ "different number of arguments of " ++ snd n ++ " at " ++ showSIRange (fst n)
-      | any (== n) [n' | TypeFamily n' _ _ <- ds] -> return []
-      | otherwise -> return
-        [ Let n
-            (listToMaybe [t | PrecDef n' t <- ds, n' == n])
-            (listToMaybe [t | TypeAnn n' t <- ds, n' == n])
-            (map (fst . fst) vs)
-            (foldr (uncurry SLam) (compileGuardTrees par ulend lend ge
-                [ compilePatts (zip (map snd vs) $ reverse [0..length vs - 1]) gsx
-                | FunAlt _ vs gsx <- fs
-                ]) (map fst vs))
-        ]
+    fs@((FunAlt n vs _): _) -> case map head $ group [length vs | FunAlt _ vs _ <- fs] of
+        [num]
+          | num == 0 && length fs > 1 -> fail $ "redefined " ++ snd n ++ " at " ++ showSIRange (fst n)
+          | any (== n) [n' | TypeFamily n' _ _ <- ds] -> return []
+          | otherwise -> return
+            [ Let n
+                (listToMaybe [t | PrecDef n' t <- ds, n' == n])
+                (listToMaybe [t | TypeAnn n' t <- ds, n' == n])
+                (map (fst . fst) vs)
+                (foldr (uncurry SLam) (compileGuardTrees par ulend lend ge
+                    [ compilePatts (zip (map snd vs) $ reverse [0.. num - 1]) gsx
+                    | FunAlt _ vs gsx <- fs
+                    ]) (map fst vs))
+            ]
+        _ -> fail $ "different number of arguments of " ++ snd n ++ " at " ++ showSIRange (fst n)
     x -> return x
   where
     noTA x = ((Visible, Wildcard SType), x)
diff --git a/testdata/language-features/basic-values/redefine02.reject.wip.lc b/testdata/language-features/basic-values/redefine02.reject.lc
index 7510e602..7510e602 100644
--- a/testdata/language-features/basic-values/redefine02.reject.wip.lc
+++ b/testdata/language-features/basic-values/redefine02.reject.lc
diff --git a/testdata/language-features/basic-values/redefine02.reject.out b/testdata/language-features/basic-values/redefine02.reject.out
new file mode 100644
index 00000000..790b6e63
--- /dev/null
+++ b/testdata/language-features/basic-values/redefine02.reject.out
@@ -0,0 +1,3 @@
+"testdata/language-features/basic-values/redefine02.reject.lc" (line 3, column 9):
+expecting lowercase ident, uppercase ident or operator definition
+Invalid indentation.  Found a token at indentation 8.  Expecting a token at an indentation greater than or equal to 13.IndentStream {indentationState = IndentationState {minIndentation = 13, maxIndentation = 14, absMode = False, tokenRel = Ge}, tokenStream = ""} or Invalid indentation.  Found a token at indentation 8.  Expecting a token at an indentation greater than or equal to 12.IndentStream {indentationState = IndentationState {minIndentation = 12, maxIndentation = 12, absMode = False, tokenRel = Ge}, tokenStream = ""}
\ No newline at end of file
diff --git a/testdata/language-features/basic-values/redefine03.reject.wip.lc b/testdata/language-features/basic-values/redefine03.reject.lc
index 62e5705e..62e5705e 100644
--- a/testdata/language-features/basic-values/redefine03.reject.wip.lc
+++ b/testdata/language-features/basic-values/redefine03.reject.lc
diff --git a/testdata/language-features/basic-values/redefine03.reject.out b/testdata/language-features/basic-values/redefine03.reject.out
new file mode 100644
index 00000000..05f009e1
--- /dev/null
+++ b/testdata/language-features/basic-values/redefine03.reject.out
@@ -0,0 +1,4 @@
+"testdata/language-features/basic-values/redefine03.reject.lc" (line 4, column 1):
+unexpected end of input
+expecting ".", "%", character, literal string, float, "#", natural, "_", "'", lowercase ident, "(", uppercase ident, "[", List comprehension, "{", "let", "@", symbols, ":", backquoted, "::", "~", "->", "=>", "where", "data", "class", "instance", "type", "infix", "infixl", "infixr" or operator definition
+redefined x at testdata/language-features/basic-values/redefine03.reject.lc 2:9-2:10
\ No newline at end of file