Add 'type family (m :: Symbol) <> (n :: Symbol)'
authorOleg Grenrus <oleg.grenrus@iki.fi>
Thu, 19 Jan 2017 20:19:25 +0000 (15:19 -0500)
committerBen Gamari <ben@smart-cactus.org>
Fri, 20 Jan 2017 18:42:56 +0000 (13:42 -0500)
Reviewers: dfeuer, austin, bgamari, hvr

Subscribers: dfeuer, mpickering, RyanGlScott, ekmett, yav, lelf,
simonpj, thomie

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

GHC Trac Issues: #12162

13 files changed:
compiler/prelude/PrelNames.hs
compiler/typecheck/TcTypeNats.hs
docs/users_guide/8.2.1-notes.rst
libraries/base/GHC/TypeLits.hs
libraries/base/changelog.md
testsuite/tests/ghci/scripts/T9181.stdout
testsuite/tests/typecheck/should_compile/TcTypeSymbolSimple.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T
testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.stdout [new file with mode: 0644]
testsuite/tests/typecheck/should_run/all.T

index fcddcdb..4d28ba3 100644 (file)
@@ -1769,6 +1769,9 @@ callStackTyConKey = mkPreludeTyConUnique 183
 typeRepTyConKey :: Unique
 typeRepTyConKey = mkPreludeTyConUnique 184
 
+typeSymbolAppendFamNameKey :: Unique
+typeSymbolAppendFamNameKey = mkPreludeTyConUnique 185
+
 ---------------- Template Haskell -------------------
 --      THNames.hs: USES TyConUniques 200-299
 -----------------------------------------------------
index d01ffee..6aff38a 100644 (file)
@@ -12,6 +12,7 @@ module TcTypeNats
   , typeNatSubTyCon
   , typeNatCmpTyCon
   , typeSymbolCmpTyCon
+  , typeSymbolAppendTyCon
   ) where
 
 import Type
@@ -33,10 +34,14 @@ import PrelNames  ( gHC_TYPELITS
                   , typeNatSubTyFamNameKey
                   , typeNatCmpTyFamNameKey
                   , typeSymbolCmpTyFamNameKey
+                  , typeSymbolAppendFamNameKey
+                  )
+import FastString ( FastString
+                  , fsLit, nilFS, nullFS, unpackFS, mkFastString, appendFS
                   )
-import FastString ( FastString, fsLit )
 import qualified Data.Map as Map
 import Data.Maybe ( isJust )
+import Data.List  ( isPrefixOf, isSuffixOf )
 
 {-------------------------------------------------------------------------------
 Built-in type constructors for functions on type-level nats
@@ -51,6 +56,7 @@ typeNatTyCons =
   , typeNatSubTyCon
   , typeNatCmpTyCon
   , typeSymbolCmpTyCon
+  , typeSymbolAppendTyCon
   ]
 
 typeNatAddTyCon :: TyCon
@@ -154,6 +160,16 @@ typeSymbolCmpTyCon =
     , sfInteractInert = \_ _ _ _ -> []
     }
 
+typeSymbolAppendTyCon :: TyCon
+typeSymbolAppendTyCon = mkTypeSymbolFunTyCon2 name
+  BuiltInSynFamily
+    { sfMatchFam      = matchFamAppendSymbol
+    , sfInteractTop   = interactTopAppendSymbol
+    , sfInteractInert = interactInertAppendSymbol
+    }
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "AppendSymbol")
+                typeSymbolAppendFamNameKey typeSymbolAppendTyCon
 
 
 
@@ -169,6 +185,16 @@ mkTypeNatFunTyCon2 op tcb =
     Nothing
     NotInjective
 
+-- Make a binary built-in constructor of kind: Symbol -> Symbol -> Symbol
+mkTypeSymbolFunTyCon2 :: Name -> BuiltInSynFamily -> TyCon
+mkTypeSymbolFunTyCon2 op tcb =
+  mkFamilyTyCon op
+    (mkTemplateAnonTyConBinders [ typeSymbolKind, typeSymbolKind ])
+    typeSymbolKind
+    Nothing
+    (BuiltInSynFamTyCon tcb)
+    Nothing
+    NotInjective
 
 
 {-------------------------------------------------------------------------------
@@ -183,6 +209,7 @@ axAddDef
   , axLeqDef
   , axCmpNatDef
   , axCmpSymbolDef
+  , axAppendSymbolDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -198,6 +225,8 @@ axAddDef
   , axLeq0L
   , axSubDef
   , axSub0R
+  , axAppendSymbol0R
+  , axAppendSymbol0L
   :: CoAxiomRule
 
 axAddDef = mkBinAxiom "AddDef" typeNatAddTyCon $
@@ -222,10 +251,23 @@ axCmpSymbolDef =
     , coaxrRole      = Nominal
     , coaxrProves    = \cs ->
         do [Pair s1 s2, Pair t1 t2] <- return cs
-           [s2', t2'] <- traverse isStrLitTy [s2, t2]
+           s2' <- isStrLitTy s2
+           t2' <- isStrLitTy t2
            return (mkTyConApp typeSymbolCmpTyCon [s1,t1] ===
                    ordering (compare s2' t2')) }
 
