#15318 closed bug (fixed)

Core Lint error involving newtype family instances with wrappers

Reported by: RyanGlScott Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler (Type checker) Version: 8.4.3
Keywords: TypeFamilies Cc: mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash or panic Test Case: indexed-types/should_compile/T15318
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4902
Wiki Page:

Description

The following program gives a Core Lint error on GHC 8.4 and later:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

data family Sn a
newtype instance Sn (Either a b) where
  SnC :: forall b a. Char -> Sn (Either a b)
$ /opt/ghc/8.4.3/bin/ghc -dcore-lint Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
    [in body of lambda with binder dt_aZm :: Char]
    From-type of Cast differs from type of enclosed expression
    From-type: R:SnEither a_auS b_auR
    Type of enclosed expr: Sn (Either a_auS b_auR)
    Actual enclosed expr: dt_aZm
                          `cast` (Sym (N:R:SnEither[0]
                                           <a_auS>_N <b_auR>_N) ; Sym (D:R:SnEither0[0]
                                                                           <a_auS>_N <b_auR>_N)
                                  :: (Char :: *) ~R# (Sn (Either a_auS b_auR) :: *))
    Coercion used in cast: Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
*** Offending Program ***
$WSnC [InlPrag=INLINE[2]] :: forall b a. Char -> Sn (Either a b)
[GblId[DataConWrapper],
 Arity=1,
 Caf=NoCafRefs,
 Str=<L,U>,
 Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)
         Tmpl= \ (@ b_auR) (@ a_auS) (dt_aZm [Occ=Once] :: Char) ->
                 (dt_aZm
                  `cast` (Sym (N:R:SnEither[0]
                                   <a_auS>_N <b_auR>_N) ; Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
                          :: (Char :: *) ~R# (Sn (Either a_auS b_auR) :: *)))
                 `cast` (Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
                         :: (R:SnEither a_auS b_auR :: *)
                            ~R# (Sn (Either a_auS b_auR) :: *))}]
$WSnC
  = \ (@ b_auR) (@ a_auS) (dt_aZm [Occ=Once] :: Char) ->
      (dt_aZm
       `cast` (Sym (N:R:SnEither[0]
                        <a_auS>_N <b_auR>_N) ; Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
               :: (Char :: *) ~R# (Sn (Either a_auS b_auR) :: *)))
      `cast` (Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
              :: (R:SnEither a_auS b_auR :: *)
                 ~R# (Sn (Either a_auS b_auR) :: *))

$trModule1_r10g :: Addr#
[GblId, Caf=NoCafRefs]
$trModule1_r10g = "main"#

$trModule2_r10D :: TrName
[GblId, Caf=NoCafRefs]
$trModule2_r10D = TrNameS $trModule1_r10g

$trModule3_r10E :: Addr#
[GblId, Caf=NoCafRefs]
$trModule3_r10E = "Bug"#

$trModule4_r10F :: TrName
[GblId, Caf=NoCafRefs]
$trModule4_r10F = TrNameS $trModule3_r10E

$trModule :: Module
[GblId, Caf=NoCafRefs]
$trModule = Module $trModule2_r10D $trModule4_r10F

$krep_r10G :: KindRep
[GblId]
$krep_r10G = KindRepTyConApp $tcChar ([] @ KindRep)

$krep1_r10H :: KindRep
[GblId, Caf=NoCafRefs]
$krep1_r10H = KindRepVar 1#

$krep2_r10I :: KindRep
[GblId, Caf=NoCafRefs]
$krep2_r10I = KindRepVar 0#

$krep3_r10J :: [KindRep]
[GblId, Caf=NoCafRefs]
$krep3_r10J = : @ KindRep $krep2_r10I ([] @ KindRep)

$krep4_r10K :: [KindRep]
[GblId, Caf=NoCafRefs]
$krep4_r10K = : @ KindRep $krep1_r10H $krep3_r10J

$krep5_r10L :: KindRep
[GblId]
$krep5_r10L = KindRepTyConApp $tcEither $krep4_r10K

$tcSn1_r10M :: Addr#
[GblId, Caf=NoCafRefs]
$tcSn1_r10M = "Sn"#

$tcSn2_r10N :: TrName
[GblId, Caf=NoCafRefs]
$tcSn2_r10N = TrNameS $tcSn1_r10M

$tcSn :: TyCon
[GblId]
$tcSn
  = TyCon
      461968091845555535##
      16320521938866097056##
      $trModule
      $tcSn2_r10N
      0#
      krep$*Arr*

$krep6_r10O :: [KindRep]
[GblId]
$krep6_r10O = : @ KindRep $krep5_r10L ([] @ KindRep)

$krep7_r10P :: KindRep
[GblId]
$krep7_r10P = KindRepTyConApp $tcSn $krep6_r10O

$krep8_r10Q :: KindRep
[GblId]
$krep8_r10Q = KindRepFun $krep_r10G $krep7_r10P

$tc'SnC1_r10R :: Addr#
[GblId, Caf=NoCafRefs]
$tc'SnC1_r10R = "'SnC"#

$tc'SnC2_r10S :: TrName
[GblId, Caf=NoCafRefs]
$tc'SnC2_r10S = TrNameS $tc'SnC1_r10R

$tc'SnC :: TyCon
[GblId]
$tc'SnC
  = TyCon
      3818830880305712792##
      17484539998814842835##
      $trModule
      $tc'SnC2_r10S
      2#
      $krep8_r10Q

*** End of Offense ***


<no location info>: error: 
Compilation had errors

If we look at the Core for $WSnC, we see the culprit:

$WSnC
  = \ (@ b_auR) (@ a_auS) (dt_aZm [Occ=Once] :: Char) ->
      (dt_aZm
       `cast` (Sym (N:R:SnEither[0]
                        <a_auS>_N <b_auR>_N) ; Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
               :: (Char :: *) ~R# (Sn (Either a_auS b_auR) :: *)))
      `cast` (Sym (D:R:SnEither0[0] <a_auS>_N <b_auR>_N)
              :: (R:SnEither a_auS b_auR :: *)
                 ~R# (Sn (Either a_auS b_auR) :: *))

The inner cast goes from Char to Sn (Either a b), but then the outer cast goes from R:SnEither a b to Sn (Either a b), which is not transitive.

Change History (5)

comment:1 Changed 15 months ago by mpickering

Differential Rev(s): Phab:D4902

See https://phabricator.haskell.org/D4902 which is Richard's fix cherry-picked with Ryan's test. A team effort.

Last edited 15 months ago by mpickering (previous) (diff)

comment:2 Changed 15 months ago by simonpj

Yes, Phab:D4902 will fix the bug, but it perpetuates a mistake!

Consider

  data family S a
  data family T a
  
  data    instance S [a] = MkS a
  newtype instance T [a] = MkT a

Currently, we get this:

  data SList a = MkS a
  axiom coS a :: SList a ~ S [a]

  -- Wrapper for MkS
  $WMkS :: a -> S [a]
  $WMkS x = MkS x |> coS a

  -- newtype TList a = MkT a
  axiom coTList a :: a ~ TList a
  axiom coT a :: TList a ~ T [a]

  -- Worker for MkT
  MkT :: a -> T [a]
  MkT x = x |> coTList a |> coT a

Notice the inconsistency: the cast that takes us from the representation type to the final user type is done in the wrapper for data types, but in the worker for a newtype. (Reminder: for data types the worker isn't an executable function, it's the Core data constructor; but for a newtype the "worker" is an executable function that expands to a cast.)

This inconsistency shows up in the MkId functions wrapNewTypeBody and unwrapNewTypeBody. The former wraps two casts (as above) while the latter unwraps only one!

I think we can readily remove the inconsistency:

  • Don't export wrapNewTypeBody from MkId; it is not used outside.
  • Remove the extra cast from wrapNewTypeBody
  • Do not make the change to mkDataConRep proposed in Phab:D4902.
  • Make a wrapper for family-instance newtypes. Do this by making wwrapper_reqd return True for all types for which isFamInstTyCon holds. (Currently that predicate is not tested for newtypes.)

I think that might be it. It solves the problem at source, produces less code and less to explain (because it's consistent).

comment:3 Changed 15 months ago by Ryan Scott <ryan.gl.scott@…>

In 9275186/ghc:

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

comment:4 Changed 15 months ago by RyanGlScott

Status: newmerge
Test Case: indexed-types/should_compile/T15318

comment:5 Changed 14 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.