Add 'type family (m :: Symbol) <> (n :: Symbol)'

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

8 files changed, 67 insertions, 3 deletions

diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index 43bbbacd74..2e149d31d2 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -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
index 0000000000..85daeae73b
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/TcTypeSymbolSimple.hs
@@ -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 _ = ()
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c5e9163bbe..465d8acf9d 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -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, [''])
diff --git a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
index 4098b3c667..fb1463cc86 100644
--- a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
+++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.hs
@@ -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/TcTypeNatSimpleRun.stdout b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
index 9adb27b5bc..74c592960e 100644
--- a/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
+++ b/testsuite/tests/typecheck/should_run/TcTypeNatSimpleRun.stdout
@@ -1 +1 @@
-[True,True,True,True,True]
+[True,True,True,True,True,True,True]
diff --git a/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.hs b/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.hs
new file mode 100644
index 0000000000..518d4e523c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.hs
@@ -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
index 0000000000..dfe7f46481
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/TcTypeSymbolSimpleRun.stdout
@@ -0,0 +1 @@
+[True,True]
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index ac63f98508..ff138e4e4d 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -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, [''])