[commit: ghc] master: Fix the test for #13938 (3ebf05f)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/3ebf05f5410a3e89d4dc6d451aea5020706fa5b0/ghc

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

commit 3ebf05f5410a3e89d4dc6d451aea5020706fa5b0
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Tue Mar 27 08:52:15 2018 -0400

    Fix the test for #13938
    
    Only half of the test files were checked in for T13938.
    This commit adds the missing half.


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

3ebf05f5410a3e89d4dc6d451aea5020706fa5b0
 testsuite/tests/dependent/should_compile/Makefile  |  5 ++
 testsuite/tests/dependent/should_compile/T13938.hs | 82 ++++------------------
 .../should_compile/{T13938.hs => T13938a.hs}       |  2 +-
 testsuite/tests/dependent/should_compile/all.T     |  3 +-
 4 files changed, 23 insertions(+), 69 deletions(-)

diff --git a/testsuite/tests/dependent/should_compile/Makefile b/testsuite/tests/dependent/should_compile/Makefile
index 9101fbd..0f85518 100644
--- a/testsuite/tests/dependent/should_compile/Makefile
+++ b/testsuite/tests/dependent/should_compile/Makefile
@@ -1,3 +1,8 @@
 TOP=../../..
 include $(TOP)/mk/boilerplate.mk
 include $(TOP)/mk/test.mk
+
+T13938:
+	$(RM) T13938a.hi T13938a.o T13938.hi T13938.o
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938a.hs
+	'$(TEST_HC)' $(TEST_HC_OPTS) -O -c T13938.hs
diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938.hs
index 3ba9e27..dd4f3d6 100644
--- a/testsuite/tests/dependent/should_compile/T13938.hs
+++ b/testsuite/tests/dependent/should_compile/T13938.hs
@@ -1,80 +1,28 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 module T13938 where
 
-import Data.Kind (Type)
+import T13938a
+import Data.Kind
+import Data.Type.Equality
+import GHC.TypeLits
 
-data family Sing (a :: k)
-data instance Sing (z :: [a]) where
-  SNil  :: Sing '[]
-  SCons :: Sing x -> Sing xs -> Sing (x:xs)
+type family Length (l :: [a]) :: Nat where {}
+type family Map (f :: a ~> b) (l :: [a]) :: [b] where {}
 
-data TyFun :: Type -> Type -> Type
-type a ~> b = TyFun a b -> Type
-infixr 0 ~>
+type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
+  = Length l :~: Length (Map f l)
+data WhyMapPreservesLengthSym1 (f :: x ~> y) :: [x] ~> Type
+type instance Apply (WhyMapPreservesLengthSym1 f) l = WhyMapPreservesLength f l
 
-type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
-type a @@ b = Apply a b
-infixl 9 @@
-
-data FunArrow = (:->) -- ^ '(->)'
-              | (:~>) -- ^ '(~>)'
-
-class FunType (arr :: FunArrow) where
-  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
-
-class FunType arr => AppType (arr :: FunArrow) where
-  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
-
-type FunApp arr = (FunType arr, AppType arr)
-
-instance FunType (:->) where
-  type Fun k1 (:->) k2 = k1 -> k2
-
-$(return []) -- This is only necessary for GHC 8.0 -- GHC 8.2 is smarter
-
-instance AppType (:->) where
-  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
-
-instance FunType (:~>) where
-  type Fun k1 (:~>) k2 = k1 ~> k2
-
-$(return [])
-
-instance AppType (:~>) where
-  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
-
-infixr 0 -?>
-type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
-
-elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
-            Sing l
-         -> p '[]
-         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
-         -> p l
-elimList = elimListPoly @(:->)
-
-elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
-                 Sing l
-              -> p @@ '[]
-              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
-              -> p @@ l
-elimListTyFun = elimListPoly @(:~>) @_ @p
-
-elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
-                FunApp arr
-             => Sing l
-             -> App [a] arr Type p '[]
-             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
-             -> App [a] arr Type p l
-elimListPoly SNil                      pNil _     = pNil
-elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
+mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).
+                      Length l :~: Length (Map f l)
+mapPreservesLength
+  = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l undefined undefined undefined
diff --git a/testsuite/tests/dependent/should_compile/T13938.hs b/testsuite/tests/dependent/should_compile/T13938a.hs
similarity index 99%
copy from testsuite/tests/dependent/should_compile/T13938.hs
copy to testsuite/tests/dependent/should_compile/T13938a.hs
index 3ba9e27..3a09292 100644
--- a/testsuite/tests/dependent/should_compile/T13938.hs
+++ b/testsuite/tests/dependent/should_compile/T13938a.hs
@@ -9,7 +9,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
-module T13938 where
+module T13938a where
 
 import Data.Kind (Type)
 
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index ab7ab3c..da25b22 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -28,6 +28,7 @@ test('T12176', normal, compile, [''])
 test('T14038', normal, compile, [''])
 test('T12742', normal, compile, [''])
 test('T13910', normal, compile, [''])
-test('T13938', normal, compile, [''])
+test('T13938', [extra_files(['T13938a.hs'])], run_command,
+     ['$MAKE -s --no-print-directory T13938'])
 test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])