update to current master againwip/T13904

1 files changed, 34 insertions, 0 deletions

diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.hs b/testsuite/tests/partial-sigs/should_fail/T14040a.hs
new file mode 100644
index 0000000000..2985339f49
--- /dev/null
+++ b/testsuite/tests/partial-sigs/should_fail/T14040a.hs
@@ -0,0 +1,34 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds, PolyKinds #-}
+module T14040a where
+
+import Data.Kind
+
+data family Sing (a :: k)
+
+data WeirdList :: Type -> Type where
+  WeirdNil  :: WeirdList a
+  WeirdCons :: a -> WeirdList (WeirdList a) -> WeirdList a
+
+data instance Sing (z :: WeirdList a) where
+  SWeirdNil  :: Sing WeirdNil
+  SWeirdCons :: Sing w -> Sing wws -> Sing (WeirdCons w wws)
+
+elimWeirdList :: forall (a :: Type) (wl :: WeirdList a)
+                        (p :: forall (x :: Type). x -> WeirdList x -> Type).
+                 Sing wl
+              -> (forall (y :: Type). p _ WeirdNil)
+              -> (forall (z :: Type) (x :: z) (xs :: WeirdList (WeirdList z)).
+                    Sing x -> Sing xs -> p _ xs
+                  -> p _ (WeirdCons x xs))
+              -> p _ wl
+elimWeirdList SWeirdNil pWeirdNil _ = pWeirdNil
+elimWeirdList (SWeirdCons (x :: Sing (x :: z))
+                          (xs :: Sing (xs :: WeirdList (WeirdList z))))
+              pWeirdNil pWeirdCons
+  = pWeirdCons @z @x @xs x xs
+      (elimWeirdList @(WeirdList z) @xs @p xs pWeirdNil pWeirdCons)