diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,15 @@
 Changelog for singletons project
 ================================
 
+2.5.1
+-----
+* `ShowSing` is now a type class (with a single instance) instead of a type
+  synonym. This was changed because defining `ShowSing` as a type synonym
+  prevents it from working well with recursive types due to an unfortunate GHC
+  bug. For more information, see
+  [issue #371](https://github.com/goldfirere/singletons/issues/371).
+* Add an `IsString` instance for `SomeSing`.
+
 2.5
 ---
 * The `Data.Promotion.Prelude.*` namespace has been removed. Use the
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,5 @@
-singletons 2.5
-==============
+singletons 2.5.1
+================
 
 [![Hackage](https://img.shields.io/hackage/v/singletons.svg)](http://hackage.haskell.org/package/singletons)
 [![Build Status](https://travis-ci.org/goldfirere/singletons.svg?branch=master)](https://travis-ci.org/goldfirere/singletons)
@@ -33,6 +33,10 @@
 `Data.Maybe`, `Data.Either`, `Data.Tuple` and `Data.List`. See the promotion
 paper for a more thorough introduction.
 
+[This blog series](https://blog.jle.im/entry/introduction-to-singletons-1.html),
+authored by Justin Le, offers a tutorial for this library that assumes no
+knowledge of dependent types.
+
 Compatibility
 -------------
 
@@ -52,7 +56,6 @@
 * `KindSignatures`
 * `NoStarIsType`
 * `PolyKinds`
-* `QuantifiedConstraints`
 * `RankNTypes`
 * `ScopedTypeVariables`
 * `StandaloneDeriving`
diff --git a/singletons.cabal b/singletons.cabal
--- a/singletons.cabal
+++ b/singletons.cabal
@@ -1,5 +1,5 @@
 name:           singletons
-version:        2.5
+version:        2.5.1
                 -- Remember to bump version in the Makefile as well
 cabal-version:  >= 1.10
 synopsis:       A framework for generating singleton types
@@ -9,7 +9,7 @@
 maintainer:     Ryan Scott <ryan.gl.scott@gmail.com>
 bug-reports:    https://github.com/goldfirere/singletons/issues
 stability:      experimental
-tested-with:    GHC == 8.6.1
+tested-with:    GHC == 8.6.2
 extra-source-files: README.md, CHANGES.md,
                     tests/compile-and-dump/buildGoldenFiles.awk,
                     tests/compile-and-dump/GradingClient/*.hs,
@@ -38,7 +38,7 @@
 source-repository this
   type:     git
   location: https://github.com/goldfirere/singletons.git
-  tag:      v2.5
+  tag:      v2.5.1
 
 source-repository head
   type:     git
diff --git a/src/Data/Singletons.hs b/src/Data/Singletons.hs
--- a/src/Data/Singletons.hs
+++ b/src/Data/Singletons.hs
@@ -5,7 +5,6 @@
 {-# LANGUAGE MagicHash #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
@@ -86,12 +85,15 @@
 import Data.Singletons.Internal
 import Data.Singletons.Prelude.Enum
 import Data.Singletons.Prelude.Eq
+import Data.Singletons.Prelude.IsString
 import Data.Singletons.Prelude.Monoid
 import Data.Singletons.Prelude.Num
 import Data.Singletons.Prelude.Ord
 import Data.Singletons.Prelude.Semigroup
 import Data.Singletons.Promote
 import Data.Singletons.ShowSing
+import Data.String
+import qualified Data.Text as T (pack)
 
 ----------------------------------------------------------------------
 ---- SomeSing instances ----------------------------------------------
@@ -138,6 +140,9 @@
 
 instance SMonoid k => Monoid (SomeSing k) where
   mempty = SomeSing sMempty
+
+instance SIsString k => IsString (SomeSing k) where
+  fromString s = withSomeSing (T.pack s) (SomeSing . sFromString)
 
 ----------------------------------------------------------------------
 ---- Defunctionalization symbols -------------------------------------
diff --git a/src/Data/Singletons/Prelude/Monoid.hs b/src/Data/Singletons/Prelude/Monoid.hs
--- a/src/Data/Singletons/Prelude/Monoid.hs
+++ b/src/Data/Singletons/Prelude/Monoid.hs
@@ -4,7 +4,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
@@ -174,7 +173,6 @@
   -- deriving newtype instance Monoid a => Monoid (Down a)
   instance Monoid a => Monoid (Down a) where
       mempty = Down mempty
-      Down a `mappend` Down b = Down (a `mappend` b)
 
   -- deriving newtype instance Applicative First
   instance Applicative First where
diff --git a/src/Data/Singletons/Prelude/Semigroup.hs b/src/Data/Singletons/Prelude/Semigroup.hs
--- a/src/Data/Singletons/Prelude/Semigroup.hs
+++ b/src/Data/Singletons/Prelude/Semigroup.hs
@@ -4,7 +4,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TemplateHaskell #-}
diff --git a/src/Data/Singletons/ShowSing.hs b/src/Data/Singletons/ShowSing.hs
--- a/src/Data/Singletons/ShowSing.hs
+++ b/src/Data/Singletons/ShowSing.hs
@@ -29,7 +29,6 @@
   ShowSing
   ) where
 
-import Data.Kind
 import Data.Singletons.Internal
 import Data.Singletons.Prelude.Instances
 import Data.Singletons.Single
@@ -70,7 +69,7 @@
 -- @
 --
 -- Because that quantified constraint is somewhat lengthy, we provide the
--- 'ShowSing' type synonym as a convenient shorthand. Thus, the above instance
+-- 'ShowSing' class synonym as a convenient shorthand. Thus, the above instance
 -- is equivalent to:
 --
 -- @
@@ -87,7 +86,82 @@
 -- * A 'Show' instance for the singleton type
 --
 -- What a bargain!
-type ShowSing k = (forall z. Show (Sing (z :: k)) :: Constraint)
+class    (forall (z :: k). Show (Sing z)) => ShowSing k
+instance (forall (z :: k). Show (Sing z)) => ShowSing k
+
+{-
+Note [Define ShowSing as a class, not a type synonym]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In an ideal world, we would simply define ShowSing as an ordinary type synonym,
+like this:
+
+  type ShowSing k = (forall (z :: k). Show (Sing z) :: Constraint)
+
+In fact, I used to assume that we lived in an ideal world, so I defined
+ShowSing as a type synonym in version 2.5 of this library. However, I realized
+some time after 2.5's release that the world is far from ideal, unfortunately,
+and that this approach is unfeasible at the time being due to GHC Trac #15888.
+
+To be more precise, the exact issue involves an infelicity in the way
+QuantifiedConstraints interacts with recursive type class instances.
+Consider the following example (from #371):
+
+  $(singletons [d|
+    data X a = X1 | X2 (Y a) deriving Show
+    data Y a = Y1 | Y2 (X a) deriving Show
+    |])
+
+This will generate the following instances:
+
+  deriving instance ShowSing (Y a) => Show (Sing (z :: X a))
+  deriving instance ShowSing (X a) => Show (Sing (z :: Y a))
+
+So far, so good. Now, suppose you try to actually `show` a singleton for X.
+For example:
+
+  show (sing @(X1 :: X Bool))
+
+Somewhat surprisingly, this will be rejected by the typechecker with the
+following error:
+
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: Show (Sing z)
+
+To see why this happens, observe what goes on if we expand the occurrences of
+the ShowSing type synonym in the generated instances:
+
+  deriving instance (forall z. Show (Sing (z :: Y a))) => Show (Sing (z :: X a))
+  deriving instance (forall z. Show (Sing (z :: X a))) => Show (Sing (z :: Y a))
+
+Due to the way QuantifiedConstraints currently works (as surmised in Trac
+#15888), when GHC has a Wanted `Show (Sing X1 :: X Bool)` constraint, it
+chooses the appropriate instance and emits a Wanted
+`forall z. Show (Sing (z :: Y Bool))` constraint (from the instance context).
+GHC skolemizes the `z` to `z1` and tries to solve a Wanted
+`Show (Sing (z1 :: Y Bool))` constraint. GHC chooses the appropriate instance
+and emits a Wanted `forall z. Show (Sing (z :: X Bool))` constraint. GHC
+skolemizes the `z` to `z2` and tries to solve a Wanted
+`Show (Sing (z2 :: X Bool))` constraint... we repeat the process and find
+ourselves in an infinite loop that eventually overflows the reduction stack.
+Eep.
+
+Until Trac #15888 is fixed, there are two possible ways to work around this
+problem:
+
+1. Make derived instances' type inference more clever. If you look closely,
+   you'll notice that the `ShowSing (X a)`/`ShowSing (Y a)` constraints in
+   the generated instances are entirely redundant and could safely be left
+   off. But determining this would require significantly improving singletons'
+   Template Haskell capabilities for type inference, which is a path that we
+   usually spurn in favor of keeping the generated code dumb but predictable.
+2. Define `ShowSing` as a class (with a single instance) instead of a type
+   synonym. `ShowSing`-as-a-class ties the recursive knot during instance
+   resolution and thus avoids the problems that the type synonym version
+   currently suffers from.
+
+Given the two options, (2) is by far the easier option, so that is what we
+ultimately went with.
+-}
 
 ------------------------------------------------------------
 -- TypeLits instances
diff --git a/tests/SingletonsTestSuite.hs b/tests/SingletonsTestSuite.hs
--- a/tests/SingletonsTestSuite.hs
+++ b/tests/SingletonsTestSuite.hs
@@ -102,6 +102,7 @@
     , compileAndDumpStdTest "FunctorLikeDeriving"
     , compileAndDumpStdTest "T353"
     , compileAndDumpStdTest "T358"
+    , compileAndDumpStdTest "T371"
     ],
     testCompileAndDumpGroup "Promote"
     [ compileAndDumpStdTest "Constructors"
diff --git a/tests/SingletonsTestSuiteUtils.hs b/tests/SingletonsTestSuiteUtils.hs
--- a/tests/SingletonsTestSuiteUtils.hs
+++ b/tests/SingletonsTestSuiteUtils.hs
@@ -69,7 +69,6 @@
   , "-XTypeApplications"
   , "-XEmptyCase"
   , "-XNoStarIsType"
-  , "-XQuantifiedConstraints"
   ]
 
 -- Compile a test using specified GHC options. Save output to file, filter with
diff --git a/tests/compile-and-dump/Singletons/T358.ghc86.template b/tests/compile-and-dump/Singletons/T358.ghc86.template
--- a/tests/compile-and-dump/Singletons/T358.ghc86.template
+++ b/tests/compile-and-dump/Singletons/T358.ghc86.template
@@ -108,8 +108,10 @@
         forall b (t :: b). Sing t -> Sing (Apply Method2aSym0 t :: [a])
       sMethod2b ::
         forall b (t :: b). Sing t -> Sing (Apply Method2bSym0 t :: [a])
-      sMethod2a _ = Data.Singletons.Prelude.Instances.SNil
-      sMethod2b _ = Data.Singletons.Prelude.Instances.SNil
+      sMethod2a _
+        = Data.Singletons.Prelude.Instances.SNil
+      sMethod2b _
+        = Data.Singletons.Prelude.Instances.SNil
     instance SC2 a => SingI (Method2aSym0 :: (~>) b a) where
       sing = (singFun1 @Method2aSym0) sMethod2a
     instance SC2 a => SingI (Method2bSym0 :: (~>) b a) where
diff --git a/tests/compile-and-dump/Singletons/T371.ghc86.template b/tests/compile-and-dump/Singletons/T371.ghc86.template
new file mode 100644
--- /dev/null
+++ b/tests/compile-and-dump/Singletons/T371.ghc86.template
@@ -0,0 +1,233 @@
+Singletons/T371.hs:(0,0)-(0,0): Splicing declarations
+    singletons
+      [d| data Y (a :: Type)
+            = Y1 | Y2 (X a)
+            deriving Show
+          data X (a :: Type)
+            = X1 | X2 (Y a)
+            deriving Show |]
+  ======>
+    data X (a :: Type)
+      = X1 | X2 (Y a)
+      deriving Show
+    data Y (a :: Type)
+      = Y1 | Y2 (X a)
+      deriving Show
+    type X1Sym0 = X1
+    type X2Sym1 (t0123456789876543210 :: Y a0123456789876543210) =
+        X2 t0123456789876543210
+    instance SuppressUnusedWarnings X2Sym0 where
+      suppressUnusedWarnings = snd (((,) X2Sym0KindInference) ())
+    data X2Sym0 :: forall (a0123456789876543210 :: Type).
+                   (~>) (Y a0123456789876543210) (X (a0123456789876543210 :: Type))
+      where
+        X2Sym0KindInference :: forall t0123456789876543210
+                                      arg. SameKind (Apply X2Sym0 arg) (X2Sym1 arg) =>
+                               X2Sym0 t0123456789876543210
+    type instance Apply X2Sym0 t0123456789876543210 = X2 t0123456789876543210
+    type Y1Sym0 = Y1
+    type Y2Sym1 (t0123456789876543210 :: X a0123456789876543210) =
+        Y2 t0123456789876543210
+    instance SuppressUnusedWarnings Y2Sym0 where
+      suppressUnusedWarnings = snd (((,) Y2Sym0KindInference) ())
+    data Y2Sym0 :: forall (a0123456789876543210 :: Type).
+                   (~>) (X a0123456789876543210) (Y (a0123456789876543210 :: Type))
+      where
+        Y2Sym0KindInference :: forall t0123456789876543210
+                                      arg. SameKind (Apply Y2Sym0 arg) (Y2Sym1 arg) =>
+                               Y2Sym0 t0123456789876543210
+    type instance Apply Y2Sym0 t0123456789876543210 = Y2 t0123456789876543210
+    type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: X a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
+      ShowsPrec_0123456789876543210 _ X1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "X1") a_0123456789876543210
+      ShowsPrec_0123456789876543210 p_0123456789876543210 (X2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "X2 ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
+    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: X a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =
+        ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
+      suppressUnusedWarnings
+        = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
+    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: X a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol
+      where
+        ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
+                                                                 a0123456789876543210
+                                                                 a0123456789876543210
+                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
+                                                          ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
+      suppressUnusedWarnings
+        = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
+    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.
+                                                                                      (~>) (X a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)
+      where
+        ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
+                                                                 a0123456789876543210
+                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
+                                                          ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
+      suppressUnusedWarnings
+        = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
+    data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.
+                                              (~>) GHC.Types.Nat ((~>) (X a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
+      where
+        ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
+                                                                 arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
+                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
+    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
+    instance PShow (X a) where
+      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
+    type family ShowsPrec_0123456789876543210 (a :: GHC.Types.Nat) (a :: Y a) (a :: GHC.Types.Symbol) :: GHC.Types.Symbol where
+      ShowsPrec_0123456789876543210 _ Y1 a_0123456789876543210 = Apply (Apply ShowStringSym0 "Y1") a_0123456789876543210
+      ShowsPrec_0123456789876543210 p_0123456789876543210 (Y2 arg_0123456789876543210) a_0123456789876543210 = Apply (Apply (Apply ShowParenSym0 (Apply (Apply (>@#@$) p_0123456789876543210) (Data.Singletons.Prelude.Num.FromInteger 10))) (Apply (Apply (.@#@$) (Apply ShowStringSym0 "Y2 ")) (Apply (Apply ShowsPrecSym0 (Data.Singletons.Prelude.Num.FromInteger 11)) arg_0123456789876543210))) a_0123456789876543210
+    type ShowsPrec_0123456789876543210Sym3 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Y a0123456789876543210) (a0123456789876543210 :: GHC.Types.Symbol) =
+        ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) where
+      suppressUnusedWarnings
+        = snd (((,) ShowsPrec_0123456789876543210Sym2KindInference) ())
+    data ShowsPrec_0123456789876543210Sym2 (a0123456789876543210 :: GHC.Types.Nat) (a0123456789876543210 :: Y a0123456789876543210) :: (~>) GHC.Types.Symbol GHC.Types.Symbol
+      where
+        ShowsPrec_0123456789876543210Sym2KindInference :: forall a0123456789876543210
+                                                                 a0123456789876543210
+                                                                 a0123456789876543210
+                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym3 a0123456789876543210 a0123456789876543210 arg) =>
+                                                          ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    type instance Apply (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210 a0123456789876543210 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) where
+      suppressUnusedWarnings
+        = snd (((,) ShowsPrec_0123456789876543210Sym1KindInference) ())
+    data ShowsPrec_0123456789876543210Sym1 (a0123456789876543210 :: GHC.Types.Nat) :: forall a0123456789876543210.
+                                                                                      (~>) (Y a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol)
+      where
+        ShowsPrec_0123456789876543210Sym1KindInference :: forall a0123456789876543210
+                                                                 a0123456789876543210
+                                                                 arg. SameKind (Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) arg) (ShowsPrec_0123456789876543210Sym2 a0123456789876543210 arg) =>
+                                                          ShowsPrec_0123456789876543210Sym1 a0123456789876543210 a0123456789876543210
+    type instance Apply (ShowsPrec_0123456789876543210Sym1 a0123456789876543210) a0123456789876543210 = ShowsPrec_0123456789876543210Sym2 a0123456789876543210 a0123456789876543210
+    instance SuppressUnusedWarnings ShowsPrec_0123456789876543210Sym0 where
+      suppressUnusedWarnings
+        = snd (((,) ShowsPrec_0123456789876543210Sym0KindInference) ())
+    data ShowsPrec_0123456789876543210Sym0 :: forall a0123456789876543210.
+                                              (~>) GHC.Types.Nat ((~>) (Y a0123456789876543210) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
+      where
+        ShowsPrec_0123456789876543210Sym0KindInference :: forall a0123456789876543210
+                                                                 arg. SameKind (Apply ShowsPrec_0123456789876543210Sym0 arg) (ShowsPrec_0123456789876543210Sym1 arg) =>
+                                                          ShowsPrec_0123456789876543210Sym0 a0123456789876543210
+    type instance Apply ShowsPrec_0123456789876543210Sym0 a0123456789876543210 = ShowsPrec_0123456789876543210Sym1 a0123456789876543210
+    instance PShow (Y a) where
+      type ShowsPrec a a a = Apply (Apply (Apply ShowsPrec_0123456789876543210Sym0 a) a) a
+    data instance Sing :: X a -> Type
+      where
+        SX1 :: Sing X1
+        SX2 :: forall a (n :: Y a). (Sing (n :: Y a)) -> Sing (X2 n)
+    type SX = (Sing :: X a -> Type)
+    instance SingKind a => SingKind (X a) where
+      type Demote (X a) = X (Demote a)
+      fromSing SX1 = X1
+      fromSing (SX2 b) = X2 (fromSing b)
+      toSing X1 = SomeSing SX1
+      toSing (X2 (b :: Demote (Y a)))
+        = case toSing b :: SomeSing (Y a) of {
+            SomeSing c -> SomeSing (SX2 c) }
+    data instance Sing :: Y a -> Type
+      where
+        SY1 :: Sing Y1
+        SY2 :: forall a (n :: X a). (Sing (n :: X a)) -> Sing (Y2 n)
+    type SY = (Sing :: Y a -> Type)
+    instance SingKind a => SingKind (Y a) where
+      type Demote (Y a) = Y (Demote a)
+      fromSing SY1 = Y1
+      fromSing (SY2 b) = Y2 (fromSing b)
+      toSing Y1 = SomeSing SY1
+      toSing (Y2 (b :: Demote (X a)))
+        = case toSing b :: SomeSing (X a) of {
+            SomeSing c -> SomeSing (SY2 c) }
+    instance SShow (Y a) => SShow (X a) where
+      sShowsPrec ::
+        forall (t1 :: GHC.Types.Nat) (t2 :: X a) (t3 :: GHC.Types.Symbol).
+        Sing t1
+        -> Sing t2
+           -> Sing t3
+              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (X a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
+                                                             -> Type) t1) t2) t3)
+      sShowsPrec
+        _
+        SX1
+        (sA_0123456789876543210 :: Sing a_0123456789876543210)
+        = (applySing
+             ((applySing ((singFun2 @ShowStringSym0) sShowString))
+                (sing :: Sing "X1")))
+            sA_0123456789876543210
+      sShowsPrec
+        (sP_0123456789876543210 :: Sing p_0123456789876543210)
+        (SX2 (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
+        (sA_0123456789876543210 :: Sing a_0123456789876543210)
+        = (applySing
+             ((applySing
+                 ((applySing ((singFun3 @ShowParenSym0) sShowParen))
+                    ((applySing
+                        ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
+                       (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
+                ((applySing
+                    ((applySing ((singFun3 @(.@#@$)) (%.)))
+                       ((applySing ((singFun2 @ShowStringSym0) sShowString))
+                          (sing :: Sing "X2 "))))
+                   ((applySing
+                       ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
+                          (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))
+                      sArg_0123456789876543210))))
+            sA_0123456789876543210
+    instance SShow (X a) => SShow (Y a) where
+      sShowsPrec ::
+        forall (t1 :: GHC.Types.Nat) (t2 :: Y a) (t3 :: GHC.Types.Symbol).
+        Sing t1
+        -> Sing t2
+           -> Sing t3
+              -> Sing (Apply (Apply (Apply (ShowsPrecSym0 :: TyFun GHC.Types.Nat ((~>) (Y a) ((~>) GHC.Types.Symbol GHC.Types.Symbol))
+                                                             -> Type) t1) t2) t3)
+      sShowsPrec
+        _
+        SY1
+        (sA_0123456789876543210 :: Sing a_0123456789876543210)
+        = (applySing
+             ((applySing ((singFun2 @ShowStringSym0) sShowString))
+                (sing :: Sing "Y1")))
+            sA_0123456789876543210
+      sShowsPrec
+        (sP_0123456789876543210 :: Sing p_0123456789876543210)
+        (SY2 (sArg_0123456789876543210 :: Sing arg_0123456789876543210))
+        (sA_0123456789876543210 :: Sing a_0123456789876543210)
+        = (applySing
+             ((applySing
+                 ((applySing ((singFun3 @ShowParenSym0) sShowParen))
+                    ((applySing
+                        ((applySing ((singFun2 @(>@#@$)) (%>))) sP_0123456789876543210))
+                       (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 10)))))
+                ((applySing
+                    ((applySing ((singFun3 @(.@#@$)) (%.)))
+                       ((applySing ((singFun2 @ShowStringSym0) sShowString))
+                          (sing :: Sing "Y2 "))))
+                   ((applySing
+                       ((applySing ((singFun3 @ShowsPrecSym0) sShowsPrec))
+                          (Data.Singletons.Prelude.Num.sFromInteger (sing :: Sing 11))))
+                      sArg_0123456789876543210))))
+            sA_0123456789876543210
+    deriving instance Data.Singletons.ShowSing.ShowSing (Y a) =>
+                      Show (Sing (z :: X a))
+    deriving instance Data.Singletons.ShowSing.ShowSing (X a) =>
+                      Show (Sing (z :: Y a))
+    instance SingI X1 where
+      sing = SX1
+    instance SingI n => SingI (X2 (n :: Y a)) where
+      sing = SX2 sing
+    instance SingI (X2Sym0 :: (~>) (Y a) (X (a :: Type))) where
+      sing = (singFun1 @X2Sym0) SX2
+    instance SingI (TyCon1 X2 :: (~>) (Y a) (X (a :: Type))) where
+      sing = (singFun1 @(TyCon1 X2)) SX2
+    instance SingI Y1 where
+      sing = SY1
+    instance SingI n => SingI (Y2 (n :: X a)) where
+      sing = SY2 sing
+    instance SingI (Y2Sym0 :: (~>) (X a) (Y (a :: Type))) where
+      sing = (singFun1 @Y2Sym0) SY2
+    instance SingI (TyCon1 Y2 :: (~>) (X a) (Y (a :: Type))) where
+      sing = (singFun1 @(TyCon1 Y2)) SY2
diff --git a/tests/compile-and-dump/Singletons/T371.hs b/tests/compile-and-dump/Singletons/T371.hs
new file mode 100644
--- /dev/null
+++ b/tests/compile-and-dump/Singletons/T371.hs
@@ -0,0 +1,16 @@
+module T371 where
+
+import Data.Kind
+import Data.Singletons.TH
+
+$(singletons [d|
+  data X (a :: Type) = X1 | X2 (Y a) deriving Show
+  data Y (a :: Type) = Y1 | Y2 (X a) deriving Show
+  |])
+
+main :: IO ()
+main = do
+  print (sing :: Sing ('[] :: [Bool]))
+  print (sing :: Sing '[True])
+  print (sing :: Sing (X1 :: X Bool))
+  print (sing :: Sing (Y2 X1 :: Y Bool))