Opened 10 months ago

Last modified 8 months ago

#16141 merge bug (fixed)

StrictData and TypeFamilies regression

Reported by: RyanGlScott Owned by:
Priority: highest Milestone: 8.8.1
Component: Compiler (Type checker) Version: 8.6.3
Keywords: Cc: adamse
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T16141
Blocked By: Blocking:
Related Tickets: #16191 Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/88
Wiki Page:

Description

The credit goes to wuzzeb for originally discovering this bug here. I've minimized their test case slightly below:

{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

data family T
newtype instance T = MkT Int deriving Eq

With optimization enabled, this program compiles with GHC 8.0.2 through 8.4.4, but not with 8.6.3 or HEAD:

$ /opt/ghc/8.4.4/bin/ghc -fforce-recomp -O Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

$ /opt/ghc/8.6.3/bin/ghc -fforce-recomp -O Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:6:39: error:
    • Couldn't match a lifted type with an unlifted type
        arising from the coercion of the method ‘==’
          from type ‘GHC.Prim.Int# -> GHC.Prim.Int# -> Bool’
            to type ‘T -> T -> Bool’
    • When deriving the instance for (Eq T)
  |
6 | newtype instance T = MkT Int deriving Eq
  |                                       ^^

Based on the error message, it appears as if GHC mistakenly believes that the representation type of the T instance is Int#, rather than Int.

Change History (13)

comment:1 Changed 10 months ago by RyanGlScott

Hm, this appears to be my fault, as this regression was introduced in commit eb680f2c0a365b12f9b867da6bb10e9ab4b328e0 (Fix newtype instance GADTs).

comment:2 Changed 10 months ago by RyanGlScott

It turns out you don't need deriving to notice something afoot with this program. Even if you just have this:

{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

data family T
newtype instance T = MkT Int

And compile this with -O -dcore-lint, it blows up:

$ /opt/ghc/8.6.3/bin/ghc Bug.hs -O -dcore-lint    
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Tidy Core ***
<no location info>: warning:
    In a case alternative: (I# dt_aXp :: Int#)
    Type of case alternatives not the same as the annotation on case:
        Actual type: R:T
        Annotation on case: T
        Alt Rhs: dt_aXp `cast` (Sym (N:R:T[0]) :: Int# ~R# R:T)
*** Offending Program ***
$WMkT [InlPrag=INLINE[2]] :: Int -> T
[GblId[DataConWrapper],
 Arity=1,
 Caf=NoCafRefs,
 Str=<S,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=False)
         Tmpl= \ (dt_aXo [Occ=Once!] :: Int) ->
                 (case dt_aXo of { I# dt_aXp [Occ=Once] ->
                  dt_aXp `cast` (Sym (N:R:T[0]) :: Int# ~R# R:T)
                  })
                 `cast` (Sym (D:R:T0[0]) :: R:T ~R# T)}]
$WMkT
  = \ (dt_aXo [Occ=Once!] :: Int) ->
      (case dt_aXo of { I# dt_aXp [Occ=Once] ->
       dt_aXp `cast` (Sym (N:R:T[0]) :: Int# ~R# R:T)
       })
      `cast` (Sym (D:R:T0[0]) :: R:T ~R# T)

<elided>

comment:3 Changed 10 months ago by RyanGlScott

I'm starting to think that this is actually an old bug with StrictData, since the following program (which uses a plain old newtype, not a data family) also breaks Core Lint in a similar fashion with GHC 8.4.4 or later:

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

newtype T a b where
  MkT :: forall b a. Int -> T a b
$ /opt/ghc/8.4.4/bin/ghc -O -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 a case alternative: (I# dt_aXx :: Int#)
    Type of case alternatives not the same as the annotation on case:
        Actual type: T a_atk b_atj
        Annotation on case: T b_atj a_atk
        Alt Rhs: dt_aXx
                 `cast` (Sym (N:T[0] <a_atk>_P <b_atj>_P)
                         :: (Int# :: TYPE 'IntRep) ~R# (T a_atk b_atj :: *))
*** Offending Program ***
$WMkT [InlPrag=INLINE[2]] :: forall b a. Int -> T a b
[GblId[DataConWrapper],
 Arity=1,
 Caf=NoCafRefs,
 Str=<S,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=False)
         Tmpl= \ (@ b_atj) (@ a_atk) (dt_aXw [Occ=Once!] :: Int) ->
                 case dt_aXw of { I# dt_aXx [Occ=Once] ->
                 dt_aXx
                 `cast` (Sym (N:T[0] <a_atk>_P <b_atj>_P)
                         :: (Int# :: TYPE 'IntRep) ~R# (T a_atk b_atj :: *))
                 }}]
$WMkT
  = \ (@ b_atj) (@ a_atk) (dt_aXw [Occ=Once!] :: Int) ->
      case dt_aXw of { I# dt_aXx [Occ=Once] ->
      dt_aXx
      `cast` (Sym (N:T[0] <a_atk>_P <b_atj>_P)
              :: (Int# :: TYPE 'IntRep) ~R# (T a_atk b_atj :: *))
      }

<elided>

The issue appears to involve newtypes with wrappers in general. (The reason why the original program only started breaking with GHC 8.6 is because commit eb680f2c0a365b12f9b867da6bb10e9ab4b328e0 changed GHC's treatment of newtype instances so that they would have wrappers where they didn't before.)

comment:4 Changed 10 months ago by RyanGlScott

The mention of Int# has me wondering: is GHC trying to unpack the Int field of MkT? If so, I would surely think that that's incorrect, since the idea of unpacking a newtype seems bogus, especially since GHC rejects this program:

λ> newtype T = MkT {-# UNPACK #-} !Int

<interactive>:1:13: error:
    • A newtype constructor cannot have a strictness annotation,
        but ‘MkT’ does
    • In the definition of data constructor ‘MkT’
      In the newtype declaration for ‘T’

Perhaps the implementation of StrictData misses this fact, however. I'll check the code to see if that is the case.

comment:5 Changed 10 months ago by adamse

Cc: adamse added

comment:6 Changed 10 months ago by RyanGlScott

My hunch appears to be correct. The dataConSrcToImplBang function is what is responsible for making decisions about strictness/unpacking w.r.t. StrictData:

-- | Unpack/Strictness decisions from source module
dataConSrcToImplBang
   :: DynFlags
   -> FamInstEnvs
   -> Type
   -> HsSrcBang
   -> HsImplBang

dataConSrcToImplBang dflags fam_envs arg_ty
                     (HsSrcBang ann unpk NoSrcStrict)
  | xopt LangExt.StrictData dflags -- StrictData => strict field
  = dataConSrcToImplBang dflags fam_envs arg_ty
                  (HsSrcBang ann unpk SrcStrict)
  | otherwise -- no StrictData => lazy field
  = HsLazy

Notice that this does not take into account whether the Type of the field belongs to a newtype or not, so this will indeed unpack the field of a newtype with StrictData + -O enabled. Yikes.

One could fix this by propagating information about whether we're in a newtype or not to dataConSrcToImplBang. But then again, should we really even need to call dataConSrcToImplBang if we're dealing with a newtype? dataConSrcToImplBang is internal to MkId and only has one call site, so I'm inclined to just avoid invoking it at its call site, like so:

  • compiler/basicTypes/MkId.hs

    diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
    index 5a6f1fbf96..fa3d6785b7 100644
    a b mkDataConRep dflags fam_envs wrap_name mb_bangs data_con 
    637637             -- Because we are going to apply the eq_spec args manually in the
    638638             -- wrapper
    639639
    640     arg_ibangs =
    641       case mb_bangs of
    642         Nothing    -> zipWith (dataConSrcToImplBang dflags fam_envs)
    643                               orig_arg_tys orig_bangs
    644         Just bangs -> bangs
     640    new_tycon = isNewTyCon tycon
     641    arg_ibangs
     642      | new_tycon
     643      = nOfThem (length orig_arg_tys) HsLazy
     644      | otherwise
     645      = case mb_bangs of
     646          Nothing    -> zipWith (dataConSrcToImplBang dflags fam_envs)
     647                                orig_arg_tys orig_bangs
     648          Just bangs -> bangs
    645649
    646650    (rep_tys_w_strs, wrappers)
    647651      = unzip (zipWith dataConArgRep all_arg_tys (ev_ibangs ++ arg_ibangs))
    mkDataConRep dflags fam_envs wrap_name mb_bangs data_con 
    650654    (rep_tys, rep_strs) = unzip (concat rep_tys_w_strs)
    651655
    652656    wrapper_reqd =
    653         (not (isNewTyCon tycon)
     657        (not new_tycon
    654658                     -- (Most) newtypes have only a worker, with the exception
    655659                     -- of some newtypes written with GADT syntax. See below.
    656660         && (any isBanged (ev_ibangs ++ arg_ibangs)

This certainly fixes the two programs in this ticket, and it passes the rest of the testsuite. Does this sound like the right approach?

comment:7 Changed 10 months ago by RyanGlScott

Differential Rev(s): https://gitlab.haskell.org/ghc/ghc/merge_requests/88
Status: newpatch

comment:8 Changed 9 months ago by simonpj

Good catch. I think you have the right approach.

comment:9 Changed 9 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: typecheck/should_compile/T16141

Landed in 076f5862a9e46eef762ba19fb7b14e75fa03c2c0:

commit 076f5862a9e46eef762ba19fb7b14e75fa03c2c0
Author: Ryan Scott <ryan.gl.scott@gmail.com>
Date:   Sat Jan 12 19:05:46 2019 -0500

    Don't invoke dataConSrcToImplBang on newtypes

comment:10 Changed 9 months ago by RyanGlScott

Milestone: 8.8.18.6.4
Status: closedmerge

Given the severity of this bug, and that fact that there have been multiple bug reports about this (see #16191 for another one), I'll optimistically mark this as a candidate for merging into the upcoming 8.6.4 release.

comment:11 Changed 9 months ago by Marge Bot <ben+marge-bot@…>

In a5373c1/ghc:

Fix bogus worker for newtypes

The "worker" for a newtype is actually a function
with a small (compulsory) unfolding, namely a cast.

But the construction of this function was plain wrong
for newtype /instances/; it cast the arguemnt to the
family type rather than the representation type.

This never actually bit us because, in the case of a
family instance, we immediately cast the result to
the family type.  So we get
   \x. (x |> co1) |> co2

where the compositio of co1 and co2 is ill-kinded.
However the optimiser (even the simple optimiser)
just collapsed those casts, ignoring the mis-match
in the middle, so we never saw the problem.

Trac #16191 is indeed a dup of #16141; but the resaon
these tickets produce Lint errors is not the unnecessary
forcing; it's because of the ill-typed casts.

This patch fixes the ill-typed casts, properly.  I can't
see a way to trigger an actual failure prior to this
patch, but it's still wrong wrong wrong to have ill-typed
casts, so better to get rid of them.

comment:12 Changed 8 months ago by bgamari

Status: mergeclosed

comment:13 Changed 8 months ago by bgamari

Milestone: 8.6.48.8.1
Status: closedmerge

Also needs merging for 8.8.1.

Note: See TracTickets for help on using tickets.