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

1 files changed, 15 insertions, 9 deletions

diff --git a/testsuite/tests/polykinds/T11480b.hs b/testsuite/tests/polykinds/T11480b.hs
index 12802e8de3..2684c6de4e 100644
--- a/testsuite/tests/polykinds/T11480b.hs
+++ b/testsuite/tests/polykinds/T11480b.hs
@@ -21,25 +21,25 @@
 
 module T11480b where
 
-import GHC.Types (Constraint)
+import Data.Kind (Constraint, Type)
 import Data.Type.Equality as Equality
 import Data.Type.Coercion as Coercion
 import qualified Prelude
 import Prelude (Either(..))
 
-newtype Y (p :: i -> j -> *) (a :: j) (b :: i) = Y { getY :: p b a }
+newtype Y (p :: i -> j -> Type) (a :: j) (b :: i) = Y { getY :: p b a }
 
-type family Op (p :: i -> j -> *) :: j -> i -> * where
+type family Op (p :: i -> j -> Type) :: j -> i -> Type where
   Op (Y p) = p
   Op p = Y p
 
-class Vacuous (p :: i -> i -> *) (a :: i)
+class Vacuous (p :: i -> i -> Type) (a :: i)
 instance Vacuous p a
 
 data Dict (p :: Constraint) where
   Dict :: p => Dict p
 
-class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> *) where
+class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> Type) where
   type Ob p :: i -> Constraint
   type Ob p = Vacuous p
 
@@ -62,11 +62,16 @@ class Functor (Op p) (Nat p (->)) p => Category (p :: i -> i -> *) where
   default unop :: Op p ~ Y p => Op p b a -> p a b
   unop = getY
 
-class (Category p, Category q) => Functor (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) | f -> p q where
+class (Category p, Category q) =>
+      Functor (p :: i -> i -> Type)
+              (q :: j -> j -> Type)
+              (f :: i -> j) | f -> p q where
   fmap :: p a b -> q (f a) (f b)
 
-data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where
-  Nat :: (Functor p q f, Functor p q g) => { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g
+data Nat (p :: i -> i -> Type)
+         (q :: j -> j -> Type) (f :: i -> j) (g :: i -> j) where
+  Nat :: (Functor p q f, Functor p q g) =>
+         { runNat :: forall a. Ob p a => q (f a) (g a) } -> Nat p q f g
 
 instance (Category p, Category q) => Category (Nat p q) where
   type Ob (Nat p q) = Functor p q
@@ -80,7 +85,8 @@ instance (Category p, Category q) => Category (Nat p q) where
 ob :: forall p q f a. Functor p q f => Ob p a :- Ob q (f a)
 ob = Sub (case source (fmap (id :: p a a) :: q (f a) (f a)) of Dict -> Dict)
 
-instance (Category p, Category q) => Functor (Y (Nat p q)) (Nat (Nat p q) (->)) (Nat p q) where
+instance (Category p, Category q) =>
+         Functor (Y (Nat p q)) (Nat (Nat p q) (->)) (Nat p q) where
   fmap (Y f) = Nat (. f)
 
 instance (Category p, Category q) => Functor (Nat p q) (->) (Nat p q f) where