Commit c3aea396 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

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
parent e3588547
......@@ -1810,7 +1810,7 @@ tcIfaceCoAxiomRule :: IfLclName -> IfL CoAxiomRule
tcIfaceCoAxiomRule n
= case Map.lookup n typeNatCoAxiomRules of
Just ax -> return ax
_ -> pprPanic "go_axiom_rule" (ppr n)
_ -> pprPanic "tcIfaceCoAxiomRule" (ppr n)
tcIfaceDataCon :: Name -> IfL DataCon
tcIfaceDataCon name = do { thing <- tcIfaceGlobal name
......
{-# 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
......
......@@ -70,3 +70,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
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
module T14934 where
import T14934a
import GHC.TypeLits
g :: Foo (1 - 0)
g = f MkFoo1
{-# 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
......@@ -597,3 +597,5 @@ test('T14732', normal, compile, [''])
test('T14774', [], run_command, ['$MAKE -s --no-print-directory T14774'])
test('T14763', normal, compile, [''])
test('T14811', normal, compile, [''])
test('T14934', [extra_files(['T14934.hs', 'T14934a.hs'])], run_command,
['$MAKE -s --no-print-directory T14934'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment