summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--compiler/basicTypes/DataCon.hs2
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs35
-rw-r--r--libraries/base/Data/Type/Equality.hs3
-rw-r--r--testsuite/tests/dependent/should_compile/Dep2.hs2
-rw-r--r--testsuite/tests/dependent/should_compile/KindEqualities.hs6
-rw-r--r--testsuite/tests/dependent/should_compile/KindEqualities.stderr2
-rw-r--r--testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs7
-rw-r--r--testsuite/tests/polykinds/T13391.hs7
-rw-r--r--testsuite/tests/polykinds/T13391.stderr7
-rw-r--r--testsuite/tests/polykinds/T13391a.hs7
-rw-r--r--testsuite/tests/polykinds/all.T2
11 files changed, 71 insertions, 9 deletions
diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index 9366c2ba11..9b8c527b97 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -312,6 +312,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 f2b60dece3..876784378c 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2513,6 +2513,32 @@ checkValidDataCon dflags existential_ok tc con
; checkTc (existential_ok || isVanillaDataCon con)
(badExistential con)
+ ; typeintype <- xoptM LangExt.TypeInType
+ ; let (_, _, eq_specs, _, _, _) = dataConFullSig con
+ -- dataConEqSpec retrieves both the real GADT equalities
+ -- plus any user-written GADT-like equalities. But we don't
+ -- want anything user-written. If we don't exclude user-written
+ -- ones, test case polykinds/T13391a fails.
+
+ invisible_gadt_eq_specs = filter is_invisible_eq_spec eq_specs
+ univ_tvs = dataConUnivTyVars con
+ tc_bndrs = tyConBinders tc
+
+ vis_map :: VarEnv ArgFlag
+ vis_map = zipVarEnv univ_tvs (map tyConBinderArgFlag tc_bndrs)
+
+ -- See Note [Wrong visibility for GADTs] for why we have to build the map
+ -- above instead of just looking at the datacon tyvar binder
+ is_invisible_eq_spec eq_spec
+ = isInvisibleArgFlag arg_flag
+ where
+ eq_tv = eqSpecTyVar eq_spec
+ arg_flag = expectJust "checkValidDataCon" $
+ lookupVarEnv vis_map eq_tv
+
+ ; 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
@@ -3226,6 +3252,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 2b95a588ae..a3d2e0ef15 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/dependent/should_compile/Dep2.hs
index 34be3cffc6..df1cb51e08 100644
--- a/testsuite/tests/dependent/should_compile/Dep2.hs
+++ b/testsuite/tests/dependent/should_compile/Dep2.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE PolyKinds, GADTs #-}
+{-# LANGUAGE TypeInType, GADTs #-}
module Dep2 where
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.hs b/testsuite/tests/dependent/should_compile/KindEqualities.hs
index 1f2e82c302..4cba8281ca 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.hs
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.hs
@@ -1,8 +1,10 @@
-{-# LANGUAGE PolyKinds, GADTs, ExplicitForAll #-}
+{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
module KindEqualities where
+import Data.Kind
+
data TyRep1 :: * -> * where
TyInt1 :: TyRep1 Int
TyBool1 :: TyRep1 Bool
@@ -13,7 +15,7 @@ zero1 TyBool1 = False
data Proxy (a :: k) = P
-data TyRep :: k -> * where
+data TyRep :: forall k. k -> * where
TyInt :: TyRep Int
TyBool :: TyRep Bool
TyMaybe :: TyRep Maybe
diff --git a/testsuite/tests/dependent/should_compile/KindEqualities.stderr b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
index af429d106b..ad9562eae8 100644
--- a/testsuite/tests/dependent/should_compile/KindEqualities.stderr
+++ b/testsuite/tests/dependent/should_compile/KindEqualities.stderr
@@ -1,5 +1,5 @@
-KindEqualities.hs:23:1: warning: [-Wincomplete-patterns (in -Wextra)]
+KindEqualities.hs:25:1: warning: [-Wincomplete-patterns (in -Wextra)]
Pattern match(es) are non-exhaustive
In an equation for ‘zero’:
Patterns not matched: (TyApp (TyApp _ _) _)
diff --git a/testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs b/testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs
index 25da616583..c492ac87a1 100644
--- a/testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs
+++ b/testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs
@@ -4,7 +4,7 @@
, GADTs
, MultiParamTypeClasses
, OverloadedLabels
- , PolyKinds
+ , TypeInType
, ScopedTypeVariables
, TypeApplications
, TypeOperators
@@ -13,12 +13,13 @@
import GHC.OverloadedLabels
import GHC.Records
-import GHC.TypeLits
+import GHC.TypeLits hiding (type (*))
+import Data.Kind
data Label (x :: Symbol) = Label
data Labelled x a = Label x := a
-data Rec :: [(k, *)] -> * where
+data Rec :: forall k. [(k, *)] -> * where
Nil :: Rec '[]
(:>) :: Labelled x a -> Rec xs -> Rec ('(x, a) ': xs)
infixr 5 :>
diff --git a/testsuite/tests/polykinds/T13391.hs b/testsuite/tests/polykinds/T13391.hs
new file mode 100644
index 0000000000..6de3c3aa40
--- /dev/null
+++ b/testsuite/tests/polykinds/T13391.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PolyKinds, GADTs #-}
+
+module T13391 where
+
+data G (a :: k) where
+ 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 0000000000..55fff35b3a
--- /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/T13391a.hs b/testsuite/tests/polykinds/T13391a.hs
new file mode 100644
index 0000000000..4d5cc607c0
--- /dev/null
+++ b/testsuite/tests/polykinds/T13391a.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE GADTs #-}
+module T13391a where
+
+-- this caused a panic during the work on T13391.
+
+data A a where
+ A3 :: b ~ Int => b -> A Int
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 78c16975da..0e5bcf1939 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -169,3 +169,5 @@ test('BadKindVar', normal, compile_fail, [''])
test('T13738', normal, compile_fail, [''])
test('T14209', normal, compile, [''])
test('T14265', normal, compile_fail, [''])
+test('T13391', normal, compile_fail, [''])
+test('T13391a', normal, compile, [''])
View Lorry Controller Status