[Git][ghc/ghc][wip/T18891] Wibbles
Simon Peyton Jones
gitlab at gitlab.haskell.org
Tue Nov 24 15:26:40 UTC 2020
Simon Peyton Jones pushed to branch wip/T18891 at Glasgow Haskell Compiler / GHC
Commits:
66356469 by Simon Peyton Jones at 2020-11-24T15:26:02+00:00
Wibbles
- - - - -
9 changed files:
- compiler/GHC/Tc/TyCl/Instance.hs
- testsuite/tests/dependent/should_fail/T13780a.hs
- testsuite/tests/th/T9692.hs
- testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
- testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
- + testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
- + testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -865,7 +865,7 @@ tcDataFamInstHeader
-- e.g. data instance D [a] :: * -> * where ...
-- Here the "header" is the bit before the "where"
tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
- hs_ctxt hs_pats m_ksig hs_cons new_or_data
+ hs_ctxt hs_pats m_ksig _hs_cons new_or_data
= do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats)
; (tclvl, wanted, (scoped_tvs, (stupid_theta, lhs_ty, master_res_kind, instance_res_kind)))
<- pushLevelAndSolveEqualitiesX "tcDataFamInstHeader" $
@@ -884,8 +884,9 @@ tcDataFamInstHeader mb_clsinfo fam_tc outer_bndrs fixity
-- Add constraints from the result signature
; res_kind <- tc_kind_sig m_ksig
- -- Add constraints from the data constructors
- ; kcConDecls new_or_data res_kind hs_cons
+ -- Do not add constraints from the data constructors
+ -- See Note [Kind inference for data family instances]
+-- ; kcConDecls new_or_data res_kind hs_cons
-- Check that the result kind of the TyCon applied to its args
-- is compatible with the explicit signature (or Type, if there
@@ -1049,6 +1050,73 @@ however, so this Note aims to describe these subtleties:
themselves. Heavy sigh. But not truly hard; that's what tcbVisibilities
does.
+Note [Kind inference for data family instances]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this GADT-style data type declaration, where I have used
+fresh variables in the data constructor's type, to stress that c,d are
+quite distinct from a,b.
+ data T a b where
+ MkT :: forall c d. c d -> T c d
+
+Following Note [Inferring kinds for type declarations] in GHC.Tc.TyCl,
+to infer T's kind, we initially give T :: kappa, a monomorpic kind,
+gather constraints from the header and data constructors, and conclude
+ T :: (kappa1 -> type) -> kappa1 -> Type
+Then we generalise, giving
+ T :: forall k. (k->Type) -> k -> Type
+
+Now what about a data /instance/ decl
+ data family T :: forall k. (k->Type) -> k -> Type
+
+ data instance T p Int where ...
+
+No doubt here! The poly-kinded T is instantiate with k=Type, so the
+header really looks like
+ data instance T @Type (p :: Type->Type) Int where ...
+
+But what about this?
+ data instance T p q where
+ MkT :: forall r. r Int -> T r Int
+
+Remember: we already /fully know/ T's kind -- that came from the
+family declaration, and is not influenced by the data instances.
+
+So what kind do 'p' and 'q' have? No clues from the header, but from
+the data constructor we can clearly see that (r :: Type->Type). Does
+that mean that the the /entire data instance/ is instantiated at Type,
+like this?
+ data instance T @Type (p :: Type->Type) (q :: Type) where
+ ...
+
+Not at all! This is a /GADT/-style decl, so the kind argument might
+be instantiated by the GADT, thus:
+ data instance T @k (p :: k->Type) (q :: k) where
+ MkT :: forall (r :: Type -> Type).
+ r Int -> T @Type r Int
+
+SHORT SUMMARY: in a data instance decl, it's not clear whether kind
+constraints arising from the data constructors should be considered
+local to the (GADT) data /constructor/ or should apply to the entire
+data instance.
+
+DESIGN CHOICE: in data/newtype family instance declarations, we ignore
+the /data constructor/ declarations altogether, looking only at the
+data instance /header/.
+
+Observations:
+* This choice is simple to describe, as well as simple to implment.
+ For a data/newtype instance decl, the instance kinds are influenced
+ /only/ by the header.
+
+* We could treat Haskell-98 style data-instance decls differently, by
+ taking the data constructors into account, since there are no GADT
+ issues.
+
+* Ditto newtypes, since again you can't have newtype GADTs.
+
+But for now at least, we keep the simplest choice. See #18891 and !4419
+for more discussion of this issue.a
+
-}
=====================================
testsuite/tests/dependent/should_fail/T13780a.hs
=====================================
@@ -1,9 +1,11 @@
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE DataKinds, PolyKinds #-}
module T13780a where
-data family Sing (a :: k)
+data family Sing (c :: k)
+
+data Foo b = b ~ Bool => MkFoo
-data Foo a = a ~ Bool => MkFoo
data instance Sing (z :: Foo a) = (z ~ MkFoo) => SMkFoo
=====================================
testsuite/tests/th/T9692.hs
=====================================
@@ -12,7 +12,7 @@ class C a where
data F a (b :: k) :: Type
instance C Int where
- data F Int x = FInt x
+ data F Int (x :: Type) = FInt x
$( do info <- qReify (mkName "F")
runIO $ putStrLn $ pprint info
=====================================
testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs
=====================================
@@ -4,6 +4,7 @@
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE GADTs #-}
module UnliftedNewtypesUnassociatedFamily where
@@ -20,7 +21,14 @@ newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep])
data instance DFT 'LiftedRep = MkDFT4 | MkDFT5
data family DF :: TYPE (r :: RuntimeRep)
-newtype instance DF = MkDF1 Int#
-newtype instance DF = MkDF2 Word#
-newtype instance DF = MkDF3 (# Int#, Word# #)
+
+newtype instance DF :: TYPE 'IntRep where
+ MkDF1 :: Int# -> DF
+
+newtype instance DF :: TYPE 'WordRep where
+ MkDF2 :: Word# -> DF
+
+newtype instance DF :: TYPE ('TupleRep '[ 'IntRep, 'WordRep ]) where
+ MkDF3 :: (# Int#, Word# #) -> DF
+
data instance DF = MkDF4 | MkDF5
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr
=====================================
@@ -1,11 +1,5 @@
-UnliftedNewtypesFamilyKindFail2.hs:12:20:
- Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
- In the first argument of ‘F’, namely ‘5’
- In the newtype instance declaration for ‘F’
-
-UnliftedNewtypesFamilyKindFail2.hs:12:31:
- Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
- In the first argument of ‘F’, namely ‘5’
- In the type ‘(F 5)’
- In the definition of data constructor ‘MkF’
+UnliftedNewtypesFamilyKindFail2.hs:12:20: error:
+ • Expected a type, but ‘5’ has kind ‘GHC.Num.Natural.Natural’
+ • In the first argument of ‘F’, namely ‘5’
+ In the newtype instance declaration for ‘F’
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr
=====================================
@@ -5,10 +5,3 @@ UnliftedNewtypesInstanceFail.hs:13:3: error:
but ‘Bar Bool’ has kind ‘TYPE 'IntRep’
• In the newtype instance declaration for ‘Bar’
In the instance declaration for ‘Foo Bool’
-
-UnliftedNewtypesInstanceFail.hs:14:17: error:
- • Couldn't match kind ‘'WordRep’ with ‘'IntRep’
- Expected kind ‘TYPE 'IntRep’, but ‘Word#’ has kind ‘TYPE 'WordRep’
- • In the type ‘Word#’
- In the definition of data constructor ‘BarBoolC’
- In the newtype instance declaration for ‘Bar’
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE UnliftedNewtypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE GADTs #-}
+
+module UnliftedNewtypesUnassociatedFamily where
+
+import GHC.Int (Int(I#))
+import GHC.Word (Word(W#))
+import GHC.Exts (Int#,Word#)
+import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep))
+
+data family DF :: TYPE (r :: RuntimeRep)
+
+-- All these fail: see #18891 and !4419
+-- See Note [Kind inference for data family instances]
+-- in GHC.Tc.TyCl.Instance
+newtype instance DF = MkDF1a Int#
+newtype instance DF = MkDF2a Word#
+newtype instance DF = MkDF3a (# Int#, Word# #)
=====================================
testsuite/tests/typecheck/should_fail/UnliftedNewtypesUnassociatedFamilyFail.stderr
=====================================
@@ -0,0 +1,18 @@
+
+UnliftedNewtypesUnassociatedFamilyFail.hs:21:30: error:
+ • Expecting a lifted type, but ‘Int#’ is unlifted
+ • In the type ‘Int#’
+ In the definition of data constructor ‘MkDF1a’
+ In the newtype instance declaration for ‘DF’
+
+UnliftedNewtypesUnassociatedFamilyFail.hs:22:30: error:
+ • Expecting a lifted type, but ‘Word#’ is unlifted
+ • In the type ‘Word#’
+ In the definition of data constructor ‘MkDF2a’
+ In the newtype instance declaration for ‘DF’
+
+UnliftedNewtypesUnassociatedFamilyFail.hs:23:30: error:
+ • Expecting a lifted type, but ‘(# Int#, Word# #)’ is unlifted
+ • In the type ‘(# Int#, Word# #)’
+ In the definition of data constructor ‘MkDF3a’
+ In the newtype instance declaration for ‘DF’
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -546,6 +546,7 @@ test('UnliftedNewtypesConstraintFamily', normal, compile_fail, [''])
test('UnliftedNewtypesMismatchedKind', normal, compile_fail, [''])
test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, [''])
test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, [''])
+test('UnliftedNewtypesUnassociatedFamilyFail', normal, compile_fail, [''])
test('T13834', normal, compile_fail, [''])
test('T17077', normal, compile_fail, [''])
test('T16512a', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/66356469127cf1b67b00ee3a1dbaf382776cdbb1
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/66356469127cf1b67b00ee3a1dbaf382776cdbb1
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201124/6e018530/attachment-0001.html>
More information about the ghc-commits
mailing list