+axAppendSymbolDef = CoAxiomRule
+    { coaxrName      = fsLit "AppendSymbolDef"
+    , coaxrAsmpRoles = [Nominal, Nominal]
+    , coaxrRole      = Nominal
+    , coaxrProves    = \cs ->
+        do [Pair s1 s2, Pair t1 t2] <- return cs
+           s2' <- isStrLitTy s2
+           t2' <- isStrLitTy t2
+           let z = mkStrLitTy (appendFS s2' t2')
+           return (mkTyConApp typeSymbolAppendTyCon [s1, t1] === z)
+    }
+
 axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon $
               \x y -> fmap num (minus x y)
 
@@ -245,6 +287,10 @@ axCmpNatRefl    = mkAxiom1 "CmpNatRefl"
 axCmpSymbolRefl = mkAxiom1 "CmpSymbolRefl"
                 $ \(Pair s _) -> (cmpSymbol s s) === ordering EQ
 axLeq0L     = mkAxiom1 "Leq0L"    $ \(Pair s _) -> (num 0 <== s) === bool True
+axAppendSymbol0R  = mkAxiom1 "Concat0R"
+            $ \(Pair s t) -> (mkStrLitTy nilFS `appendSymbol` s) === t
+axAppendSymbol0L  = mkAxiom1 "Concat0L"
+            $ \(Pair s t) -> (s `appendSymbol` mkStrLitTy nilFS) === t
 
 typeNatCoAxiomRules :: Map.Map FastString CoAxiomRule
 typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
@@ -254,6 +300,7 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axLeqDef
   , axCmpNatDef
   , axCmpSymbolDef
+  , axAppendSymbolDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -268,6 +315,8 @@ typeNatCoAxiomRules = Map.fromList $ map (\x -> (coaxrName x, x))
   , axCmpSymbolRefl
   , axLeq0L
   , axSubDef
+  , axAppendSymbol0R
+  , axAppendSymbol0L
   ]
 
 
@@ -297,6 +346,9 @@ cmpNat s t = mkTyConApp typeNatCmpTyCon [s,t]
 cmpSymbol :: Type -> Type -> Type
 cmpSymbol s t = mkTyConApp typeSymbolCmpTyCon [s,t]
 
+appendSymbol :: Type -> Type -> Type
+appendSymbol s t = mkTyConApp typeSymbolAppendTyCon [s, t]
+
 (===) :: Type -> Type -> Pair Type
 x === y = Pair x y
 
@@ -352,8 +404,9 @@ mkBinAxiom str tc f =
     , coaxrRole      = Nominal
     , coaxrProves    = \cs ->
         do [Pair s1 s2, Pair t1 t2] <- return cs
-           [s2', t2'] <- traverse isNumLitTy [s2, t2]
-           z          <- f s2' t2'
+           s2' <- isNumLitTy s2
+           t2' <- isNumLitTy t2
+           z   <- f s2' t2'
            return (mkTyConApp tc [s1,t1] === z)
     }
 
@@ -444,6 +497,16 @@ matchFamCmpSymbol [s,t]
         mbY = isStrLitTy t
 matchFamCmpSymbol _ = Nothing
 
