diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index da9b8dff86cc30b70a5ce39fa4c76ed30007b076..3e9865c854a5d127906b6c85cb4a6ae75c6d6de1 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -5,6 +5,9 @@ module TcTypeNats
   , typeNatCoAxiomRules
   , BuiltInSynFamily(..)
 
+    -- If you define a new built-in type family, make sure to export its TyCon
+    -- from here as well.
+    -- See Note [Adding built-in type families]
   , typeNatAddTyCon
   , typeNatMulTyCon
   , typeNatExpTyCon
@@ -53,10 +56,86 @@ import Data.Maybe ( isJust )
 import Control.Monad ( guard )
 import Data.List  ( isPrefixOf, isSuffixOf )
 
+{-
+Note [Type-level literals]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are currently two forms of type-level literals: natural numbers, and
+symbols (even though this module is named TcTypeNats, it covers both).
+
+Type-level literals are supported by CoAxiomRules (conditional axioms), which
+power the built-in type families (see Note [Adding built-in type families]).
+Currently, all built-in type families are for the express purpose of supporting
+type-level literals.
+
+See also the Wiki page:
+
+    https://ghc.haskell.org/trac/ghc/wiki/TypeNats
+
+Note [Adding built-in type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+There are a few steps to adding a built-in type family:
+
+* Adding a unique for the type family TyCon
+
+  These go in PrelNames. It will likely be of the form
+  @myTyFamNameKey = mkPreludeTyConUnique xyz@, where @xyz@ is a number that
+  has not been chosen before in PrelNames. There are several examples already
+  in PrelNames—see, for instance, typeNatAddTyFamNameKey.
+
+* Adding the type family TyCon itself
+
+  This goes in TcTypeNats. There are plenty of examples of how to define
+  these—see, for instance, typeNatAddTyCon.
+
+  Once your TyCon has been defined, be sure to:
+
+  - Export it from TcTypeNats. (Not doing so caused #14632.)
+  - Include it in the typeNatTyCons list, defined in TcTypeNats.
+
+* Exposing associated type family axioms
+
+  When defining the type family TyCon, you will need to define an axiom for
+  the type family in general (see, for instance, axAddDef), and perhaps other
+  auxiliary axioms for special cases of the type family (see, for instance,
+  axAdd0L and axAdd0R).
+
+  After you have defined all of these axioms, be sure to include them in the
+  typeNatCoAxiomRules list, defined in TcTypeNats.
+  (Not doing so caused #14934.)
+
+* Define the type family somewhere
+
+  Finally, you will need to define the type family somewhere, likely in @base@.
+  Currently, all of the built-in type families are defined in GHC.TypeLits or
+  GHC.TypeNats, so those are likely candidates.
+
+  Since the behavior of your built-in type family is specified in TcTypeNats,
+  you should give an open type family definition with no instances, like so:
+
+    type family MyTypeFam (m :: Nat) (n :: Nat) :: Nat
+
+  Changing the argument and result kinds as appropriate.
+
+* Update the relevant test cases
+
+  The GHC test suite will likely need to be updated after you add your built-in
+  type family. For instance:
+
+  - The T9181 test prints the :browse contents of GHC.TypeLits, so if you added
+    a test there, the expected output of T9181 will need to change.
+  - The TcTypeNatSimple and TcTypeSymbolSimple tests have compile-time unit
+    tests, as well as TcTypeNatSimpleRun and TcTypeSymbolSimpleRun, which have
+    runtime unit tests. Consider adding further unit tests to those if your
+    built-in type family deals with Nats or Symbols, respectively.
+-}
+
 {-------------------------------------------------------------------------------
 Built-in type constructors for functions on type-level nats
 -}
 
+-- The list of built-in type family TyCons that GHC uses.
+-- If you define a built-in type family, make sure to add it to this list.
+-- See Note [Adding built-in type families]
 typeNatTyCons :: [TyCon]
 typeNatTyCons =
   [ typeNatAddTyCon
@@ -266,6 +345,7 @@ Built-in rules axioms
 
 -- If you add additional rules, please remember to add them to
 -- `typeNatCoAxiomRules` also.
+-- See Note [Adding built-in type families]
 axAddDef
   , axMulDef
   , axExpDef
@@ -375,6 +455,9 @@ axAppendSymbol0R  = mkAxiom1 "Concat0R"
 axAppendSymbol0L  = mkAxiom1 "Concat0L"
             $ \(Pair s t) -> (s `appendSymbol` mkStrLitTy nilFS) === t
 
+-- The list of built-in type family axioms that GHC uses.
+-- If you define new axioms, make sure to include them in this list.
+-- See Note [Adding built-in type families]
 typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
 typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   [ axAddDef
@@ -398,6 +481,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axCmpSymbolRefl
   , axLeq0L
   , axSubDef
+  , axSub0R
   , axAppendSymbol0R
   , axAppendSymbol0L
   , axDivDef
diff --git a/testsuite/tests/typecheck/should_compile/Makefile b/testsuite/tests/typecheck/should_compile/Makefile
index a7780efb0f591702a1de4ed3f421b55ca7bfaf99..1bf561ae3df7d81bafa0e0e3d3fcc3b9cfc8164d 100644
--- a/testsuite/tests/typecheck/should_compile/Makefile
+++ b/testsuite/tests/typecheck/should_compile/Makefile
@@ -66,3 +66,8 @@ T13585:
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T13585a.hs -O
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T13585b.hs -O
 	'$(TEST_HC)' $(TEST_HC_OPTS) -c T13585.hs  -O
+
+T14934:
+	$(RM) -f T14934a.o T14934a.hi T14934.o T14934.hi
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T14934a.hs -O
+	'$(TEST_HC)' $(TEST_HC_OPTS) -c T14934.hs  -O
diff --git a/testsuite/tests/typecheck/should_compile/T14934.hs b/testsuite/tests/typecheck/should_compile/T14934.hs
new file mode 100644
index 0000000000000000000000000000000000000000..581e93186ee10ac688a06bc39a2ecb64fd803572
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14934.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T14934 where
+
+import T14934a
+import GHC.TypeLits
+
+g :: Foo (1 - 0)
+g = f MkFoo1
diff --git a/testsuite/tests/typecheck/should_compile/T14934a.hs b/testsuite/tests/typecheck/should_compile/T14934a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..3ba59ff9763572ed76fcb3ade0a0a2c0384613ff
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T14934a.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+module T14934a where
+
+import GHC.TypeLits
+
+data Foo :: Nat -> * where
+  MkFoo0 :: Foo 0
+  MkFoo1 :: Foo 1
+
+f :: Foo (1 - 0) -> Foo 1
+f x = x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index f38a1ff90f3d660b07bd50a31c9f8fc73b9964d0..1ea388c84ca887545515538fe3e65c6565f246c9 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -593,3 +593,5 @@ test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutio
 test('T14732', normal, compile, [''])
 test('T14763', normal, compile, [''])
 test('T14811', normal, compile, [''])
+test('T14934', [extra_files(['T14934.hs', 'T14934a.hs'])], run_command,
+               ['$MAKE -s --no-print-directory T14934'])