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

 Thanks, monoidal. Your program also exhibits the same Core Lint error in
 GHC 8.4, unlike the original program.

 I think it's actually easier to see what goes wrong if you add a second
 method to `SDecide` so that there's not as many coercions cluttering up
 the `-dcore-lint` output:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeApplications #-}
 module SGenerics where

 import Data.Kind
 import Data.Proxy

 -----

 type family Rep (a :: Type) :: Type
 type instance Rep () = ()

 type family PFrom (x :: a) :: Rep a

 -----

 class SDecide k where
   test :: forall (a :: k). Proxy a
   dummy :: k

 instance SDecide () where
   test = undefined
   dummy = undefined

 test1 :: forall (a :: k). SDecide (Rep k) => Proxy a
 test1 = seq (test @_ @(PFrom a)) Proxy

 test2 :: forall (a :: ()). Proxy a
 test2 = test1
 }}}

 {{{
 $ /opt/ghc/8.6.1/bin/ghci Bug.hs -dcore-lint -ddump-tc
 <elided>
 [1 of 1] Compiling SGenerics        ( Bug.hs, interpreted )
 TYPE SIGNATURES
   dummy :: forall k. SDecide k => k
   test :: forall k (a :: k). SDecide k => Proxy a
   test1 :: forall k (a :: k). SDecide (Rep k) => Proxy a
   test2 :: forall (a :: ()). Proxy a
 TYPE CONSTRUCTORS
   type family PFrom (x :: a) :: Rep a open
   type family Rep a :: * open
   class SDecide k where
     test :: forall (a :: k). Proxy a
     dummy :: k
     {-# MINIMAL test, dummy #-}
 COERCION AXIOMS
   axiom SGenerics.D:R:Rep() :: Rep () = () -- Defined at Bug.hs:15:15
 INSTANCES
   instance SDecide () -- Defined at Bug.hs:25:10
 FAMILY INSTANCES
   type instance Rep ()
 Dependent modules: []
 Dependent packages: [base-4.12.0.0, ghc-prim-0.5.3,
                      integer-gmp-1.0.2.0]

 ==================== Typechecker ====================
 <elided>

 *** Core Lint errors : in result of Simplifier ***
 Bug.hs:32:1: warning:
     [in body of lambda with binder a_a1UE :: ()]
     Kind application error in
       coercion ‘(Proxy (Sym (D:R:Rep()[0])) <a_a1Dx>_P)_R’
       Function kind = forall k. k -> *
       Arg kinds = [(Rep (), *), (a_a1Dx, ())]
     Fun: Rep ()
          (a_a1Dx, ())
 Bug.hs:32:1: warning:
     [in body of lambda with binder a_a1UE :: ()]
     From-type of Cast differs from type of enclosed expression
     From-type: ()
     Type of enclosed expr: Rep ()
     Actual enclosed expr: PFrom a_a1UE
     Coercion used in cast: Sym (D:R:Rep()[0])
 *** Offending Program ***
 <elided>

 test2 :: forall (a :: ()). Proxy a
 [LclIdX,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
          WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 10 10}]
 test2
   = \ (@ (a_a1UE :: ())) ->
       break<1>()
       break<0>()
       case ($ctest_a1UM @ (PFrom a_a1UE |> D:R:Rep()[0]))
            `cast` (Inst (forall (a :: Sym (D:R:Rep()[0])).
                          (Proxy (Sym (D:R:Rep()[0])) <a>_P)_R) (Coh <PFrom
 a_a1UE>_N
                                                                     (Sym
 (D:R:Rep()[0])))
                    :: Proxy (PFrom a_a1UE |> Sym (D:R:Rep()[0]))
                       ~R# Proxy (PFrom a_a1UE |> D:R:Rep()[0]))
       of
       { Proxy ->
       Proxy @ () @ a_a1UE
       }
 }}}

 Here, we can see exactly what goes wrong:

 * In the definition of `test2, we have the casted type `Proxy (PFrom
 a_a1UE |> Sym (D:R:Rep()[0]))`, where `a_a1UE :: ()`.
 * As can be seen in the `-ddump-tc` output, `D:R:Rep()[0] :: Rep () ~#
 ()`. Therefore, `Sym (D:R:Rep()[0]) :: () ~# Rep ()`.
 * However, `PFrom a_a1UE :: Rep ()`, so the coercion `Sym (D:R:Rep()[0])`
 is oriented the wrong way!

 -----

 There's another tiny buglet here in that Core Lint is calling `PFrom
 a_a1UE` an exclosed "expression", but it's actually a type. This is
 probably worth fixing separately.

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