[commit: ghc] ghc-8.4: Implement stopgap solution for #14728 (c21a8cc)
git at git.haskell.org
git at git.haskell.org
Mon Feb 19 20:06:39 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : ghc-8.4
Link : http://ghc.haskell.org/trac/ghc/changeset/c21a8cc2210a8a1b01de1a05f4f83ad6a6bad652/ghc
>---------------------------------------------------------------
commit c21a8cc2210a8a1b01de1a05f4f83ad6a6bad652
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date: Sun Feb 18 11:00:40 2018 -0500
Implement stopgap solution for #14728
It turns out that one can produce ill-formed Core by
combining `GeneralizedNewtypeDeriving`, `TypeInType`, and
`TypeFamilies`, as demonstrated in #14728. The root of the problem
is allowing the last parameter of a class to appear in a //kind// of
an associated type family, as our current approach to deriving
associated type family instances simply doesn't work well for that
situation.
Although it might be possible to properly implement this feature
today (see https://ghc.haskell.org/trac/ghc/ticket/14728#comment:3
for a sketch of how this might work), there does not currently exist
a performant implementation of the algorithm needed to accomplish
this. Until such an implementation surfaces, we will make this corner
case of `GeneralizedNewtypeDeriving` an error.
Test Plan: make test TEST="T14728a T14728b"
Reviewers: bgamari
Reviewed By: bgamari
Subscribers: rwbarton, thomie, carter
GHC Trac Issues: #14728
Differential Revision: https://phabricator.haskell.org/D4402
(cherry picked from commit 1ede46d415757f53af33bc6672bd9d3fba7f205d)
>---------------------------------------------------------------
c21a8cc2210a8a1b01de1a05f4f83ad6a6bad652
compiler/typecheck/TcDeriv.hs | 43 ++++++++++++++++++++--
testsuite/tests/deriving/should_fail/T14728a.hs | 20 ++++++++++
.../tests/deriving/should_fail/T14728a.stderr | 7 ++++
testsuite/tests/deriving/should_fail/T14728b.hs | 16 ++++++++
.../tests/deriving/should_fail/T14728b.stderr | 7 ++++
testsuite/tests/deriving/should_fail/all.T | 2 +
6 files changed, 92 insertions(+), 3 deletions(-)
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 33ce581..a93712c 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -1314,6 +1314,8 @@ mkNewTypeEqn
&& ats_ok
-- Check (b) from Note [GND and associated type families]
&& isNothing at_without_last_cls_tv
+ -- Check (d) from Note [GND and associated type families]
+ && isNothing at_last_cls_tv_in_kinds
-- Check that eta reduction is OK
eta_ok = rep_tc_args `lengthAtLeast` nt_eta_arity
@@ -1330,6 +1332,12 @@ mkNewTypeEqn
at_without_last_cls_tv
= find (\tc -> last_cls_tv `notElem` tyConTyVars tc) atf_tcs
+ at_last_cls_tv_in_kinds
+ = find (\tc -> any (at_last_cls_tv_in_kind . tyVarKind)
+ (tyConTyVars tc)
+ || at_last_cls_tv_in_kind (tyConResKind tc)) atf_tcs
+ at_last_cls_tv_in_kind kind
+ = last_cls_tv `elemVarSet` exactTyCoVarsOfType kind
at_tcs = classATs cls
last_cls_tv = ASSERT( notNull cls_tyvars )
last cls_tyvars
@@ -1337,14 +1345,22 @@ mkNewTypeEqn
cant_derive_err
= vcat [ ppUnless eta_ok eta_msg
, ppUnless ats_ok ats_msg
- , maybe empty at_tv_msg
- at_without_last_cls_tv]
+ , maybe empty at_without_last_cls_tv_msg
+ at_without_last_cls_tv
+ , maybe empty at_last_cls_tv_in_kinds_msg
+ at_last_cls_tv_in_kinds
+ ]
eta_msg = text "cannot eta-reduce the representation type enough"
ats_msg = text "the class has associated data types"
- at_tv_msg at_tc = hang
+ at_without_last_cls_tv_msg at_tc = hang
(text "the associated type" <+> quotes (ppr at_tc)
<+> text "is not parameterized over the last type variable")
2 (text "of the class" <+> quotes (ppr cls))
+ at_last_cls_tv_in_kinds_msg at_tc = hang
+ (text "the associated type" <+> quotes (ppr at_tc)
+ <+> text "contains the last type variable")
+ 2 (text "of the class" <+> quotes (ppr cls)
+ <+> text "in a kind, which is not (yet) allowed")
MASSERT( cls_tys `lengthIs` (classArity cls - 1) )
case mb_strat of
@@ -1530,6 +1546,27 @@ However, we must watch out for three things:
GHC's termination checker isn't sophisticated enough to conclude that the
definition of T MyInt terminates, so UndecidableInstances is required.
+(d) For the time being, we do not allow the last type variable of the class to
+ appear in a /kind/ of an associated type family definition. For instance:
+
+ class C a where
+ type T1 a -- OK
+ type T2 (x :: a) -- Illegal: a appears in the kind of x
+ type T3 y :: a -- Illegal: a appears in the kind of (T3 y)
+
+ The reason we disallow this is because our current approach to deriving
+ associated type family instances—i.e., by unwrapping the newtype's type
+ constructor as shown above—is ill-equipped to handle the scenario when
+ the last type variable appears as an implicit argument. In the worst case,
+ allowing the last variable to appear in a kind can result in improper Core
+ being generated (see #14728).
+
+ There is hope for this feature being added some day, as one could
+ conceivably take a newtype axiom (which witnesses a coercion between a
+ newtype and its representation type) at lift that through each associated
+ type at the Core level. See #14728, comment:3 for a sketch of how this
+ might work. Until then, we disallow this featurette wholesale.
+
************************************************************************
* *
\subsection[TcDeriv-normal-binds]{Bindings for the various classes}
diff --git a/testsuite/tests/deriving/should_fail/T14728a.hs b/testsuite/tests/deriving/should_fail/T14728a.hs
new file mode 100644
index 0000000..28cf8e0
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728a.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14728a where
+
+import Data.Functor.Identity
+import Data.Kind
+
+class C (a :: Type) where
+ type T a (x :: a) :: Type
+ type U z :: a
+
+instance C () where
+ type T () '() = Bool
+
+deriving instance C (Identity a)
+
+f :: T (Identity ()) ('Identity '())
+f = True
diff --git a/testsuite/tests/deriving/should_fail/T14728a.stderr b/testsuite/tests/deriving/should_fail/T14728a.stderr
new file mode 100644
index 0000000..b76d073
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728a.stderr
@@ -0,0 +1,7 @@
+
+T14728a.hs:17:1: error:
+ • Can't make a derived instance of ‘C (Identity a)’
+ (even with cunning GeneralizedNewtypeDeriving):
+ the associated type ‘T’ contains the last type variable
+ of the class ‘C’ in a kind, which is not (yet) allowed
+ • In the stand-alone deriving instance for ‘C (Identity a)’
diff --git a/testsuite/tests/deriving/should_fail/T14728b.hs b/testsuite/tests/deriving/should_fail/T14728b.hs
new file mode 100644
index 0000000..7fdfcb3
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728b.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T14728b where
+
+import Data.Functor.Identity
+import Data.Kind
+
+class C (a :: Type) where
+ type U z :: a
+
+instance C () where
+ type U z = '()
+
+deriving instance C (Identity a)
diff --git a/testsuite/tests/deriving/should_fail/T14728b.stderr b/testsuite/tests/deriving/should_fail/T14728b.stderr
new file mode 100644
index 0000000..ee74f8b4
--- /dev/null
+++ b/testsuite/tests/deriving/should_fail/T14728b.stderr
@@ -0,0 +1,7 @@
+
+T14728b.hs:16:1: error:
+ • Can't make a derived instance of ‘C (Identity a)’
+ (even with cunning GeneralizedNewtypeDeriving):
+ the associated type ‘U’ contains the last type variable
+ of the class ‘C’ in a kind, which is not (yet) allowed
+ • In the stand-alone deriving instance for ‘C (Identity a)’
diff --git a/testsuite/tests/deriving/should_fail/all.T b/testsuite/tests/deriving/should_fail/all.T
index c9b8469..acd3486 100644
--- a/testsuite/tests/deriving/should_fail/all.T
+++ b/testsuite/tests/deriving/should_fail/all.T
@@ -69,3 +69,5 @@ test('T12512', omit_ways(['ghci']), compile_fail, [''])
test('T12801', normal, compile_fail, [''])
test('T14365', [extra_files(['T14365B.hs','T14365B.hs-boot'])],
multimod_compile_fail, ['T14365A',''])
+test('T14728a', normal, compile_fail, [''])
+test('T14728b', normal, compile_fail, [''])
More information about the ghc-commits
mailing list