[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):

 As far as the other Core Lint error goes, I think I've narrowed it down to
 [http://git.haskell.org/ghc.git/blob/671537364ae09dc65d4bb1c646aa80e9c8f808df:/compiler/coreSyn/CoreOpt.hs#l1056
 pushCoDataCon] (which implements the `S_KPush` rule from //System FC with
 Explicit Kind Equality//), as that's the function that annotates `$ctest`
 with the coercion `forall (a :: Sym (D:R:Rep()[0])). (Proxy (Sym
 (D:R:Rep()[0])) <a>_P)_R`.

 I tried tracing through the steps of `S_KPush` to see if this coercion is
 what should have been produced, but I'm uncertain in my results simply
 because the way that GHC represents type abstraction congruence coercions
 is slightly different than the way they're represented in the paper.

 In the paper, a type abstraction congruence coercion is of the form:

 {{{
 ∀_η (a_1, a_2, c). γ
 }}}

 Where `η` is a kind coercion, `a_1` and `a_2` are two fresh type variables
 inhabiting the from- and to-kinds of `η`, respectively, and `c` is a fresh
 coercion variable witnessing `a_1 ~ a_2`. See the `CT_AllT` rule in Figure
 4 for a complete presentation of how it's typed.

 Since the type of `$ctest` is `∀(a : k). Proxy k a`, applying `Ψ` to this
 type (where `Ψ` is defined in Section 5 of the paper) should produce:

 {{{
 ∀_(Sym (D:R:Rep()[0])) (a_1, a_2, c). <Proxy> (Sym (D:R:Rep()[0])) c
 }}}

 This does look a bit different than the coercion that GHC is actually
 producing, since the last argument to `<Proxy>` is `c` instead of `<a>`.
 However, it's quite hard for me to determine if this difference is
 intentional, especially after reading GHC's
 [http://git.haskell.org/ghc.git/blob/671537364ae09dc65d4bb1c646aa80e9c8f808df:/compiler/types/TyCoRep.hs#l1038
 Note [Forall coercions]], which presents the typing rule as:

 {{{
 kind_co : k1 ~ k2
 tv1:k1 |- co : t1 ~ t2
 -------------------------------------------------------------------
 ForAllCo tv1 kind_co co : all tv1:k1. t1  ~
                           all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
 }}}

 This presentation is quite different from the `CT_AllT` typing rule in the
 paper, as it does not introduce two fresh type variables of different
 kinds equated by a coercion variable. Instead, it uses the same type
 variable in both sides of the `ForAllCo`, and tries to fix up the kind of
 the type variable in the to-type with this strange `tv1 |> sym kind_co`
 coercion.

 GHC's unusual treatment of this typing rule at least explains why the kind
 of the coercion we see in this program is `(forall (a :: ()). Proxy () a)
 ~R# (forall (a :: Rep ()). Proxy (Rep ()) (a |> D:R:Rep()[0]))`. Still, I
 find it difficult to convince myself that this alternate treatment is
 correct. After all, the type `forall (a :: Rep ()). Proxy (Rep ()) (a |>
 D:R:Rep()[0])` looks blatantly ill kinded to me, since `(a |>
 D:R:Rep()[0])` is of kind `()`, not `Rep ()` as it claims.

 Richard, do you have any insights here?

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