1 files changed, 48 insertions, 0 deletions
diff --git a/testsuite/tests/typecheck/should_compile/T16188.hs b/testsuite/tests/typecheck/should_compile/T16188.hs
new file mode 100644
index 0000000000..31144198a3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T16188.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T16188 where
+
+import Data.Kind (Type)
+import Data.Type.Bool (type (&&))
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: a ~> b) (x :: a) :: b
+data family Sing :: forall k. k -> Type
+
+data instance Sing :: Bool -> Type where
+  SFalse :: Sing False
+  STrue  :: Sing True
+
+(%&&) :: forall (x :: Bool) (y :: Bool).
+         Sing x -> Sing y -> Sing (x && y)
+SFalse %&& _ = SFalse
+STrue  %&& a = a
+
+data RegExp :: Type -> Type where
+  App :: RegExp t -> RegExp t -> RegExp t
+
+data instance Sing :: forall t. RegExp t -> Type where
+  SApp :: Sing re1 -> Sing re2 -> Sing (App re1 re2)
+
+data ReNotEmptySym0 :: forall t. RegExp t ~> Bool
+type instance Apply ReNotEmptySym0 r = ReNotEmpty r
+
+type family ReNotEmpty (r :: RegExp t) :: Bool where
+  ReNotEmpty (App re1 re2) = ReNotEmpty re1 && ReNotEmpty re2
+
+sReNotEmpty :: forall t (r :: RegExp t).
+               Sing r -> Sing (Apply ReNotEmptySym0 r :: Bool)
+sReNotEmpty (SApp sre1 sre2) = sReNotEmpty sre1 %&& sReNotEmpty sre2
+
+blah :: forall (t :: Type) (re :: RegExp t).
+        Sing re -> ()
+blah (SApp sre1 sre2)
+  = case (sReNotEmpty sre1, sReNotEmpty sre2) of
+      (STrue, STrue) -> ()