diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index bcd511b982fa93dc97feaacba6acd69b614af313..ca7fac97bc9e5184892ae9b0e54b94baa754ab73 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -45,7 +45,7 @@ import TcRnMonad
import TcEnv
import TcEvidence
import InstEnv
-import TysWiredIn ( heqDataCon, coercibleDataCon )
+import TysWiredIn ( heqDataCon )
import CoreSyn ( isOrphan )
import FunDeps
import TcMType
@@ -454,7 +454,7 @@ tcInstBinder _ subst (Anon ty)
| isPredTy substed_ty
= do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
- ; addErrTcM (env, text "Illegal constraint in a type:" <+> ppr tidy_ty)
+ ; addErrTcM (env, text "Illegal constraint in a kind:" <+> ppr tidy_ty)
-- just invent a new variable so that we can continue
; u <- newUnique
@@ -481,8 +481,6 @@ tcInstBinder _ subst (Anon ty)
| Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
= if | tc `hasKey` eqTyConKey
-> Just (mkEqBoxTy, Nominal, k1, k2)
- | tc `hasKey` coercibleTyConKey
- -> Just (mkCoercibleBoxTy, Representational, k1, k2)
| otherwise
-> Nothing
| otherwise
@@ -507,15 +505,6 @@ mkEqBoxTy co ty1 ty2
; return $ mkTyConApp (promoteDataCon datacon) [k, ty1, ty2, hetero] }
where k = typeKind ty1
--- | This takes @a ~R# b@ and returns @Coercible a b@.
-mkCoercibleBoxTy :: TcCoercion -> Type -> Type -> TcM Type
--- monadic just for convenience with mkEqBoxTy
-mkCoercibleBoxTy co ty1 ty2
- = do { return $
- mkTyConApp (promoteDataCon coercibleDataCon)
- [k, ty1, ty2, mkCoercionTy co] }
- where k = typeKind ty1
-
{-
************************************************************************
* *
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 0647ca4884117f3d98729ac146957e03d4bbfa5b..03d38664aa2163eb55c4274af1fa9ed7ee7b6213 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -100,7 +100,7 @@ import PrelNames hiding ( wildCardName )
import qualified GHC.LanguageExtensions as LangExt
import Maybes
-import Data.List ( mapAccumR )
+import Data.List ( find, mapAccumR )
import Control.Monad
{-
@@ -1150,6 +1150,11 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
; when (isFamInstTyCon (dataConTyCon dc)) $
-- see Trac #15245
promotionErr name FamDataConPE
+ ; let (_, _, _, theta, _, _) = dataConFullSig dc
+ ; case dc_theta_illegal_constraint theta of
+ Just pred -> promotionErr name $
+ ConstrainedDataConPE pred
+ Nothing -> pure ()
; let tc = promoteDataCon dc
; return (mkNakedTyConApp tc [], tyConKind tc) }
@@ -1201,6 +1206,18 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
_ -> do { traceTc "lk1 (loopy)" (ppr name)
; return tc_tc } }
+ -- We cannot promote a data constructor with a context that contains
+ -- constraints other than equalities, so error if we find one.
+ -- See Note [Don't promote data constructors with non-equality contexts]
+ dc_theta_illegal_constraint :: ThetaType -> Maybe PredType
+ dc_theta_illegal_constraint = find go
+ where
+ go :: PredType -> Bool
+ go pred | Just tc <- tyConAppTyCon_maybe pred
+ = not $ tc `hasKey` eqTyConKey
+ || tc `hasKey` heqTyConKey
+ | otherwise = True
+
{-
Note [Type-checking inside the knot]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1365,6 +1382,24 @@ in the e2 example, we'll desugar the type, zonking the kind unification
variables as we go. When we encounter the unconstrained kappa, we
want to default it to '*', not to (Any *).
+Note [Don't promote data constructors with non-equality contexts]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+With -XTypeInType, one can promote almost any data constructor. There is a
+notable exception to this rule, however: data constructors that contain
+non-equality constraints, such as:
+
+ data Foo a where
+ MkFoo :: Show a => Foo a
+
+MkFoo cannot be promoted since GHC cannot produce evidence for (Show a) at the
+kind level. Therefore, we check the context of each data constructor before
+promotion, and give a sensible error message if the context contains an illegal
+constraint.
+
+Note that equality constraints (i.e, (~) and (~~)) /are/
+permitted inside data constructor contexts. All other constraints are
+off-limits, however (and likely will remain off-limits until dependent types
+become a reality in GHC).
Help functions for type applications
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2685,6 +2720,9 @@ promotionErr name err
2 (parens reason))
where
reason = case err of
+ ConstrainedDataConPE pred
+ -> text "it has an unpromotable context"
+ <+> quotes (ppr pred)
FamDataConPE -> text "it comes from a data family instance"
NoDataKindsTC -> text "perhaps you intended to use DataKinds"
NoDataKindsDC -> text "perhaps you intended to use DataKinds"
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index d13941d9ec83a29228dd85e3ec518c09b91ac6dc..d91b5e9e78edcae8b1ddecf160ad5991dedaa462 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1096,6 +1096,10 @@ data PromotionErr
| FamDataConPE -- Data constructor for a data family
-- See Note [AFamDataCon: not promoting data family constructors]
-- in TcEnv.
+ | ConstrainedDataConPE PredType
+ -- Data constructor with a non-equality context
+ -- See Note [Don't promote data constructors with
+ -- non-equality contexts] in TcHsType
| PatSynPE -- Pattern synonyms
-- See Note [Don't promote pattern synonyms] in TcEnv
@@ -1250,14 +1254,16 @@ instance Outputable IdBindingInfo where
text "TopLevelLet" <+> ppr fvs <+> ppr closed_type
instance Outputable PromotionErr where
- ppr ClassPE = text "ClassPE"
- ppr TyConPE = text "TyConPE"
- ppr PatSynPE = text "PatSynPE"
- ppr PatSynExPE = text "PatSynExPE"
- ppr FamDataConPE = text "FamDataConPE"
- ppr RecDataConPE = text "RecDataConPE"
- ppr NoDataKindsTC = text "NoDataKindsTC"
- ppr NoDataKindsDC = text "NoDataKindsDC"
+ ppr ClassPE = text "ClassPE"
+ ppr TyConPE = text "TyConPE"
+ ppr PatSynPE = text "PatSynPE"
+ ppr PatSynExPE = text "PatSynExPE"
+ ppr FamDataConPE = text "FamDataConPE"
+ ppr (ConstrainedDataConPE pred) = text "ConstrainedDataConPE"
+ <+> parens (ppr pred)
+ ppr RecDataConPE = text "RecDataConPE"
+ ppr NoDataKindsTC = text "NoDataKindsTC"
+ ppr NoDataKindsDC = text "NoDataKindsDC"
pprTcTyThingCategory :: TcTyThing -> SDoc
pprTcTyThingCategory (AGlobal thing) = pprTyThingCategory thing
@@ -1267,14 +1273,15 @@ pprTcTyThingCategory (ATcTyCon {}) = text "Local tycon"
pprTcTyThingCategory (APromotionErr pe) = pprPECategory pe
pprPECategory :: PromotionErr -> SDoc
-pprPECategory ClassPE = text "Class"
-pprPECategory TyConPE = text "Type constructor"
-pprPECategory PatSynPE = text "Pattern synonym"
-pprPECategory PatSynExPE = text "Pattern synonym existential"
-pprPECategory FamDataConPE = text "Data constructor"
-pprPECategory RecDataConPE = text "Data constructor"
-pprPECategory NoDataKindsTC = text "Type constructor"
-pprPECategory NoDataKindsDC = text "Data constructor"
+pprPECategory ClassPE = text "Class"
+pprPECategory TyConPE = text "Type constructor"
+pprPECategory PatSynPE = text "Pattern synonym"
+pprPECategory PatSynExPE = text "Pattern synonym existential"
+pprPECategory FamDataConPE = text "Data constructor"
+pprPECategory ConstrainedDataConPE{} = text "Data constructor"
+pprPECategory RecDataConPE = text "Data constructor"
+pprPECategory NoDataKindsTC = text "Type constructor"
+pprPECategory NoDataKindsDC = text "Data constructor"
{-
************************************************************************
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index 466584ad3a26f963d70f212b4f3bb93fa9d3abb8..1b19b4cda8e63248d1edbc8eda41ec31df2d5a2e 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -8546,12 +8546,24 @@ constructors are prefixed by a tick ``'``): ::
'L :: k1 -> Sum k1 k2
'R :: k2 -> Sum k1 k2
-.. note::
- Data family instances cannot be promoted at the moment: GHC’s type theory
- just isn’t up to the task of promoting data families, which requires full
- dependent types.
+Virtually all data constructors, even those with rich kinds, can be promoted.
+There are only a couple of exceptions to this rule:
+
+- Data family instance constructors cannot be promoted at the moment. GHC's
+ type theory just isn’t up to the task of promoting data families, which
+ requires full dependent types.
+
+- Data constructors with contexts that contain non-equality constraints cannot
+ be promoted. For example: ::
+
+ data Foo :: Type -> Type where
+ MkFoo1 :: a ~ Int => Foo a -- promotable
+ MkFoo2 :: a ~~ Int => Foo a -- promotable
+ MkFoo3 :: Show a => Foo a -- not promotable
- See also :ghc-ticket:`15245`.
+ ``MkFoo1`` and ``MkFoo2`` can be promoted, since their contexts
+ only involve equality-oriented constraints. However, ``MkFoo3``'s context
+ contains a non-equality constraint ``Show a``, and thus cannot be promoted.
.. _promotion-syntax:
diff --git a/testsuite/tests/dependent/should_compile/T14845_compile.hs b/testsuite/tests/dependent/should_compile/T14845_compile.hs
new file mode 100644
index 0000000000000000000000000000000000000000..04f50189b8b1be114be64c2dcf1331bb58146726
--- /dev/null
+++ b/testsuite/tests/dependent/should_compile/T14845_compile.hs
@@ -0,0 +1,16 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+{-# Language FlexibleContexts #-}
+{-# Language RankNTypes #-}
+{-# Language TypeOperators #-}
+module T14845 where
+
+import Data.Kind
+import Data.Type.Equality
+
+data A :: Type -> Type where
+ MkA1 :: a ~ Int => A a
+ MkA2 :: a ~~ Int => A a
+
+data SA :: forall a. A a -> Type where
+ SMkA1 :: SA MkA1
+ SMkA2 :: SA MkA2
diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 2865351ff5fbdd74c54eada8b37def3e1eb70524..64782c027641cc71cd151dbc19851f7bb5f33b60 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -47,6 +47,7 @@ test('T14556', normal, compile, [''])
test('T14720', normal, compile, [''])
test('T14066a', normal, compile, [''])
test('T14749', normal, compile, [''])
+test('T14845_compile', normal, compile, [''])
test('T14991', normal, compile, [''])
test('T15264', normal, compile, [''])
-test('DkNameRes', normal, compile, [''])
\ No newline at end of file
+test('DkNameRes', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/PromotedClass.stderr b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
index f0683309bc62001676492c708437c60d1b2d97da..4da1a32fca5d7a8c084191ef35e3dfcb5cf675ee 100644
--- a/testsuite/tests/dependent/should_fail/PromotedClass.stderr
+++ b/testsuite/tests/dependent/should_fail/PromotedClass.stderr
@@ -1,5 +1,6 @@
PromotedClass.hs:10:15: error:
- • Illegal constraint in a type: Show a0
+ • Data constructor ‘MkX’ cannot be used here
+ (it has an unpromotable context ‘Show a’)
• In the first argument of ‘Proxy’, namely ‘( 'MkX 'True)’
In the type signature: foo :: Proxy ( 'MkX 'True)
diff --git a/testsuite/tests/dependent/should_fail/T13895.hs b/testsuite/tests/dependent/should_fail/T13895.hs
new file mode 100644
index 0000000000000000000000000000000000000000..5897cd814963f6317a9f4ba2b68f6aee675e6b9f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module T13895 where
+
+import Data.Data (Data, Typeable)
+import Data.Kind
+
+dataCast1 :: forall (a :: Type).
+ Data a
+ => forall (c :: Type -> Type)
+ (t :: forall (k :: Type). Typeable k => k -> Type).
+ Typeable t
+ => (forall d. Data d => c (t d))
+ -> Maybe (c a)
+dataCast1 _ = undefined
diff --git a/testsuite/tests/dependent/should_fail/T13895.stderr b/testsuite/tests/dependent/should_fail/T13895.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..0ae1710bf08b5acee8b1a5b3d673de6a8ecae187
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T13895.stderr
@@ -0,0 +1,20 @@
+
+T13895.hs:12:23: error:
+ • Illegal constraint in a kind: Typeable k0
+ • In the first argument of ‘Typeable’, namely ‘t’
+ In the type signature:
+ dataCast1 :: forall (a :: Type).
+ Data a =>
+ forall (c :: Type -> Type)
+ (t :: forall (k :: Type). Typeable k => k -> Type).
+ Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
+
+T13895.hs:13:38: error:
+ • Illegal constraint in a kind: Typeable k0
+ • In the first argument of ‘c’, namely ‘(t d)’
+ In the type signature:
+ dataCast1 :: forall (a :: Type).
+ Data a =>
+ forall (c :: Type -> Type)
+ (t :: forall (k :: Type). Typeable k => k -> Type).
+ Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)
diff --git a/testsuite/tests/dependent/should_fail/T14845.stderr b/testsuite/tests/dependent/should_fail/T14845.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..3c11d151958eccb71cd2a0601b2fc06dbbd4ef39
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845.stderr
@@ -0,0 +1,7 @@
+
+T14845.hs:19:16: error:
+ • Data constructor ‘MkA3’ cannot be used here
+ (it has an unpromotable context ‘Coercible a Int’)
+ • In the first argument of ‘SA’, namely ‘(MkA3 :: A Int)’
+ In the type ‘SA (MkA3 :: A Int)’
+ In the definition of data constructor ‘SMkA3’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.hs b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
new file mode 100644
index 0000000000000000000000000000000000000000..46c13510279de977a2298eba47c28e7727cd2874
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.hs
@@ -0,0 +1,10 @@
+{-# Language PolyKinds, DataKinds, KindSignatures, GADTs, TypeInType, ConstraintKinds #-}
+module T14845_fail1 where
+
+import Data.Kind
+
+data Struct :: (k -> Constraint) -> (k -> Type) where
+ S :: cls a => Struct cls a
+
+data Foo a where
+ F :: Foo (S::Struct Eq a)
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail1.stderr b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..c1f1c8605d374baa953c29b3d272870c6bdefe3f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail1.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail1.hs:10:13: error:
+ • Data constructor ‘S’ cannot be used here
+ (it has an unpromotable context ‘cls a’)
+ • In the first argument of ‘Foo’, namely ‘(S :: Struct Eq a)’
+ In the type ‘Foo (S :: Struct Eq a)’
+ In the definition of data constructor ‘F’
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.hs b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
new file mode 100644
index 0000000000000000000000000000000000000000..4c5dac730f76e76334e4706477f1da4a4f9c6168
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T14845_fail2 where
+
+import Data.Coerce
+import Data.Kind
+
+data A :: Type -> Type where
+ MkA :: Coercible a Int => A a
+
+data SA :: forall a. A a -> Type where
+ SMkA :: SA MkA
diff --git a/testsuite/tests/dependent/should_fail/T14845_fail2.stderr b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..9fe733f374f19e6effb701188b18eaf4316f36cd
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_fail2.stderr
@@ -0,0 +1,7 @@
+
+T14845_fail2.hs:14:14: error:
+ • Data constructor ‘MkA’ cannot be used here
+ (it has an unpromotable context ‘Coercible a Int’)
+ • In the first argument of ‘SA’, namely ‘MkA’
+ In the type ‘SA MkA’
+ In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/T15215.stderr b/testsuite/tests/dependent/should_fail/T15215.stderr
index 80181b44bdd2fd2357565843267c704f8e5d50f0..53aff765a326df8b6bbc2319ea8157758c95b112 100644
--- a/testsuite/tests/dependent/should_fail/T15215.stderr
+++ b/testsuite/tests/dependent/should_fail/T15215.stderr
@@ -6,7 +6,7 @@ T15215.hs:9:3: error:
In the data type declaration for ‘A’
T15215.hs:12:14: error:
- • Illegal constraint in a type: Show (Maybe a0)
+ • Illegal constraint in a kind: Show (Maybe a0)
• In the first argument of ‘SA’, namely ‘MkA’
In the type ‘SA MkA’
In the definition of data constructor ‘SMkA’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 8e5185f1aebcfa8cd2d4e8f1982b78107aa8397e..2bfc39a6b8a1652440686f6240ae35682149def8 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -19,6 +19,7 @@ test('T13601', normal, compile_fail, [''])
test('T13780a', normal, compile_fail, [''])
test('T13780c', [extra_files(['T13780b.hs'])],
multimod_compile_fail, ['T13780c', ''])
+test('T13895', normal, compile_fail, [''])
test('T14066', normal, compile_fail, [''])
test('T14066c', normal, compile_fail, [''])
test('T14066d', normal, compile_fail, [''])
@@ -26,6 +27,8 @@ test('T14066e', normal, compile_fail, [''])
test('T14066f', normal, compile_fail, [''])
test('T14066g', normal, compile_fail, [''])
test('T14066h', normal, compile_fail, [''])
+test('T14845_fail1', normal, compile_fail, [''])
+test('T14845_fail2', normal, compile_fail, [''])
test('InferDependency', normal, compile_fail, [''])
test('T15245', normal, compile_fail, [''])
test('T15215', normal, compile_fail, [''])