[commit: ghc] master: Fix newtype instance GADTs (9275186)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/927518668111584a06f12bd9eb1b0910a38acf4f/ghc

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

commit 927518668111584a06f12bd9eb1b0910a38acf4f
Author: Ryan Scott <ryan.gl.scott at gmail.com>
Date:   Thu Jul 5 08:49:50 2018 -0400

    Fix newtype instance GADTs
    
    Summary: This was taken from Richard's branch, which in turn was
    submitted to Phab by Matthew, which in turn was commandeered by Ryan.
    
    This fixes an issue with newtype instances in which too many
    coercions were being applied in the worker. This fixes the issue by
    removing the data family instance axiom from the worker and moving
    to the wrapper. Moreover, we now require all newtype instances
    to have wrappers, for symmetry with data instances.
    
    Reviewers: goldfire, bgamari, simonpj, mpickering
    
    Reviewed By: mpickering
    
    Subscribers: simonpj, rwbarton, thomie, carter
    
    GHC Trac Issues: #15318
    
    Differential Revision: https://phabricator.haskell.org/D4902


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

927518668111584a06f12bd9eb1b0910a38acf4f
 compiler/basicTypes/MkId.hs                        | 52 ++++++++++++++++++----
 .../tests/indexed-types/should_compile/T15318.hs   |  8 ++++
 testsuite/tests/indexed-types/should_compile/all.T |  1 +
 3 files changed, 52 insertions(+), 9 deletions(-)

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 602cd3d..4cd20ff 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -19,8 +19,7 @@ module MkId (
 
         mkPrimOpId, mkFCallId,
 
-        wrapNewTypeBody, unwrapNewTypeBody,
-        wrapFamInstBody,
+        unwrapNewTypeBody, wrapFamInstBody,
         DataConBoxer(..), mkDataConRep, mkDataConWorkId,
 
         -- And some particular Ids; see below for why they are wired in
@@ -247,6 +246,47 @@ Hence we translate to
         -- Coercion from family type to representation type
   Co7T a :: T [a] ~ :R7T a
 
+Newtype instances through an additional wrinkle into the mix. Consider the
+following example (adapted from #15318, comment:2):
+
+  data family T a
+  newtype instance T [a] = MkT [a]
+
+Within the newtype instance, there are three distinct types at play:
+
+1. The newtype's underlying type, [a].
+2. The instance's representation type, TList a (where TList is the
+   representation tycon).
+3. The family type, T [a].
+
+We need two coercions in order to cast from (1) to (3):
+
+(a) A newtype coercion axiom:
+
+      axiom coTList a :: TList a ~ [a]
+
+    (Where TList is the representation tycon of the newtype instance.)
+
+(b) A data family instance coercion axiom:
+
+      axiom coT a :: T [a] ~ TList a
+
+When we translate the newtype instance to Core, we obtain:
+
+    -- Wrapper
+  $WMkT :: forall a. [a] -> T [a]
+  $WMkT a x = MkT a x |> Sym (coT a)
+
+    -- Worker
+  MkT :: forall a. [a] -> TList [a]
+  MkT a x = x |> Sym (coTList a)
+
+Unlike for data instances, the worker for a newtype instance is actually an
+executable function which expands to a cast, but otherwise, the general
+strategy is essentially the same as for data instances. Also note that we have
+a wrapper, which is unusual for a newtype, but we make GHC produce one anyway
+for symmetry with the way data instances are handled.
+
 Note [Newtype datacons]
 ~~~~~~~~~~~~~~~~~~~~~~~
 The "data constructor" for a newtype should always be vanilla.  At one
@@ -614,8 +654,8 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
                      -- of some newtypes written with GADT syntax. See below.
          && (any isBanged (ev_ibangs ++ arg_ibangs)
                      -- Some forcing/unboxing (includes eq_spec)
-             || isFamInstTyCon tycon  -- Cast result
              || (not $ null eq_spec))) -- GADT
+      || isFamInstTyCon tycon -- Cast result
       || dataConUserTyVarsArePermuted data_con
                      -- If the data type was written with GADT syntax and
                      -- orders the type variables differently from what the
@@ -1009,15 +1049,9 @@ wrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
 --
 -- If a coercion constructor is provided in the newtype, then we use
 -- it, otherwise the wrap/unwrap are both no-ops
---
--- If the we are dealing with a newtype *instance*, we have a second coercion
--- identifying the family instance with the constructor of the newtype
--- instance.  This coercion is applied in any case (ie, composed with the
--- coercion constructor of the newtype or applied by itself).
 
 wrapNewTypeBody tycon args result_expr
   = ASSERT( isNewTyCon tycon )
-    wrapFamInstBody tycon args $
     mkCast result_expr (mkSymCo co)
   where
     co = mkUnbranchedAxInstCo Representational (newTyConCo tycon) args []
diff --git a/testsuite/tests/indexed-types/should_compile/T15318.hs b/testsuite/tests/indexed-types/should_compile/T15318.hs
new file mode 100644
index 0000000..342b6ef
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15318.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+module T15138 where
+
+data family Sn a
+newtype instance Sn (Either a b) where
+  SnC :: forall b a. Char -> Sn (Either a b)
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 6255dd2..5cecd52 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -284,5 +284,6 @@ test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
 test('T13777', normal, compile, [''])
 test('T14164', normal, compile, [''])
+test('T15318', normal, compile, [''])
 test('T15322', normal, compile, [''])
 test('T15322a', normal, compile_fail, [''])