From 3ebf05f5410a3e89d4dc6d451aea5020706fa5b0 Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Tue, 27 Mar 2018 08:52:15 -0400
Subject: Fix the test for #13938

Only half of the test files were checked in for T13938.
This commit adds the missing half.
---
 .../tests/dependent/should_compile/T13938a.hs      | 80 ++++++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 testsuite/tests/dependent/should_compile/T13938a.hs

(limited to 'testsuite/tests/dependent/should_compile/T13938a.hs')

diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs
new file mode 100644
index 0000000000..3a09292922
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T13938a.hs
@@ -0,0 +1,80 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module T13938a where
+
+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 -> 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 = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+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)
-- 
cgit v1.2.1


From d650729f9a0f3b6aa5e6ef2d5fba337f6f70fa60 Mon Sep 17 00:00:00 2001
From: Vladislav Zavialov <vlad.z.4096@gmail.com>
Date: Thu, 14 Jun 2018 15:02:36 -0400
Subject: Embrace -XTypeInType, add -XStarIsType

Summary:
Implement the "Embrace Type :: Type" GHC proposal,
.../ghc-proposals/blob/master/proposals/0020-no-type-in-type.rst

GHC 8.0 included a major change to GHC's type system: the Type :: Type
axiom. Though casual users were protected from this by hiding its
features behind the -XTypeInType extension, all programs written in GHC
8+ have the axiom behind the scenes. In order to preserve backward
compatibility, various legacy features were left unchanged. For example,
with -XDataKinds but not -XTypeInType, GADTs could not be used in types.
Now these restrictions are lifted and -XTypeInType becomes a redundant
flag that will be eventually deprecated.

* Incorporate the features currently in -XTypeInType into the
  -XPolyKinds and -XDataKinds extensions.
* Introduce a new extension -XStarIsType to control how to parse * in
  code and whether to print it in error messages.

Test Plan: Validate

Reviewers: goldfire, hvr, bgamari, alanz, simonpj

Reviewed By: goldfire, simonpj

Subscribers: rwbarton, thomie, mpickering, carter

GHC Trac Issues: #15195

Differential Revision: https://phabricator.haskell.org/D4748
---
 testsuite/tests/dependent/should_compile/T13938a.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'testsuite/tests/dependent/should_compile/T13938a.hs')

diff --git a/testsuite/tests/dependent/should_compile/T13938a.hs b/testsuite/tests/dependent/should_compile/T13938a.hs
index 3a09292922..5197747e87 100644
--- a/testsuite/tests/dependent/should_compile/T13938a.hs
+++ b/testsuite/tests/dependent/should_compile/T13938a.hs
@@ -7,7 +7,8 @@
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeOperators #-}
 module T13938a where
 
-- 
cgit v1.2.1