Fix newtype instance GADTs
authorRyan Scott <ryan.gl.scott@gmail.com>
Thu, 5 Jul 2018 12:49:50 +0000 (08:49 -0400)
committerBen Gamari <ben@smart-cactus.org>
Thu, 12 Jul 2018 21:06:12 +0000 (17:06 -0400)
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

(cherry picked from commit 927518668111584a06f12bd9eb1b0910a38acf4f)

compiler/basicTypes/MkId.hs
testsuite/tests/indexed-types/should_compile/T15318.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T

index d6a52b4..294a845 100644 (file)
@@ -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 (file)
index 0000000..342b6ef
--- /dev/null
@@ -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)
index 56448ac..8a2af94 100644 (file)
@@ -284,3 +284,4 @@ test('T15144', normal, compile, [''])
 test('T15122', normal, compile, [''])
 test('T13777', normal, compile, [''])
 test('T14164', normal, compile, [''])
+test('T15318', normal, compile, [''])