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

4 files changed, 12 insertions, 8 deletions

diff --git a/testsuite/tests/gadt/T7293.hs b/testsuite/tests/gadt/T7293.hs
index 26d9188f81..ed82f2a35b 100644
--- a/testsuite/tests/gadt/T7293.hs
+++ b/testsuite/tests/gadt/T7293.hs
@@ -3,9 +3,11 @@
 
 module T7294 where
 
+import Data.Kind (Type)
+
 data Nat = Zero | Succ Nat
 
-data Vec :: * -> Nat -> * where
+data Vec :: Type -> Nat -> Type where
   Nil :: Vec a Zero
   Cons :: a -> Vec a n -> Vec a (Succ n)
 
@@ -14,7 +16,7 @@ type instance m :< Zero = False
 type instance Zero :< Succ n = True
 type instance Succ n :< Succ m = n :< m
 
-data SNat :: Nat -> * where
+data SNat :: Nat -> Type where
   SZero :: SNat Zero
   SSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
 
diff --git a/testsuite/tests/gadt/T7293.stderr b/testsuite/tests/gadt/T7293.stderr
index 664f9a09df..87856d4009 100644
--- a/testsuite/tests/gadt/T7293.stderr
+++ b/testsuite/tests/gadt/T7293.stderr
@@ -1,9 +1,9 @@
 
-T7293.hs:24:1: error: [-Woverlapping-patterns (in -Wdefault), -Werror=overlapping-patterns]
+T7293.hs:26:1: error: [-Woverlapping-patterns (in -Wdefault), -Werror=overlapping-patterns]
     Pattern match is redundant
     In an equation for ‘nth’: nth Nil _ = ...
 
-T7293.hs:24:5: error: [-Winaccessible-code (in -Wdefault), -Werror=inaccessible-code]
+T7293.hs:26:5: error: [-Winaccessible-code (in -Wdefault), -Werror=inaccessible-code]
     • Couldn't match type ‘'True’ with ‘'False’
       Inaccessible code in
         a pattern with constructor: Nil :: forall a. Vec a 'Zero,
diff --git a/testsuite/tests/gadt/T7294.hs b/testsuite/tests/gadt/T7294.hs
index 1c39a2a574..d7615955a7 100644
--- a/testsuite/tests/gadt/T7294.hs
+++ b/testsuite/tests/gadt/T7294.hs
@@ -4,9 +4,11 @@
 
 module T7294 where
 
+import Data.Kind (Type)
+
 data Nat = Zero | Succ Nat
 
-data Vec :: * -> Nat -> * where
+data Vec :: Type -> Nat -> Type where
   Nil :: Vec a Zero
   Cons :: a -> Vec a n -> Vec a (Succ n)
 
@@ -15,7 +17,7 @@ type instance m :< Zero = False
 type instance Zero :< Succ n = True
 type instance Succ n :< Succ m = n :< m
 
-data SNat :: Nat -> * where
+data SNat :: Nat -> Type where
   SZero :: SNat Zero
   SSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
 
diff --git a/testsuite/tests/gadt/T7294.stderr b/testsuite/tests/gadt/T7294.stderr
index 63b3e0e3ef..d7b53ee9e2 100644
--- a/testsuite/tests/gadt/T7294.stderr
+++ b/testsuite/tests/gadt/T7294.stderr
@@ -1,9 +1,9 @@
 
-T7294.hs:25:1: warning: [-Woverlapping-patterns (in -Wdefault)]
+T7294.hs:27:1: warning: [-Woverlapping-patterns (in -Wdefault)]
     Pattern match is redundant
     In an equation for ‘nth’: nth Nil _ = ...
 
-T7294.hs:25:5: warning: [-Winaccessible-code (in -Wdefault)]
+T7294.hs:27:5: warning: [-Winaccessible-code (in -Wdefault)]
     • Couldn't match type ‘'True’ with ‘'False’
       Inaccessible code in
         a pattern with constructor: Nil :: forall a. Vec a 'Zero,