[commit: ghc] wip/rae: Test #14038 in dependent/should_compile/T14038 (a0c6a10)

[git at git.haskell.org]

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

On branch  : wip/rae
Link       : http://ghc.haskell.org/trac/ghc/changeset/a0c6a10d74d7dbf36822aec75446664485cd5059/ghc

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

commit a0c6a10d74d7dbf36822aec75446664485cd5059
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Tue Aug 8 18:20:42 2017 -0400

    Test #14038 in dependent/should_compile/T14038


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

a0c6a10d74d7dbf36822aec75446664485cd5059
 .../should_compile/T14038.hs}                      | 27 +++++++++++-----------
 testsuite/tests/dependent/should_compile/all.T     |  1 +
 2 files changed, 15 insertions(+), 13 deletions(-)

diff --git a/testsuite/tests/indexed-types/should_fail/T13877.hs b/testsuite/tests/dependent/should_compile/T14038.hs
similarity index 72%
copy from testsuite/tests/indexed-types/should_fail/T13877.hs
copy to testsuite/tests/dependent/should_compile/T14038.hs
index ee5f16b..839220a 100644
--- a/testsuite/tests/indexed-types/should_fail/T13877.hs
+++ b/testsuite/tests/dependent/should_compile/T14038.hs
@@ -1,31 +1,32 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
-module T13877 where
+module T14038 where
 
-import Data.Kind
+import Data.Kind (Type)
 
 data family Sing (a :: k)
 data instance Sing (z :: [a]) where
   SNil  :: Sing '[]
   SCons :: Sing x -> Sing xs -> Sing (x:xs)
 
-data TyFun :: * -> * -> *
-type a ~> b = TyFun a b -> *
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
 infixr 0 ~>
 
 type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
 type a @@ b = Apply a b
 infixl 9 @@
 
-data FunArrow = (:->) | (:~>)
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
 
 class FunType (arr :: FunArrow) where
   type Fun (k1 :: Type) arr (k2 :: Type) :: Type
@@ -50,25 +51,25 @@ instance AppType (:~>) where
 infixr 0 -?>
 type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
 
-listElim :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+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
-listElim = listElimPoly @(:->) @a @p @l
+elimList = elimListPoly @(:->)
 
-listElimTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+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
-listElimTyFun = listElimPoly @(:->) @a @p @l
+elimListTyFun = elimListPoly @(:~>) @_ @p
 
-listElimPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+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
-listElimPoly SNil                      pNil _     = pNil
-listElimPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (listElimPoly @arr @a @p @xs xs pNil pCons)
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index b854f1d..a135892 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -25,3 +25,4 @@ test('T11966', normal, compile, [''])
 test('T12442', normal, compile, [''])
 test('T13538', normal, compile, [''])
 test('T12176', normal, compile, [''])
+test('T14038', expect_broken(14038), compile, [''])