Commit 7aa000b6 authored by Richard Eisenberg's avatar Richard Eisenberg

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
parent 5935acdb
......@@ -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]
......
......@@ -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)
......
......@@ -4,9 +4,8 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExplicitNamespaces #-}
......
{-# LANGUAGE PolyKinds, GADTs #-}
{-# LANGUAGE TypeInType, GADTs #-}
module Dep2 where
......
{-# 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
......
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 _ _) _)
......@@ -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 :>
......
{-# LANGUAGE PolyKinds, GADTs #-}
module T13391 where
data G (a :: k) where
GInt :: G Int
GMaybe :: G Maybe
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’
{-# LANGUAGE GADTs #-}
module T13391a where
-- this caused a panic during the work on T13391.
data A a where
A3 :: b ~ Int => b -> A Int
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment