[commit: ghc] ghc-8.2: Add regression test for #13538 (4f9e73f)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-8.2
Link       : http://ghc.haskell.org/trac/ghc/changeset/4f9e73f1529224d42c1d90c7bf8efad3c9e44cd8/ghc

>---------------------------------------------------------------

commit 4f9e73f1529224d42c1d90c7bf8efad3c9e44cd8
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Thu Apr 6 16:42:39 2017 -0400

    Add regression test for #13538
    
    Commit 2b64e926a628fb2a3710b0360123ea73331166fe (#13135) ended
    up fixing #13538 as well. Let's add a regression test so that it stays
    fixed.
    
    Test Plan: make test TEST=T13538
    
    Reviewers: austin, bgamari
    
    Reviewed By: bgamari
    
    Subscribers: rwbarton, thomie
    
    GHC Trac Issues: #13538
    
    Differential Revision: https://phabricator.haskell.org/D3426
    
    (cherry picked from commit e61900c994334c209a9de763993716314abf9f6d)


>---------------------------------------------------------------

4f9e73f1529224d42c1d90c7bf8efad3c9e44cd8
 testsuite/tests/dependent/should_compile/T13538.hs | 45 ++++++++++++++++++++++
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 46 insertions(+)

diff --git a/testsuite/tests/dependent/should_compile/T13538.hs b/testsuite/tests/dependent/should_compile/T13538.hs
new file mode 100644
index 0000000..f9d904f
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13538.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies, TypeFamilyDependencies #-}
+{-# LANGUAGE KindSignatures, DataKinds, PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeApplications     #-}
+module T13538 where
+
+import GHC.TypeLits
+import Data.Proxy
+
+-- | Synonym for a type-level snoc (injective!)
+type (ns :: [k]) +: (n :: k) = GetList1 (SinkFirst (n ': ns))
+infixl 5 +:
+
+
+
+-- | A weird data type used to make `(+:)` operation injective.
+--   `List k [k]` must have at least two elements.
+data List1 k = L1Single k | L1Head k [k]
+
+-- | Sink first element of a list to the end of the list
+type family SinkFirst (xs :: [k]) = (ys :: List1 k) | ys -> xs where
+  SinkFirst '[y]       = 'L1Single y
+  -- SinkFirst (y ': x ': xs :: [Nat])
+  --     = ('L1Head x (GetList1Nat (SinkFirst (y ': xs))) :: List1 Nat)
+  SinkFirst (y ': x ': xs :: [k])
+      = ('L1Head x (GetList1    (SinkFirst (y ': xs))) :: List1 k)
+
+type family GetList1 (ts :: List1 k) = (rs :: [k]) | rs -> ts where
+  GetList1 ('L1Single x) = '[x]
+  GetList1 ('L1Head y (x ':xs)) = y ': x ': xs
+type family GetList1Nat (ts :: List1 Nat) = (rs :: [Nat]) | rs -> ts where
+  GetList1Nat ('L1Single x) = '[x]
+  GetList1Nat ('L1Head y (x ': xs)) = y ': x ': xs
+
+type family (++) (as :: [k]) (bs :: [k]) :: [k] where
+  '[] ++ bs = bs
+  (a ': as) ++ bs = a ': (as ++ bs)
+
+
+ff :: Proxy k -> Proxy (as +: k) -> Proxy (k ': bs) -> Proxy (as ++ bs)
+ff _ _ _ = Proxy
+
+yy :: Proxy '[3,7,2]
+yy = ff (Proxy @5) (Proxy @'[3,7,5]) (Proxy @'[5,2])
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 6d39e45..a921743 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -22,3 +22,4 @@ test('RaeJobTalk', normal, compile, [''])
 test('T11635', normal, compile, [''])
 test('T11719', normal, compile, [''])
 test('T12442', normal, compile, [''])
+test('T13538', normal, compile, [''])