+matchFamAppendSymbol :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamAppendSymbol [s,t]
+  | Just x <- mbX, nullFS x = Just (axAppendSymbol0R, [t], t)
+  | Just y <- mbY, nullFS y = Just (axAppendSymbol0L, [s], s)
+  | Just x <- mbX, Just y <- mbY =
+    Just (axAppendSymbolDef, [s,t], mkStrLitTy (appendFS x y))
+  where
+  mbX = isStrLitTy s
+  mbY = isStrLitTy t
+matchFamAppendSymbol _ = Nothing
 
 {-------------------------------------------------------------------------------
 Interact with axioms
@@ -542,8 +605,26 @@ interactTopCmpSymbol [s,t] r
   | Just EQ <- isOrderingLitTy r = [ s === t ]
 interactTopCmpSymbol _ _ = []
 
+interactTopAppendSymbol :: [Xi] -> Xi -> [Pair Type]
+interactTopAppendSymbol [s,t] r
+  -- (AppendSymbol a b ~ "") => (a ~ "", b ~ "")
+  | Just z <- mbZ, nullFS z =
+    [s === mkStrLitTy nilFS, t === mkStrLitTy nilFS ]
+
+  -- (AppendSymbol "foo" b ~ "foobar") => (b ~ "bar")
+  | Just x <- fmap unpackFS mbX, Just z <- fmap unpackFS mbZ, x `isPrefixOf` z =
+    [ t === mkStrLitTy (mkFastString $ drop (length x) z) ]
+
+  -- (AppendSymbol f "bar" ~ "foobar") => (f ~ "foo")
+  | Just y <- fmap unpackFS mbY, Just z <- fmap unpackFS mbZ, y `isSuffixOf` z =
+    [ t === mkStrLitTy (mkFastString $ take (length z - length y) z) ]
 
+  where
+  mbX = isStrLitTy s
+  mbY = isStrLitTy t
+  mbZ = isStrLitTy r
 
+interactTopAppendSymbol _ _ = []
 
 {-------------------------------------------------------------------------------
 Interaction with inerts
@@ -592,9 +673,12 @@ interactInertLeq [x1,y1] z1 [x2,y2] z2
 interactInertLeq _ _ _ _ = []
 
 
-
-
-
+interactInertAppendSymbol :: [Xi] -> Xi -> [Xi] -> Xi -> [Pair Type]
+interactInertAppendSymbol [x1,y1] z1 [x2,y2] z2
+  | sameZ && tcEqType x1 x2         = [ y1 === y2 ]
+  | sameZ && tcEqType y1 y2         = [ x1 === x2 ]
+  where sameZ = tcEqType z1 z2
+interactInertAppendSymbol _ _ _ _ = []
 
 
 
index c5e3cb6..094fce9 100644 (file)
@@ -226,6 +226,9 @@ See ``changelog.md`` in the ``base`` package for full release notes.
   provided in GHC's version of the ``Read`` class, and allows users to write
   more efficient ``Read1`` and ``Read2`` instances.
 
+- Add ``type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol`` to
+  ``GHC.TypeLits``
+
 binary
 ~~~~~~
 
index 6d66c11..41cf523 100644 (file)
@@ -35,6 +35,7 @@ module GHC.TypeLits
 
     -- * Functions on type literals
   , type (<=), type (<=?), type (+), type (*), type (^), type (-)
+  , AppendSymbol
   , CmpNat, CmpSymbol
 
   -- * User-defined type errors
@@ -203,6 +204,10 @@ type family (m :: Nat) ^ (n :: Nat) :: Nat
 -- @since 4.7.0.0
 type family (m :: Nat) - (n :: Nat) :: Nat
 
+-- | Concatenation of type-level symbols.
+--
+-- @since 4.10.0.0
+type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
 
 -- | A description of a custom type error.
 data {-kind-} ErrorMessage = Text Symbol
index f1a93ee..608830a 100644 (file)
@@ -40,6 +40,9 @@
 
   * Add `plusForeignPtr` to `Foreign.ForeignPtr`.
 
+  * Add `type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol` to `GHC.TypeLits`
+    (#12162)
+
 ## 4.9.0.0  *May 2016*
 
   * Bundled with GHC 8.0
index 43bbbac..2e149d3 100644 (file)
@@ -12,6 +12,9 @@ type (GHC.TypeLits.<=) (x :: GHC.Types.Nat) (y :: GHC.Types.Nat) =
 type family (GHC.TypeLits.<=?) (a :: GHC.Types.Nat)
                                (b :: GHC.Types.Nat)
             :: Bool
+type family GHC.TypeLits.AppendSymbol (a :: GHC.Types.Symbol)
+                                      (b :: GHC.Types.Symbol)
+            :: GHC.Types.Symbol
 type family GHC.TypeLits.CmpNat (a :: GHC.Types.Nat)
                                 (b :: GHC.Types.Nat)
             :: Ordering
diff --git a/testsuite/tests/typecheck/should_compile/TcTypeSymbolSimple.hs b/testsuite/tests/typecheck/should_compile/TcTypeSymbolSimple.hs
new file mode 100644 (file)
index 0000000..85daeae
--- /dev/null
@@ -0,0 +1,28 @@
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
+module TcTypeNatSimple where
+import GHC.TypeLits
+import Data.Proxy
+
+--------------------------------------------------------------------------------
+-- Test evaluation
+
+te1 :: Proxy (AppendSymbol "" x) -> Proxy x
+te1 = id
+
+te2 :: Proxy (AppendSymbol x "") -> Proxy x
+te2 = id
+
+te3 :: Proxy (AppendSymbol "type" "level") -> Proxy "typelevel"
+te3 = id
+
+--------------------------------------------------------------------------------
+-- Test interactions with inerts
+
+tei1 :: Proxy (AppendSymbol y x) -> Proxy x -> ()
+tei1 _ _ = ()
+
+tei2 :: Proxy (AppendSymbol "foo" x) -> ()
+tei2 _ = ()
+
+tei3 :: Proxy (AppendSymbol x "foo") -> ()
+tei3 _ = ()
index c5e9163..465d8ac 100644 (file)
@@ -427,6 +427,7 @@ test('T7888', normal, compile, [''])
 test('T7891', normal, compile, [''])
 test('T7903', normal, compile, [''])
 test('TcTypeNatSimple', normal, compile, [''])
+test('TcTypeSymbolSimple', normal, compile, [''])
 test('TcCoercibleCompile', [], compile, [''])
 test('T8392', normal, compile, [''])
 test('T8474', normal, compile, [''])
index 4098b3c..fb1463c 100644 (file)
@@ -9,9 +9,15 @@ import Data.Proxy
 tsub :: Proxy (x + y) -> Proxy y -> Proxy x
 tsub _ _ = Proxy
 
+tsub2 :: Proxy (x + y) -> (Proxy x, Proxy y)
+tsub2 _ = (Proxy, Proxy)
+
 tdiv :: Proxy (x * y) -> Proxy y -> Proxy x
 tdiv _ _ = Proxy
 
+tdiv2 :: Proxy (x * y) -> (Proxy x, Proxy y)
+tdiv2 _ = (Proxy, Proxy)
+
 troot :: Proxy (x ^ y) -> Proxy y -> Proxy x
 troot _ _ = Proxy
 
@@ -23,12 +29,14 @@ tleq _ = Proxy
 
 main :: IO ()
 main = print [ sh (tsub  (Proxy :: Proxy 5) (Proxy :: Proxy 3)) == "2"
+             , let (p, q) = tsub2 (Proxy :: Proxy 0)
+               in (sh p, sh q) == ("0", "0")
              , sh (tdiv  (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "4"
+             , let (p, q) = tdiv2 (Proxy :: Proxy 1)
+               in (sh p, sh q) == ("1", "1")
              , sh (troot (Proxy :: Proxy 9) (Proxy :: Proxy 2)) == "3"
              , sh (tlog  (Proxy :: Proxy 8) (Proxy :: Proxy 2)) == "3"
              , sh (tleq  (Proxy :: Proxy 0))                    == "0"
              ]
   where
   sh x = show (natVal x)
-
-
diff --git a/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.hs b/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.hs
new file mode 100644 (file)
index 0000000..518d4e5
--- /dev/null
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
+module Main(main) where
+import GHC.TypeLits
+import Data.Proxy
+
+--------------------------------------------------------------------------------
+-- Test top-reactions
+
+tappend :: Proxy (AppendSymbol x y) -> Proxy x -> Proxy y
+tappend _ _ = Proxy
+
+tappend2 :: Proxy (AppendSymbol x y) -> (Proxy x, Proxy y)
+tappend2 _ = (Proxy, Proxy)
+
+main :: IO ()
+main = print [ symbolVal (tappend (Proxy :: Proxy "abc") (Proxy :: Proxy "ab"))
+               == "c"
+             , let (p, q) = tappend2 (Proxy :: Proxy "")
+               in (symbolVal p, symbolVal q) == ("", "")
+             ]
+  where
+  sh x = show (natVal x)
diff --git a/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.stdout b/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.stdout
new file mode 100644 (file)
index 0000000..dfe7f46
--- /dev/null
@@ -0,0 +1 @@
+[True,True]
index ac63f98..ff138e4 100755 (executable)
@@ -102,6 +102,7 @@ test('T5913', normal, compile_and_run, [''])
 test('T7748', normal, compile_and_run, [''])
 test('T7861', [omit_ways('debug'), exit_code(1)], compile_and_run, [''])
 test('TcTypeNatSimpleRun', normal, compile_and_run, [''])
+test('TcTypeSymbolSimpleRun', normal, compile_and_run, [''])
 test('T8119', normal, ghci_script, ['T8119.script'])
 test('T8492', normal, compile_and_run, [''])
 test('T8739', normal, compile_and_run, [''])