Add test files

tests/idris2/reg028/Test.idr

@@ -0,0 +1,16 @@
+module Test
+
+data Dummy : (lbl : Type) -> (st : List lbl) -> Type -> Type where
+  MkDummy : a -> Dummy b st a
+
+
+public export
+interface IxPure (f : (lbl : Type) -> (st : List lbl) -> Type -> Type)
+          where
+  ixPure : a -> f lbl st a
+
+IxPure Dummy where
+  ixPure = MkDummy
+
+pure12 : Dummy String xs Nat
+pure12 = ixPure Z

tests/idris2/reg028/expected

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

tests/idris2/reg028/run

@@ -0,0 +1,3 @@
+$1 --check Test.idr
+
+rm -rf build