Provide a better error message for unpromotable data constructor contexts
authorRyan Scott <ryan.gl.scott@gmail.com>
Sun, 17 Jun 2018 16:28:23 +0000 (12:28 -0400)
committerBen Gamari <ben@smart-cactus.org>
Sun, 17 Jun 2018 16:42:56 +0000 (12:42 -0400)
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

16 files changed:
compiler/typecheck/Inst.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcRnTypes.hs
docs/users_guide/glasgow_exts.rst
testsuite/tests/dependent/should_compile/T14845_compile.hs [new file with mode: 0644]
testsuite/tests/dependent/should_compile/all.T
testsuite/tests/dependent/should_fail/PromotedClass.stderr
testsuite/tests/dependent/should_fail/T13895.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T13895.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14845.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14845_fail1.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14845_fail1.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14845_fail2.hs [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T14845_fail2.stderr [new file with mode: 0644]
testsuite/tests/dependent/should_fail/T15215.stderr
testsuite/tests/dependent/should_fail/all.T

index bcd511b..ca7fac9 100644 (file)
@@ -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
-
 {-
 ************************************************************************
 *                                                                      *
index 0647ca4..03d3866 100644 (file)
@@ -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"
index d13941d..d91b5e9 100644 (file)
@@ -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"
 
 {-
 ************************************************************************
index 466584a..1b19b4c 100644 (file)
@@ -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 (file)
index 0000000..04f5018
--- /dev/null
@@ -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
index 2865351..64782c0 100644 (file)
@@ -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, [''])
index f068330..4da1a32 100644 (file)
@@ -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 (file)
index 0000000..5897cd8
--- /dev/null
@@ -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 (file)
index 0000000..0ae1710
--- /dev/null
@@ -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 (file)
index 0000000..3c11d15
--- /dev/null
@@ -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 (file)
index 0000000..46c1351
--- /dev/null
@@ -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 (file)
index 0000000..c1f1c86
--- /dev/null
@@ -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 (file)
index 0000000..4c5dac7
--- /dev/null
@@ -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 (file)
index 0000000..9fe733f
--- /dev/null
@@ -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’
index 80181b4..53aff76 100644 (file)
@@ -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’
index 8e5185f..2bfc39a 100644 (file)
@@ -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, [''])