Commit 1ede46d4 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

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
parent 90804660
......@@ -1308,6 +1308,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
......@@ -1324,6 +1326,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
......@@ -1331,14 +1339,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
......@@ -1525,6 +1541,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}
......
{-# 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
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)’
{-# 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)
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)’
......@@ -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, [''])
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