Core Lint error involving newtype family instances with wrappers

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.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	mpickering
Operating system
Architecture