Fix #13391 by checking for kind-GADTs
authorRichard Eisenberg <rae@cs.brynmawr.edu>
Tue, 15 Aug 2017 21:22:50 +0000 (17:22 -0400)
committerRichard Eisenberg <rae@cs.brynmawr.edu>
Fri, 29 Sep 2017 01:02:38 +0000 (21:02 -0400)
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

compiler/basicTypes/DataCon.hs
compiler/typecheck/TcTyClsDecls.hs
libraries/base/Data/Type/Equality.hs
testsuite/tests/dependent/should_compile/Dep2.hs
testsuite/tests/dependent/should_compile/KindEqualities.hs
testsuite/tests/dependent/should_compile/KindEqualities.stderr
testsuite/tests/overloadedrecflds/should_run/overloadedrecfldsrun07.hs
testsuite/tests/polykinds/T13391.hs [new file with mode: 0644]
testsuite/tests/polykinds/T13391.stderr [new file with mode: 0644]
testsuite/tests/polykinds/T13391a.hs [new file with mode: 0644]
testsuite/tests/polykinds/all.T

index 9366c2b..9b8c527 100644 (file)
@@ -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]
index f2b60de..8767843 100644 (file)
@@ -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)
index 2b95a58..a3d2e0e 100644 (file)
@@ -4,9 +4,8 @@
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE StandaloneDeriving     #-}
 {-# LANGUAGE NoImplicitPrelude      #-}
-{-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE TypeInType             #-}
 {-# LANGUAGE TypeFamilies           #-}
 {-# LANGUAGE UndecidableInstances   #-}
 {-# LANGUAGE ExplicitNamespaces     #-}
index 34be3cf..df1cb51 100644 (file)
@@ -1,4 +1,4 @@
-{-# LANGUAGE PolyKinds, GADTs #-}
+{-# LANGUAGE TypeInType, GADTs #-}
 
 module Dep2 where
 
index 1f2e82c..4cba828 100644 (file)
@@ -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
index af429d1..ad9562e 100644 (file)
@@ -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 _ _) _)
index 25da616..c492ac8 100644 (file)
@@ -4,7 +4,7 @@
            , GADTs
            , MultiParamTypeClasses
            , OverloadedLabels
-           , PolyKinds
+           , TypeInType
            , ScopedTypeVariables
            , TypeApplications
            , TypeOperators
 
 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 (file)
index 0000000..6de3c3a
--- /dev/null
@@ -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 (file)
index 0000000..55fff35
--- /dev/null
@@ -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 (file)
index 0000000..4d5cc60
--- /dev/null
@@ -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
index 78c1697..0e5bcf1 100644 (file)
@@ -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, [''])