Add testcases inspired by Luke Maranget's pattern match serieswip/add-testcases

In his paper "Warnings for Pattern Matching", Luke Maranget describes
three series in his appendix for which GHC's pattern match checker
scaled very badly. We mostly avoid this now with !1752. This commit adds
regression tests for each of the series.

Fixes #17264.

5 files changed, 247 insertions, 0 deletions

diff --git a/testsuite/tests/pmcheck/should_compile/all.T b/testsuite/tests/pmcheck/should_compile/all.T
index 65f8710a7f..12bb009899 100644
--- a/testsuite/tests/pmcheck/should_compile/all.T
+++ b/testsuite/tests/pmcheck/should_compile/all.T
@@ -136,6 +136,37 @@ test('CaseOfKnownCon', [], compile,
 test('TooManyDeltas', [], compile,
      ['-fmax-pmcheck-models=0 -fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
 
+# Series (inspired) by Luke Maranget
+
+test('PmSeriesS',
+     [ collect_compiler_stats('bytes allocated',10),
+       pre_cmd('$PYTHON ./genS.py 10'),
+       extra_files(['genS.py']),
+     ],
+     multimod_compile,
+     ['S', '-v0'])
+test('PmSeriesT',
+     [ collect_compiler_stats('bytes allocated',10),
+       pre_cmd('$PYTHON ./genT.py 10'),
+       extra_files(['genT.py']),
+     ],
+     multimod_compile,
+     ['T', '-v0'])
+test('PmSeriesV',
+     [ collect_compiler_stats('bytes allocated',10),
+       pre_cmd('$PYTHON ./genV.py 6'),
+       extra_files(['genV.py']),
+     ],
+     multimod_compile,
+     ['V', '-v0'])
+test('PmSeriesG',
+     [ collect_compiler_stats('bytes allocated',10),
+       pre_cmd('./genG 20'),
+       extra_files(['genG']),
+     ],
+     multimod_compile,
+     ['G', '-v0'])
+
 # EmptyCase
 test('T10746', [], compile,
      ['-fwarn-incomplete-patterns -fwarn-overlapping-patterns'])
diff --git a/testsuite/tests/pmcheck/should_compile/genG b/testsuite/tests/pmcheck/should_compile/genG
new file mode 100755
index 0000000000..f5705213ec
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/genG
@@ -0,0 +1,40 @@
+#!/bin/sh
+
+SIZE=${1:-20}
+MODULE=G
+
+# See #17264.
+#
+# Generates a function with many guards, inspired by Luc Mangaret's S series
+#
+#   module G where
+#
+#   data T = A | B
+#
+#   f :: Int -> (T, T)
+#   f n = (A, A)
+#
+#   g :: ()
+#   g
+#     | (A, A) <- f 1 = ()
+#     | (A, A) <- f 2 = ()
+#     | (A, A) <- f 3 = ()
+#     | (A, A) <- f 4 = ()
+#
+# Note how each guard splits into 2 uncovered Deltas
+
+cat > $MODULE.hs <<END
+module $MODULE where
+
+data T = A | B
+
+f :: Int -> (T, T)
+f _ = (A, A)
+
+g :: ()
+g
+END
+
+for i in $(seq -w 1 $SIZE); do
+  echo "  | (A, A) <- f $i = ()" >> $MODULE.hs
+done
diff --git a/testsuite/tests/pmcheck/should_compile/genS.py b/testsuite/tests/pmcheck/should_compile/genS.py
new file mode 100755
index 0000000000..529401cbfc
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/genS.py
@@ -0,0 +1,72 @@
+#! /usr/bin/env python3
+
+# See #17264.
+#
+# Generates a module of Luc Maranget's S series
+#
+#   module S where
+#
+#   data T = A | B
+#
+#   s :: T -> T -> T -> T -> T -> T -> T -> T -> ()
+#   s A A _ _ _ _ _ _ = ()
+#   s _ _ A A _ _ _ _ = ()
+#   s _ _ _ _ A A _ _ = ()
+#   s _ _ _ _ _ _ A A = ()
+#   s A B A B A B A B = ()
+#
+# Note how each clause splits into 2 uncovered Deltas
+# The last clause isn't strictly necessary to exhibit
+# exponential behavior in our algorithm, but the number
+# of missing matches is 2^n-1, easily demonstrated by
+# looking at the missing matches for S_2:
+#
+#   B _ B _
+#   A B B _
+#   B _ A B
+
+import sys
+
+size = int(sys.argv[1]) if len(sys.argv) > 1 else 5
+
+a = 'A'
+b = 'B'
+wc = '_'
+
+def horiz_join(M, N):
+    return [ row_M + row_N for (row_M, row_N) in zip(M, N) ]
+
+def vert_join(M, N):
+    return M + N
+
+def n_cols(M):
+    return len(M[0])
+
+def s_rec(n):
+    if n == 1:
+        return [ [ a, a ] ]
+    s_sub = s_rec(n-1)
+    top_row = [ [ a, a ] + [ wc ]*n_cols(s_sub) ]
+    left_col = [ [ wc, wc ] ]*len(s_sub)
+    return vert_join(top_row, horiz_join(left_col, s_sub))
+
+def s(n):
+    return vert_join(s_rec(n), [ [ a, b ]*n ])
+
+def debug_print(M):
+    for row in M:
+        print("".join(row))
+
+def format_hs(M):
+    hdr = """module S where
+
+data T = A | B
+
+"""
+
+    fun = "s :: " + "T -> "*n_cols(M) + "()\n"
+    for row in M:
+        fun += "s " + " ".join(row) + "= ()\n"
+    return hdr + fun
+
+open("S.hs", "w").write(format_hs(s(size)))
diff --git a/testsuite/tests/pmcheck/should_compile/genT.py b/testsuite/tests/pmcheck/should_compile/genT.py
new file mode 100755
index 0000000000..a45374c7f4
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/genT.py
@@ -0,0 +1,49 @@
+#! /usr/bin/env python3
+
+import sys
+
+# See #17264.
+#
+# Generates a module of Luc Maranget's T series
+
+size = int(sys.argv[1]) if len(sys.argv) > 1 else 3
+
+a = 'A'
+b = 'B'
+wc = '_'
+
+def horiz_join(M, N):
+    return [ row_M + row_N for (row_M, row_N) in zip(M, N) ]
+
+def vert_join(M, N):
+    return M + N
+
+def n_cols(M):
+    return len(M[0])
+
+def t(n):
+    if n == 1:
+        return [ [ a ], [ b ] ]
+
+    t_sub = t(n-1)
+    left_col = [ [ wc ] ]*len(t_sub)
+    top_rows = [ [a]*n, [b]*n ]
+    return vert_join(top_rows, horiz_join(left_col, t_sub))
+
+def debug_print(M):
+    for row in M:
+        print("".join(row))
+
+def format_hs(M):
+    hdr = """module T where
+
+data T = A | B
+
+"""
+
+    fun = "t :: " + "T -> "*n_cols(M) + "()\n"
+    for row in M:
+        fun += "t " + " ".join(row) + "= ()\n"
+    return hdr + fun
+
+open("T.hs", "w").write(format_hs(t(size)))
diff --git a/testsuite/tests/pmcheck/should_compile/genV.py b/testsuite/tests/pmcheck/should_compile/genV.py
new file mode 100755
index 0000000000..0e7a076fe4
--- /dev/null
+++ b/testsuite/tests/pmcheck/should_compile/genV.py
@@ -0,0 +1,55 @@
+#! /usr/bin/env python3
+
+import sys
+
+# See #17264.
+#
+# Generates a module of Luc Maranget's V series
+
+size = int(sys.argv[1]) if len(sys.argv) > 1 else 3
+
+a = 'A'
+b = 'B'
+wc = '_'
+
+def horiz_join(M, N):
+    return [ row_M + row_N for (row_M, row_N) in zip(M, N) ]
+
+def vert_join(M, N):
+    return M + N
+
+def b_m(n):
+    if n == 1: return [ [ b ] ]
+    b_sub = b_m(n-1)
+    top_row = [ [ b ] + [ wc ]*len(b_sub) ]
+    left_col = [ [ wc ] ] * len(b_sub)
+    return vert_join(top_row, horiz_join(left_col, b_sub))
+
+def n_cols(M):
+    return len(M[0])
+
+def v(n):
+    if n == 1:
+        return [ [ a ], [ b ] ]
+    b_sub = b_m(n)
+    v_sub = v(n-1)
+    top_row = [ [ a ]*n + [ wc ]*n_cols(v_sub) ]
+    return vert_join(top_row, horiz_join(b_sub, v_sub))
+
+def debug_print(M):
+    for row in M:
+        print("".join(row))
+
+def format_hs(M):
+    hdr = """module V where
+
+data T = A | B
+
+"""
+
+    fun = "v :: " + "T -> "*n_cols(M) + "()\n"
+    for row in M:
+        fun += "v " + " ".join(row) + "= ()\n"
+    return hdr + fun
+
+open("V.hs", "w").write(format_hs(v(size)))