Add regression test for #2349 (#4584)

idris-lang · Nov 6, 2018 · 1a7fa35 · 1a7fa35
1 parent c536a6e
commit 1a7fa35
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 1 deletion.
diff --git a/test/TestData.hs b/test/TestData.hs
@@ -182,7 +182,9 @@ testFamiliesData = [
 --       (  5, ANY  ),
       (  6, ANY  ),
       (  7, ANY  ),
-      (  8, ANY  )]),
+      (  8, ANY  ),
+--       (  9, ANY  ),
+      ( 10, ANY  )]),
   ("interpret",      "Interpret",
     [ (  1, ANY  ),
       (  2, ANY  ),

diff --git a/test/interfaces010/expected b/test/interfaces010/expected
diff --git a/test/interfaces010/interfaces010.idr b/test/interfaces010/interfaces010.idr
@@ -0,0 +1,12 @@
+module Test
+
+interface ListLike a where
+  Elem : Type
+  fromList : List Elem -> a
+
+data Silly = None | Cons Int Silly
+
+ListLike Silly where
+  Elem = Int
+  fromList [] = None
+  fromList (x :: xs) = Cons x (fromList xs)
diff --git a/test/interfaces010/run b/test/interfaces010/run
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces010.idr --check
+rm -f interfaces010 *.ibc