[GHC] #15453: Bug in opt_trans_rule in OptCoercion

[GHC]

#15453: Bug in opt_trans_rule in OptCoercion
-------------------------------------+-------------------------------------
        Reporter:  ningning          |                Owner:  ningning
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.4.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I managed to construct program which throws a Core Lint error that (I
 believe) is caused by this bug:

 {{{#!hs
 {-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Kind
 import Data.Proxy
 import Data.Type.Equality

 type family S :: Type where
   S = T
 type family T :: Type where
   T = Int

 f :: (forall (x :: S). Proxy x) :~: (forall (x :: T). Proxy x)
 f = Refl

 g :: (forall (x :: T). Proxy x) :~: (forall (x :: Int). Proxy x)
 g = Refl

 h :: (forall (x :: S). Proxy x) :~: (forall (x :: Int). Proxy x)
 h = f `trans` g
 }}}
 {{{
 $ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint -O1 -fforce-
 recomp
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of Simplifier ***
 Bug.hs:25:1: warning:
     [RHS of h :: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
                  :~: (forall (x :: Int). Proxy x)]
     From-kind of Cast differs from kind of enclosed type
     From-kind: T
     Kind of enclosed type: S
     Actual enclosed type: x_a1i3
     Coercion used in cast: D:R:T[0]
 *** Offending Program ***
 f :: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
      :~: (forall (x :: T). Proxy (x |> D:R:T[0]))
 [LclIdX,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 f = ($WRefl
        @ * @ (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])))
     `cast` (((:~:)
                <*>_N
                <forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])>_N
                (forall (x :: (D:R:S[0] ; D:R:T[0]) ; Sym (D:R:T[0])).
                 <Proxy (x |> D:R:S[0] ; D:R:T[0])>_N))_R
             :: ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
                 :~: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])))
                ~R# ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
                     :~: (forall (x :: T).
                          Proxy
                            (x |> Sym ((D:R:S[0] ; D:R:T[0]) ; Sym
 (D:R:T[0])) ; (D:R:S[0] ; D:R:T[0])))))

 g :: (forall (x :: T). Proxy (x |> D:R:T[0]))
      :~: (forall (x :: Int). Proxy x)
 [LclIdX,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 g = ($WRefl @ * @ (forall (x :: T). Proxy (x |> D:R:T[0])))
     `cast` (((:~:)
                <*>_N
                <forall (x :: T). Proxy (x |> D:R:T[0])>_N
                (forall (x :: D:R:T[0]). <Proxy (x |> D:R:T[0])>_N))_R
             :: ((forall (x :: T). Proxy (x |> D:R:T[0]))
                 :~: (forall (x :: T). Proxy (x |> D:R:T[0])))
                ~R# ((forall (x :: T). Proxy (x |> D:R:T[0]))
                     :~: (forall (x :: Int). Proxy x)))

 h :: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
      :~: (forall (x :: Int). Proxy x)
 [LclIdX,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
 h = ($WRefl
        @ * @ (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])))
     `cast` (((:~:)
                <*>_N
                <forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])>_N
                (forall (x :: D:R:S[0] ; D:R:T[0]). <Proxy (x |>
 D:R:T[0])>_N))_R
             :: ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
                 :~: (forall (x :: S). Proxy (x |> D:R:T[0])))
                ~R# ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
                     :~: (forall (x :: Int). Proxy x)))

 <elided>
 }}}

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