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

(cherry picked from commit c3aea396)

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

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

testsuite/tests/typecheck/should_compile/T14934.hs

+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+module T14934 where
+
+import T14934a
+import GHC.TypeLits
+
+g :: Foo (1 - 0)
+g = f MkFoo1

testsuite/tests/typecheck/should_compile/T14934a.hs

+{-# 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

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'])