Commit eb680f2c authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari
Browse files

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

(cherry picked from commit 92751866)
parent 1fca115b
...@@ -19,8 +19,7 @@ module MkId ( ...@@ -19,8 +19,7 @@ module MkId (
mkPrimOpId, mkFCallId, mkPrimOpId, mkFCallId,
wrapNewTypeBody, unwrapNewTypeBody, unwrapNewTypeBody, wrapFamInstBody,
wrapFamInstBody,
DataConBoxer(..), mkDataConRep, mkDataConWorkId, DataConBoxer(..), mkDataConRep, mkDataConWorkId,
-- And some particular Ids; see below for why they are wired in -- And some particular Ids; see below for why they are wired in
...@@ -247,6 +246,47 @@ Hence we translate to ...@@ -247,6 +246,47 @@ Hence we translate to
-- Coercion from family type to representation type -- Coercion from family type to representation type
Co7T a :: T [a] ~ :R7T a 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] Note [Newtype datacons]
~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~
The "data constructor" for a newtype should always be vanilla. At one 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 ...@@ -614,8 +654,8 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con
-- of some newtypes written with GADT syntax. See below. -- of some newtypes written with GADT syntax. See below.
&& (any isBanged (ev_ibangs ++ arg_ibangs) && (any isBanged (ev_ibangs ++ arg_ibangs)
-- Some forcing/unboxing (includes eq_spec) -- Some forcing/unboxing (includes eq_spec)
|| isFamInstTyCon tycon -- Cast result
|| (not $ null eq_spec))) -- GADT || (not $ null eq_spec))) -- GADT
|| isFamInstTyCon tycon -- Cast result
|| dataConUserTyVarsArePermuted data_con || dataConUserTyVarsArePermuted data_con
-- If the data type was written with GADT syntax and -- If the data type was written with GADT syntax and
-- orders the type variables differently from what the -- orders the type variables differently from what the
...@@ -1009,15 +1049,9 @@ wrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr ...@@ -1009,15 +1049,9 @@ wrapNewTypeBody :: TyCon -> [Type] -> CoreExpr -> CoreExpr
-- --
-- If a coercion constructor is provided in the newtype, then we use -- If a coercion constructor is provided in the newtype, then we use
-- it, otherwise the wrap/unwrap are both no-ops -- 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 wrapNewTypeBody tycon args result_expr
= ASSERT( isNewTyCon tycon ) = ASSERT( isNewTyCon tycon )
wrapFamInstBody tycon args $
mkCast result_expr (mkSymCo co) mkCast result_expr (mkSymCo co)
where where
co = mkUnbranchedAxInstCo Representational (newTyConCo tycon) args [] co = mkUnbranchedAxInstCo Representational (newTyConCo tycon) args []
......
{-# 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)
...@@ -284,3 +284,4 @@ test('T15144', normal, compile, ['']) ...@@ -284,3 +284,4 @@ test('T15144', normal, compile, [''])
test('T15122', normal, compile, ['']) test('T15122', normal, compile, [''])
test('T13777', normal, compile, ['']) test('T13777', normal, compile, [''])
test('T14164', normal, compile, ['']) test('T14164', normal, compile, [''])
test('T15318', normal, compile, [''])
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