[commit: ghc] ghc-8.4: Implement stopgap solution for #14728 (5423035)

git at git.haskell.org git at git.haskell.org
Sun Feb 18 19:38:55 UTC 2018


Repository : ssh://git@git.haskell.org/ghc

On branch  : ghc-8.4
Link       : http://ghc.haskell.org/trac/ghc/changeset/5423035358cfd3aad274fd3c22e4e531003e7c83/ghc

>---------------------------------------------------------------

commit 5423035358cfd3aad274fd3c22e4e531003e7c83
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)


>---------------------------------------------------------------

5423035358cfd3aad274fd3c22e4e531003e7c83
 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