Commit c6375411 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

Provide a better error message for unpromotable data constructor contexts

Trac #14845 brought to light a corner case where a data
constructor could not be promoted (even with `-XTypeInType`) due to
an unpromotable constraint in its context. However, the error message
was less than helpful, so this patch adds an additional check to
`tcTyVar` catch unpromotable data constructors like these //before//
they're promoted, and to give a sensible error message in such cases.

Test Plan: make test TEST="T13895 T14845"

Reviewers: simonpj, goldfire, bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #13895, #14845

Differential Revision: https://phabricator.haskell.org/D4728
parent 793902e6
......@@ -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
{-
************************************************************************
* *
......
......@@ -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"
......
......@@ -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"
{-
************************************************************************
......
......@@ -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:
......
{-# 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
......@@ -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, [''])
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)
{-# 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
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)
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’
{-# 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)
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’
{-# 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
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’
......@@ -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’
......@@ -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, [''])
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