From c3aea39678398fdf88166f30f0d01225a1874a32 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 19 Mar 2018 12:05:36 -0400 Subject: 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 --- compiler/typecheck/TcTypeNats.hs | 93 ++++++++++++++++++++++++++++++++++++---- 1 file changed, 84 insertions(+), 9 deletions(-) (limited to 'compiler/typecheck/TcTypeNats.hs') 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 -- cgit v1.2.1