Fix #14934 by including axSub0R in typeNatCoAxiomRules

For some reason, `axSub0R` was left out of `typeNatCoAxiomRules` in
`TcTypeNats`, which led to disaster when trying to look up `Sub0R` from
an interface file, as demonstrated in #14934.

The fix is simple—just add `axSub0R` to that list. To help prevent
an issue like this happening in the future, I added a
`Note [Adding built-in type families]` to `TcTypeNats`, which
contains a walkthrough of all the definitions in `TcTypeNats` you
need to update when adding a new built-in type family.

Test Plan: make test TEST=T14934

Reviewers: bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #14934

Differential Revision: https://phabricator.haskell.org/D4508

1 files changed, 84 insertions, 9 deletions

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index 139f62477f..24e12cd15c 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -1,19 +1,13 @@
 {-# LANGUAGE LambdaCase #-}
 
-{- Note [Type-level natural numbers]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See the Wiki page:
-
-    https://ghc.haskell.org/trac/ghc/wiki/TypeNats
-
-and Note [Adding built-in type families]
--}
-
 module TcTypeNats
   ( typeNatTyCons
   , 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
@@ -62,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
@@ -275,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
@@ -384,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
@@ -407,6 +481,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axCmpSymbolRefl
   , axLeq0L
   , axSubDef
+  , axSub0R
   , axAppendSymbol0R
   , axAppendSymbol0L
   , axDivDef