Re: [GHC] #13025: Type family reduction irregularity (change from 7.10.3 to 8.0.1)

23 Dec 2016

      #13025: Type family reduction irregularity (change from 7.10.3 to 8.0.1)
-------------------------------------+-------------------------------------
        Reporter:  acowley           |                Owner:
            Type:  bug               |               Status:  merge
        Priority:  normal            |            Milestone:  8.0.3
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  Runtime           |            Test Case:
  performance bug                    |  simplCore/should_compile/T13025
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 I don't think your patch is quite right, Simon. Here is the main payload:

 {{{
 pushCoArg :: Coercion -> CoreArg -> Maybe (CoreArg, Coercion)
 -- We have (fun |> co) arg, and we want to transform it to
 --         (fun arg) |> co
 -- This may fail, e.g. if (fun :: N) where N is a newtype
 -- C.f. simplCast in Simplify.hs

 pushCoArg co arg
   = case arg of
       Type ty | isForAllTy tyL
         -> ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
            Just (Type ty, mkInstCo co (mkNomReflCo ty))

       _ | isFunTy tyL
         , [co1, co2] <- decomposeCo 2 co
               -- If   co  :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
               -- then co1 :: tyL1 ~ tyR1
               --      co2 :: tyL2 ~ tyR2
         -> ASSERT2( isFunTy tyR, ppr co $$ ppr arg )
            Just (mkCast arg (mkSymCo co1), co2)

       _ -> Nothing
   where
     Pair tyL tyR = coercionKind co
 }}}

 This implements two of the push rules from every FC paper. But note that
 forall-types can now be heterogeneous. That is, `fun` and `fun |> co`
 might expect types of different kinds. Your patch does not take this
 possibility into account. I recommend this:

 {{{
 case arg of
   Type ty | isForAllTy tyL
     -> ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
        -- co :: (forall (a1 :: k1). ty1) ~ (forall (a2 :: k2). ty2)
        let co1 = mkSymCo (mkNthCo 0 co)
            -- co1 :: k2 ~ k1

            ty' = ty `mkCastTy` co1

            co2 = mkInstCo co (mkCoherenceLeftCo (mkNomReflCo ty) (mkSymCo
 co1))
            -- co2 :: ty1[ty |> co1 / a1] ~ ty2[ty / a2]

        in Just (Type ty', co2)
 }}}

 Note that `NthCo` can extract an equality between the kinds of the types
 related by a coercion between forall-types. See the `NthCo` case in
 !CoreLint.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13025#comment:13
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler