1 files changed, 42 insertions, 0 deletions
diff --git a/testsuite/tests/indexed-types/should_compile/T14162.hs b/testsuite/tests/indexed-types/should_compile/T14162.hs
new file mode 100644
index 0000000000..1eccbffc86
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T14162.hs
@@ -0,0 +1,42 @@
+{-# Language TypeOperators, KindSignatures, DataKinds, PolyKinds,
+             TypeFamilies, GADTs #-}
+
+module T14162 where
+
+import Data.Kind
+
+data SubList (a :: Maybe w) :: Type where
+  SubNil :: SubList 'Nothing
+
+data family Sing (a :: k)
+
+data instance Sing (x :: SubList ys) where
+  SSubNil :: Sing SubNil
+
+{-
+SubList :: forall (w::*). Maybe w -> *
+SubNil  :: forall (w::*). SubList w (Nothing w)
+
+wrkSubNil :: forall (w::*) (a :: Maybe w).
+             (a ~ Nothing w) =>
+             SubList w a
+
+Sing :: forall k. k -> *
+
+RepTc :: forall (w_aSy : *)
+                (ys_aRW :: Maybe w_aSy)
+                (x_aRX :: SubList w_aSy ys_aRW).
+                *
+
+axiom forall (w : *) (ys : Maybe w) (x : SubList ys).
+   Sing (SubList ys) (x : SubList ys) ~ RepTc w ys x
+
+data RepTc w ys x where
+  SSubNil :: RepTc w (Nothing w) (SubNil w)
+
+SSubNil :: forall (w :: *). Sing (SubList w (Nothing w)) (SubNil w)
+
+wrkSSubMil :: forall (w : *) (ys : Maybe w) (x : Sublist w ys).
+              () =>
+              RepTc w ys x
+-}