[GHC] #15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of enclosed expression

[GHC]

#15346: Core Lint error in GHC 8.6.1: From-type of Cast differs from type of
enclosed expression
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |
      Resolution:                    |             Keywords:  TypeInType
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:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I've had quite an adventure debugging this one. I haven't quite fixed
 everything, but I have discovered one surprising fact: GHC incorrectly
 implements the `S_TPush` rule from //System FC with Explicit Kind
 Equality//. In particular, we have:

 {{{
 Γ ⊢_co γ : ∀ a: κ_1. σ_1 ~ ∀ a: κ_2. σ_2
 γ' = sym (nth^1 γ)
 τ' = τ ⊳ γ'
 ----------------------------------------- S_TPush
 (ν ⊳ γ) τ --> (ν τ') ⊳ γ@(<τ> ⊳ γ')
 }}}

 But in `CoreOpt`, GHC implements this rule as:

 {{{#!hs
 pushCoTyArg :: CoercionR -> Type -> Maybe (Type, MCoercionR)
 pushCoTyArg co ty
   ...

   | isForAllTy tyL
   = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
     Just (ty `mkCastTy` mkSymCo co1, MCo co2)

   ...
   where
     Pair tyL tyR = coercionKind co
        -- co :: tyL ~ tyR
        -- tyL = forall (a1 :: k1). ty1
        -- tyR = forall (a2 :: k2). ty2

     co1 = mkNthCo Nominal 0 co
        -- co1 :: k1 ~N k2

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

 Here, `co2` is supposed to correspond to `γ@(<τ> ⊳ γ')`, or equivalently,
 `γ@(<τ> ⊳ sym (nth^1 γ))`. But note that this definition isn't correct:
 `co2` actually calculates `γ@(<τ> ⊳ nth^1 γ)`, not `γ@(<τ> ⊳ sym (nth^1
 γ))`! To fix this, all one needs to do is apply this patch:

 {{{#!diff
 diff --git a/compiler/coreSyn/CoreOpt.hs b/compiler/coreSyn/CoreOpt.hs
 index 0353ab6..5e37fee 100644
 --- a/compiler/coreSyn/CoreOpt.hs
 +++ b/compiler/coreSyn/CoreOpt.hs
 @@ -979,7 +979,7 @@ pushCoTyArg co ty

    | isForAllTy tyL
    = ASSERT2( isForAllTy tyR, ppr co $$ ppr ty )
 -    Just (ty `mkCastTy` mkSymCo co1, MCo co2)
 +    Just (ty `mkCastTy` co1, MCo co2)

    | otherwise
    = Nothing
 @@ -989,8 +989,8 @@ pushCoTyArg co ty
         -- tyL = forall (a1 :: k1). ty1
         -- tyR = forall (a2 :: k2). ty2

 -    co1 = mkNthCo Nominal 0 co
 -       -- co1 :: k1 ~N k2
 +    co1 = mkSymCo (mkNthCo Nominal 0 co)
 +       -- co1 :: k2 ~N k1
         -- Note that NthCo can extract a Nominal equality between the
         -- kinds of the types related by a coercion between forall-types.
         -- See the NthCo case in CoreLint.
 }}}

 That fixes one of the Core Lint errors in comment:3, which is nice. But
 one remains even after applying that patch:

 {{{
 *** Core Lint errors : in result of Simplifier ***
 Bug.hs:32:1: warning:
     [in body of lambda with binder a_a1qX :: ()]
     Kind application error in
       coercion ‘(Proxy (Sym (D:R:Rep()[0])) <a_avO>_P)_R’
       Function kind = forall k. k -> Type
       Arg kinds = [(Rep (), Type), (a_avO, ())]
     Fun: Rep ()
          (a_avO, ())
 }}}

 It appears that we shouldn't be constructed the coercion `(Proxy (Sym
 (D:R:Rep()[0])) <a_avO>_P)_R`, as it's ill kinded. Using `-ddump-rule-
 rewrites`, we can see that this coercion is generated here:

 {{{
 Rule fired
     Rule: Class op test
     Module: (BUILTIN)
     Before: SGenerics.test
               TyArg SGenerics.Rep ()
               ValArg SGenerics.$fSDecide()
                      `cast` ((SGenerics.SDecide (Sym
 (SGenerics.D:R:Rep()[0])))_R
                              :: SGenerics.SDecide () ~R# SGenerics.SDecide
 (SGenerics.Rep ()))
     After:  $ctest_a1r5
             `cast` (forall (a :: Sym (SGenerics.D:R:Rep()[0])).
                     (Data.Proxy.Proxy (Sym (SGenerics.D:R:Rep()[0]))
 <a>_P)_R
                     :: (forall (a :: ()). Data.Proxy.Proxy a)
                        ~R# (forall (a :: SGenerics.Rep ()).
                             Data.Proxy.Proxy (a |>
 SGenerics.D:R:Rep()[0])))
     Cont:   ApplyToTy (SGenerics.PFrom a_a1qX)
             Select nodup wild_Xj
             Stop[RhsCtxt] Data.Proxy.Proxy a_a1qX
 }}}

 That's as far as I've come debugging thus far.

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