From e04aaf75d97e53a24c381b98d58658ba3105cacb Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Mon, 19 Mar 2018 12:05:36 -0400
Subject: [PATCH] Fix #14934 by including axSub0R in typeNatCoAxiomRules
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
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 c3aea39678398fdf88166f30f0d01225a1874a32)
---
compiler/typecheck/TcTypeNats.hs | 84 +++++++++++++++++++
.../tests/typecheck/should_compile/Makefile | 5 ++
.../tests/typecheck/should_compile/T14934.hs | 9 ++
.../tests/typecheck/should_compile/T14934a.hs | 14 ++++
.../tests/typecheck/should_compile/all.T | 2 +
5 files changed, 114 insertions(+)
create mode 100644 testsuite/tests/typecheck/should_compile/T14934.hs
create mode 100644 testsuite/tests/typecheck/should_compile/T14934a.hs
diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index da9b8dff86cc..3e9865c854a5 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 a7780efb0f59..1bf561ae3df7 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 000000000000..581e93186ee1
--- /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 000000000000..3ba59ff97635
--- /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 f38a1ff90f3d..1ea388c84ca8 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'])
--
GitLab