diff --git a/README.md b/README.md
index 92f0c7e3..a33fabce 100644
--- a/README.md
+++ b/README.md
@@ -1585,6 +1585,7 @@ The following constructs are either unsupported or almost never work:
 * `{-# UNPACK #-}` pragmas
 * partial application of the `(->)` type
 * invisible type patterns
+* `AllowAmbiguousTypes`
 
 See the following sections for more details.
 
@@ -1783,3 +1784,16 @@ f @t x = x :: t
 
 See [this `singletons`
 issue](https://github.com/goldfirere/singletons/issues/583).
+
+### `AllowAmbiguousTypes`
+
+`singletons-th` does not currently support promoting or singling types with
+ambiguous type variables, which require the `AllowAmbiguousTypes` language
+extension to define. For instance, `singletons-th` does not support definitions
+such as this one:
+
+```hs
+{-# LANGUAGE AllowAmbiguousTypes #-}
+class HasName a where
+  name :: String -- This type is ambiguous
+```
diff --git a/singletons-base/src/Data/Functor/Compose/Singletons.hs b/singletons-base/src/Data/Functor/Compose/Singletons.hs
index eedf3f9a..1b3bf820 100644
--- a/singletons-base/src/Data/Functor/Compose/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Compose/Singletons.hs
@@ -36,45 +36,15 @@ import Data.Functor.Singletons
 import Data.Ord.Singletons
 import Data.Kind
 import Data.Semigroup.Singletons
-import Data.Singletons
 import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Traversable.Singletons
 
-{-
-In order to keep the type arguments to Compose poly-kinded and with inferred
-specificities, we define the singleton version of Compose, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-infixr 9 `SCompose`
-type SCompose :: Compose f g a -> Type
-data SCompose :: Compose f g a -> Type where
-  SCompose :: forall f g a (x :: f (g a)).
-              Sing x -> SCompose ('Compose @f @g @a x)
-type instance Sing @(Compose f g a) = SCompose
-instance SingI x => SingI ('Compose x) where
-  sing = SCompose sing
-instance SingI1 'Compose where
-  liftSing = SCompose
-
-infixr 9 `ComposeSym0`
-type ComposeSym0 :: f (g a) ~> Compose f g a
-data ComposeSym0 z
-type instance Apply ComposeSym0 x = 'Compose x
-instance SingI ComposeSym0 where
-  sing = singFun1 SCompose
-
-infixr 9 `ComposeSym1`
-type ComposeSym1 :: f (g a) -> Compose f g a
-type family ComposeSym1 x where
-  ComposeSym1 x = 'Compose x
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Compose]))
 
 $(singletonsOnly [d|
-  getCompose :: Compose f g a -> f (g a)
-  getCompose (Compose x) = x
-
   deriving instance Eq (f (g a)) => Eq (Compose f g a)
   deriving instance Ord (f (g a)) => Ord (Compose f g a)
 
diff --git a/singletons-base/src/Data/Functor/Const/Singletons.hs b/singletons-base/src/Data/Functor/Const/Singletons.hs
index 58cdb5d9..e5d2694d 100644
--- a/singletons-base/src/Data/Functor/Const/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Const/Singletons.hs
@@ -32,73 +32,28 @@ import Control.Applicative
 import Control.Monad.Singletons.Internal
 import Data.Eq.Singletons
 import Data.Foldable.Singletons
-import Data.Kind (Type)
 import Data.Monoid.Singletons
 import Data.Ord.Singletons
 import Data.Semigroup.Singletons.Internal.Classes
-import Data.Singletons
 import Data.Singletons.Base.Instances hiding (FoldlSym0, sFoldl)
 import Data.Singletons.Base.Enum
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import GHC.Base.Singletons
   hiding ( Const, ConstSym0, ConstSym1
          , Foldr, FoldrSym0, sFoldr )
 import GHC.Num.Singletons
 import Text.Show.Singletons
 
-{-
-Const's argument `b` is poly-kinded, and as a result, we have a choice as to
-what singleton type to give it. We could use either
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Const]))
 
-1. type SConst :: forall {k :: Type} (a :: Type) (b :: k).    Const a b -> Type
-2. type SConst :: forall             (a :: Type) (b :: Type). Const a b -> Type
-
-Option (1) is the more permissive one, so we opt for that. However, singletons-th's
-TH machinery does not jive with this option, since the SingKind instance it
-tries to generate:
-
-  instance (SingKind a, SingKind b) => SingKind (Const a b) where
-    type Demote (Const a b) = Const (Demote a) (Demote b)
-
-Assumes that `b` is of kind Type. Until we get a more reliable story for
-poly-kinded Sing instances (see #150), we simply write the singleton type by
-hand.
-
-Note that we cannot use genSingletons to generate this code because we
-would end up with the wrong specificity for the kind of `a` when singling the
-Const constructor. See Note [Preserve the order of type variables during
-singling] in D.S.TH.Single.Type, wrinkle 2. Similarly, we must define the
-defunctionalization symbols for the Const data constructor by hand to get the
-specificities right.
--}
-type SConst :: Const a b -> Type
-data SConst :: Const a b -> Type where
-  SConst :: forall {k} a (b :: k) (x :: a).
-            Sing x -> SConst ('Const @a @b x)
-type instance Sing @(Const a b) = SConst
 instance SingKind a => SingKind (Const a b) where
   type Demote (Const a b) = Const (Demote a) b
   fromSing (SConst sa) = Const (fromSing sa)
   toSing (Const a) = withSomeSing a $ SomeSing . SConst
-instance SingI a => SingI ('Const a) where
-  sing = SConst sing
-instance SingI1 'Const where
-  liftSing = SConst
-
-type ConstSym0 :: a ~> Const a b
-data ConstSym0 z
-type instance Apply ConstSym0 x = 'Const x
-instance SingI ConstSym0 where
-  sing = singFun1 SConst
-
-type ConstSym1 :: a -> Const a b
-type family ConstSym1 x where
-  ConstSym1 x = 'Const x
 
 $(singletonsOnly [d|
-  getConst :: Const a b -> a
-  getConst (Const x) = x
-
   deriving instance Bounded a => Bounded (Const a b)
   deriving instance Eq      a => Eq      (Const a b)
   deriving instance Ord     a => Ord     (Const a b)
diff --git a/singletons-base/src/Data/Functor/Product/Singletons.hs b/singletons-base/src/Data/Functor/Product/Singletons.hs
index 8c056070..a4858f97 100644
--- a/singletons-base/src/Data/Functor/Product/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Product/Singletons.hs
@@ -42,46 +42,12 @@ import Data.Monoid.Singletons hiding (SProduct(..))
 import Data.Semigroup.Singletons hiding (SProduct(..))
 import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
 import Data.Ord.Singletons
-import Data.Singletons
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Traversable.Singletons
 
-{-
-In order to keep the type arguments to Product poly-kinded and with inferred
-specificities, we define the singleton version of Product, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-type SProduct :: Product f g a -> Type
-data SProduct :: Product f g a -> Type where
-  SPair :: forall f g a (x :: f a) (y :: g a).
-           Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)
-type instance Sing @(Product f g a) = SProduct
-instance (SingI x, SingI y) => SingI ('Pair x y) where
-  sing = SPair sing sing
-instance SingI x => SingI1 ('Pair x) where
-  liftSing = SPair sing
-instance SingI2 'Pair where
-  liftSing2 = SPair
-
-type PairSym0 :: forall f g a. f a ~> g a ~> Product f g a
-data PairSym0 z
-type instance Apply PairSym0 x = PairSym1 x
-instance SingI PairSym0 where
-  sing = singFun2 SPair
-
-type PairSym1 :: forall f g a. f a -> g a ~> Product f g a
-data PairSym1 fa z
-type instance Apply (PairSym1 x) y = 'Pair x y
-instance SingI x => SingI (PairSym1 x) where
-  sing = singFun1 $ SPair (sing @x)
-instance SingI1 PairSym1 where
-  liftSing s = singFun1 $ SPair s
-
-type PairSym2 :: forall f g a. f a -> g a -> Product f g a
-type family PairSym2 x y where
-  PairSym2 x y = 'Pair x y
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Product]))
 
 $(singletonsOnly [d|
   deriving instance (Eq (f a), Eq (g a)) => Eq (Product f g a)
diff --git a/singletons-base/src/Data/Functor/Sum/Singletons.hs b/singletons-base/src/Data/Functor/Sum/Singletons.hs
index 2056447b..2e9c584b 100644
--- a/singletons-base/src/Data/Functor/Sum/Singletons.hs
+++ b/singletons-base/src/Data/Functor/Sum/Singletons.hs
@@ -32,56 +32,15 @@ import Data.Eq.Singletons
 import Data.Foldable.Singletons hiding (Sum)
 import Data.Functor.Singletons
 import Data.Functor.Sum
-import Data.Kind
 import Data.Ord.Singletons
 import Data.Semigroup.Singletons hiding (SSum(..))
-import Data.Singletons
 import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Traversable.Singletons
 
-{-
-In order to keep the type arguments to Sum poly-kinded and with inferred
-specificities, we define the singleton version of Sum, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-type SSum :: Sum f g a -> Type
-data SSum :: Sum f g a -> Type where
-  SInL :: forall f g a (x :: f a).
-          Sing x -> SSum ('InL @f @g @a x)
-  SInR :: forall f g a (y :: g a).
-          Sing y -> SSum ('InR @f @g @a y)
-type instance Sing @(Sum f g a) = SSum
-instance SingI x => SingI ('InL x) where
-  sing = SInL sing
-instance SingI1 'InL where
-  liftSing = SInL
-instance SingI y => SingI ('InR y) where
-  sing = SInR sing
-instance SingI1 'InR where
-  liftSing = SInR
-
-type InLSym0 :: forall f g a. f a ~> Sum f g a
-data InLSym0 z
-type instance Apply InLSym0 x = 'InL x
-instance SingI InLSym0 where
-  sing = singFun1 SInL
-
-type InLSym1 :: forall f g a. f a -> Sum f g a
-type family InLSym1 x where
-  InLSym1 x = 'InL x
-
-type InRSym0 :: forall f g a. g a ~> Sum f g a
-data InRSym0 z
-type instance Apply InRSym0 y = 'InR y
-instance SingI InRSym0 where
-  sing = singFun1 SInR
-
-type InRSym1 :: forall f g a. g a -> Sum f g a
-type family InRSym1 x where
-  InRSym1 y = 'InR y
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Sum]))
 
 $(singletonsOnly [d|
   deriving instance (Eq (f a), Eq (g a)) => Eq (Sum f g a)
diff --git a/singletons-base/src/Data/Proxy/Singletons.hs b/singletons-base/src/Data/Proxy/Singletons.hs
index 0cad9048..43383f9c 100644
--- a/singletons-base/src/Data/Proxy/Singletons.hs
+++ b/singletons-base/src/Data/Proxy/Singletons.hs
@@ -32,17 +32,16 @@ import Control.Applicative
 import Control.Monad
 import Control.Monad.Singletons.Internal
 import Data.Eq.Singletons
-import Data.Kind
 import Data.Monoid.Singletons
 import Data.Ord.Singletons
 import Data.Proxy
 import Data.Semigroup (Semigroup(..))
 import Data.Semigroup.Singletons.Internal.Classes
 import Data.Singletons.Decide
-import Data.Singletons
 import Data.Singletons.Base.Enum
 import Data.Singletons.Base.Instances
 import Data.Singletons.TH
+import Data.Singletons.TH.Options
 import Data.Type.Coercion
 import Data.Type.Equality hiding (type (==))
 import GHC.Base.Singletons
@@ -50,27 +49,13 @@ import GHC.Num.Singletons
 import GHC.TypeLits.Singletons.Internal
 import Text.Show.Singletons
 
-{-
-In order to keep the type argument to Proxy poly-kinded and with an inferred
-specificity, we define the singleton version of Proxy, as well as its
-defunctionalization symbols, by hand. This is very much in the spirit of the
-code in Data.Functor.Const.Singletons. (See the comments above SConst in that
-module for more details on this choice.)
--}
-type SProxy :: Proxy t -> Type
-data SProxy :: Proxy t -> Type where
-  SProxy :: forall t. SProxy ('Proxy @t)
-type instance Sing @(Proxy t) = SProxy
+$(withOptions defaultOptions{genSingKindInsts = False}
+    (genSingletons [''Proxy]))
+
 instance SingKind (Proxy t) where
   type Demote (Proxy t) = Proxy t
   fromSing SProxy = Proxy
   toSing Proxy = SomeSing SProxy
-instance SingI 'Proxy where
-  sing = SProxy
-
-type ProxySym0 :: Proxy t
-type family ProxySym0 where
-  ProxySym0 = 'Proxy
 
 instance Eq (SProxy z) where
   _ == _ = True
diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs
index e327f9d6..17a00494 100644
--- a/singletons-base/tests/SingletonsBaseTestSuite.hs
+++ b/singletons-base/tests/SingletonsBaseTestSuite.hs
@@ -150,6 +150,7 @@ tests =
     , compileAndDumpStdTest "T555"
     , compileAndDumpStdTest "T559"
     , compileAndDumpStdTest "T563"
+    , compileAndDumpStdTest "T565"
     , compileAndDumpStdTest "T567"
     , compileAndDumpStdTest "T571"
     , compileAndDumpStdTest "T581"
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T565.golden b/singletons-base/tests/compile-and-dump/Singletons/T565.golden
new file mode 100644
index 00000000..b3fe9409
--- /dev/null
+++ b/singletons-base/tests/compile-and-dump/Singletons/T565.golden
@@ -0,0 +1,16 @@
+Singletons/T565.hs:(0,0)-(0,0): Splicing declarations
+    singletons [d| data C a where D :: forall {a}. C a |]
+  ======>
+    data C a where D :: forall {a}. C a
+    type DSym0 :: forall {a}. C a
+    type family DSym0 :: C a where
+      DSym0 = D
+    data SC :: forall a. C a -> Type
+      where SD :: forall {a}. SC (D :: C a)
+    type instance Sing @(C a) = SC
+    instance SingKind a => SingKind (C a) where
+      type Demote (C a) = C (Demote a)
+      fromSing SD = D
+      toSing D = SomeSing SD
+    instance SingI D where
+      sing = SD
diff --git a/singletons-base/tests/compile-and-dump/Singletons/T565.hs b/singletons-base/tests/compile-and-dump/Singletons/T565.hs
new file mode 100644
index 00000000..deb21007
--- /dev/null
+++ b/singletons-base/tests/compile-and-dump/Singletons/T565.hs
@@ -0,0 +1,8 @@
+module T565 where
+
+import Data.Singletons.TH
+
+$(singletons [d|
+  data C a where
+    D :: forall {a}. C a
+  |])
diff --git a/singletons-th/src/Data/Singletons/TH/Single/Data.hs b/singletons-th/src/Data/Singletons/TH/Single/Data.hs
index 5c92c644..2b71ce91 100644
--- a/singletons-th/src/Data/Singletons/TH/Single/Data.hs
+++ b/singletons-th/src/Data/Singletons/TH/Single/Data.hs
@@ -231,7 +231,7 @@ singCtor dataName (DCon con_tvbs cxt name fields rty)
                   (foldType pCon indices `DSigT` rty'))
                   -- Make sure to include an explicit `rty'` kind annotation.
                   -- See Note [Preserve the order of type variables during singling],
-                  -- wrinkle 3, in D.S.TH.Single.Type.
+                  -- wrinkle 2, in D.S.TH.Single.Type.
   where
     mk_source_unpackedness :: SourceUnpackedness -> SgM SourceUnpackedness
     mk_source_unpackedness su = case su of
diff --git a/singletons-th/src/Data/Singletons/TH/Single/Type.hs b/singletons-th/src/Data/Singletons/TH/Single/Type.hs
index 27f7d1a4..09805389 100644
--- a/singletons-th/src/Data/Singletons/TH/Single/Type.hs
+++ b/singletons-th/src/Data/Singletons/TH/Single/Type.hs
@@ -36,7 +36,7 @@ singType prom ty = do
       res'  = singFamily `DAppT` (foldType prom (map DVarT arg_names) `DSigT` prom_res)
                 -- Make sure to include an explicit `prom_res` kind annotation.
                 -- See Note [Preserve the order of type variables during singling],
-                -- wrinkle 3.
+                -- wrinkle 2.
       arg_tvbs = zipWith (`DKindedTV` SpecifiedSpec) arg_names prom_args
       -- If the original type signature lacks an explicit `forall`, then do not
       -- give the singled type signature an outermost `forall`. Instead, give it
@@ -204,56 +204,7 @@ Some further complications:
       SMkT :: forall a (x :: a). Sing x -> ST (MkT x)
 
 -----
--- Wrinkle 2: The TH reification swamp
------
-
-There is another issue with type signatures that lack explicit `forall`s, one
-which the current design of Template Haskell does not make simple to fix.
-If we single code that is wrapped in TH quotes, such as in the following example:
-
-  {-# LANGUAGE PolyKinds, ... #-}
-  $(singletons [d|
-    data Proxy a = MkProxy
-    |])
-
-Then our job is made much easier when singling MkProxy, since we know that the
-only type variable that must be quantified is `a`, as that is the only one
-specified by the user. This results in the following type signature for
-MkProxy:
-
-  MkProxy :: forall a. Proxy a
-
-However, this is not the only possible way to single MkProxy. One can
-alternatively use $(genSingletons [''Proxy]), which uses TH reification to
-infer the type of MkProxy. There is perilous, however, because this is how
-TH reifies Proxy:
-
-  DataD
-    [] ''Proxy [KindedTV a () (VarT k)] Nothing
-    [NormalC 'MkProxy []]
-    []
-
-We must then construct a type signature for MkProxy using nothing but the type
-variables from the data type header. But notice that `KindedTV a () (VarT k)`
-gives no indication of whether `k` is specified or inferred! As a result, we
-conservatively assume that `k` is specified, resulting the following type
-signature for MkProxy:
-
-  MkProxy :: forall k (a :: k). Proxy a
-
-Contrast this with `MkProxy :: Proxy a`, where `k` is inferred. In other words,
-if you single MkProxy using genSingletons, then `Proxy @True` will typecheck
-but `SMkProxy @True` will /not/ typecheck—you'd have to use
-`SMkProxy @_ @True` instead. Urk!
-
-At present, Template Haskell does not have a way to distinguish among the
-specificities bound by a data type header. Without this knowledge, it is
-unclear how one could work around this issue. Thankfully, this issue is
-only likely to surface in very limited circumstances, so the damage is somewhat
-minimal.
-
------
--- Wrinkle 3: Where to put explicit kind annotations
+-- Wrinkle 2: Where to put explicit kind annotations
 -----
 
 Type variable binders are only part of the story—we must also determine what
@@ -304,28 +255,49 @@ instead:
   SNothing :: forall a. SMaybe (Nothing @a)
 
 This does work for many cases, but there are also some corner cases where this
-approach fails. Recall the `MkProxy` example from Wrinkle 2 above:
-
-  {-# LANGUAGE PolyKinds, ... #-}
-  data Proxy a = MkProxy
-  $(genSingletons [''Proxy])
-
-Due to the design of Template Haskell (discussed in Wrinkle 2), `MkProxy` will
-be reified with the type of `forall k (a :: k). Proxy a`. This means that
-if we used visible kind applications in the result type, we would end up with
-this:
-
-  SMkProxy :: forall k (a :: k). SProxy (MkProxy @k @a)
-
-This will not kind-check because MkProxy only accepts /one/ visible kind argument,
-whereas this supplies it with two. To avoid this issue, we instead use the type
-`forall k (a :: k). SProxy (MkProxy :: Proxy a)`. Granted, this type is /still/
-technically wrong due to the fact that it explicitly quantifies `k`, but at the
-very least it typechecks. If Template Haskell gained the ability to distinguish
-among the specificities of type variables bound by a data type header
-(perhaps by way of a language feature akin to
-https://github.com/ghc-proposals/ghc-proposals/pull/326), then we could revisit
-this design choice.
+approach fails. Suppose that `Nothing` was declared like so:
+
+  Nothing :: forall {a}. Maybe a
+
+Then we couldn't write `Nothing @a`, as `a` wouldn't be eligible for visible
+kind application. (GHC Core would let you write `Nothing @{a}`, but this isn't
+possible in source Haskell.) As such, the only way to fix the type of `a` in
+`Maybe a` would be to write `Nothing :: Maybe a`.
+
+An even more obscure corner case is when a type quantifies a type variable
+without mentioning it at all in the rest of the type, e.g.,
+
+  C :: forall a. D
+
+At present, singletons-th does not handle this type of corner case at all. It
+wouldn't suffice to single `C` to the following:
+
+  SC :: forall a. SD (C :: D)
+
+This is because the `a` argument to `C` is left ambiguous in the type `C :: D`,
+as the return kind `D` doesn't indicate what `a` should be. In theory, we
+/could/ write `C @a :: D` instead, which would solve that particular problem.
+But there would still be trouble on the horizon, as there are other types of
+code that singletons-th generates which exhibit similar sorts of ambiguity. For
+example, here is the defunctionalization symbol that singletons-th would
+generate for `C`:
+
+  type CSym0 :: forall a. D
+  type family CSym0 @a :: D where
+    CSym0 = C
+
+GHC will reject this type family equation, also for ambiguity-related reasons:
+
+  error: [GHC-16220]
+      • Uninferrable type variables k0, (a0 :: k0) in
+        the type family equation right-hand side: C @{k0} @a0
+      • In the type family declaration for ‘CSym0’
+
+This is fixable, but we would need to audit all potential sources of type
+variable-related ambiguity in singletons-th–generated code and make sure that
+we have covered our bases. Given that types such as `forall a. D` are rare in
+practice, I'm inclined not to worry about this unless someone specifically asks
+for this featurette.
 
 Finally, note that we need only write `Sing x_1 -> ... -> Sing x_p`, and not
 `Sing (x_1 :: PT_1) -> ... Sing (x_p :: PT_p)`. This is simply because we