[commit: ghc] wip/rae: Fix #13391 by checking for kind-GADTs (56b0c7b)

[git at git.haskell.org]

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

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

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

commit 56b0c7b1b5f929371c13f4f302bad1e2f8f652ba
Author: Richard Eisenberg <rae at cs.brynmawr.edu>
Date:   Tue Aug 15 17:22:50 2017 -0400

    Fix #13391 by checking for kind-GADTs
    
    The check is a bit gnarly, but I couldn't think of a better way.
    See the new code in TcTyClsDecls.
    
    test case: polykinds/T13391


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

56b0c7b1b5f929371c13f4f302bad1e2f8f652ba
 compiler/basicTypes/DataCon.hs                     |  2 ++
 compiler/typecheck/TcTyClsDecls.hs                 | 29 ++++++++++++++++++++++
 libraries/base/Data/Type/Equality.hs               |  3 +--
 .../should_compile/Dep2.hs => polykinds/T13391.hs} |  6 ++---
 testsuite/tests/polykinds/T13391.stderr            |  7 ++++++
 testsuite/tests/polykinds/all.T                    |  1 +
 6 files changed, 43 insertions(+), 5 deletions(-)

diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index fa8e0a8..06bb504 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -310,6 +310,8 @@ data DataCon
         -- Universally-quantified type vars [a,b,c]
         -- INVARIANT: length matches arity of the dcRepTyCon
         -- INVARIANT: result type of data con worker is exactly (T a b c)
+        -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
+        --            the tyConTyVars of the parent TyCon
         dcUnivTyVars    :: [TyVarBinder],
 
         -- Existentially-quantified type vars [x,y]
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 0974fe5..1409705 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2492,6 +2492,26 @@ checkValidDataCon dflags existential_ok tc con
         ; checkTc (existential_ok || isVanillaDataCon con)
                   (badExistential con)
 
+        ; typeintype <- xoptM LangExt.TypeInType
+        ; let invisible_gadt_eq_specs = filter is_invisible_eq_spec (dataConEqSpec con)
+              univ_tvs = dataConUnivTyVars con
+              tc_bndrs = tyConBinders tc
+
+                -- find the index of the univ tv mentioned in the eq_spec
+                -- then, look that up in the TyConBinders to see if it's visible
+                -- Maybe there's a better way, but I don't see it.
+                -- See Note [Wrong visibility for GADTs], though.
+              is_invisible_eq_spec eq_spec
+                = let eq_tv    = eqSpecTyVar eq_spec
+                      tv_index = expectJust "checkValidDataCon" $
+                                 elemIndex eq_tv univ_tvs
+                      tc_bndr  = tc_bndrs `getNth` tv_index
+                  in
+                  isInvisibleTyConBinder tc_bndr
+
+        ; checkTc (typeintype || null invisible_gadt_eq_specs)
+                  (badGADT con invisible_gadt_eq_specs)
+
           -- Check that UNPACK pragmas and bangs work out
           -- E.g.  reject   data T = MkT {-# UNPACK #-} Int     -- No "!"
           --                data T = MkT {-# UNPACK #-} !a      -- Can't unpack
@@ -3197,6 +3217,15 @@ badExistential con
        2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
                , parens $ text "Use ExistentialQuantification or GADTs to allow this" ])
 
+badGADT :: DataCon -> [EqSpec] -> SDoc
+badGADT con eq_specs
+  = hang (text "Data constructor" <+> quotes (ppr con) <+>
+               text "constrains the choice of kind parameter" <> plural eq_specs <> colon)
+       2 (vcat (map ppr_eq_spec eq_specs)) $$
+    text "Use TypeInType to allow this"
+  where
+    ppr_eq_spec eq_spec = ppr (eqSpecTyVar eq_spec) <+> char '~' <+> ppr (eqSpecType eq_spec)
+
 badStupidTheta :: Name -> SDoc
 badStupidTheta tc_name
   = text "A data type declared in GADT style cannot have a context:" <+> quotes (ppr tc_name)
diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs
index 09999b0..e34eb24 100644
--- a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ -4,9 +4,8 @@
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE StandaloneDeriving     #-}
 {-# LANGUAGE NoImplicitPrelude      #-}
-{-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeInType             #-}
 {-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE UndecidableInstances   #-}
 {-# LANGUAGE ExplicitNamespaces     #-}
diff --git a/testsuite/tests/dependent/should_compile/Dep2.hs b/testsuite/tests/polykinds/T13391.hs
similarity index 50%
copy from testsuite/tests/dependent/should_compile/Dep2.hs
copy to testsuite/tests/polykinds/T13391.hs
index 34be3cf..6de3c3a 100644
--- a/testsuite/tests/dependent/should_compile/Dep2.hs
+++ b/testsuite/tests/polykinds/T13391.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE PolyKinds, GADTs #-}
 
-module Dep2 where
+module T13391 where
 
 data G (a :: k) where
-  G1 :: G Int
-  G2 :: G Maybe
+  GInt   :: G Int
+  GMaybe :: G Maybe
diff --git a/testsuite/tests/polykinds/T13391.stderr b/testsuite/tests/polykinds/T13391.stderr
new file mode 100644
index 0000000..55fff35
--- /dev/null
+++ b/testsuite/tests/polykinds/T13391.stderr
@@ -0,0 +1,7 @@
+
+T13391.hs:6:3: error:
+    • Data constructor ‘GInt’ constrains the choice of kind parameter:
+        k ~ *
+      Use TypeInType to allow this
+    • In the definition of data constructor ‘GInt’
+      In the data type declaration for ‘G’
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index ddee253..376b5a9 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -164,3 +164,4 @@ test('T13555', normal, compile_fail, [''])
 test('T13659', normal, compile_fail, [''])
 test('T13625', normal, compile_fail, [''])
 test('T14110', normal, compile_fail, [''])
+test('T13391', normal, compile_fail, [''])