[GHC] #15318: Core Lint error involving newtype family instances with wrappers

[GHC]

#15318: Core Lint error involving newtype family instances with wrappers
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.6.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeFamilies   |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following program gives a Core Lint error on GHC 8.4 and later:

 {{{#!hs
 {-# 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.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15318>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler