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

5 Jul 2018

      #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       |           Version:  8.5
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 The following program typechecks on GHC 8.6.1-alpha1:

 {{{#!hs
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 module SGenerics where

 import Data.Kind
 import Data.Type.Equality
 import Data.Void

 -----
 -- singletons machinery
 -----

 data family Sing :: forall k. k -> Type

 data instance Sing :: () -> Type where
   STuple0 :: Sing '()

 type Refuted a = a -> Void
 data Decision a = Proved a | Disproved (Refuted a)

 -----
 -- A stripped down version of GHC.Generics
 -----

 data U1 = MkU1
 data instance Sing (z :: U1) where
   SMkU1 :: Sing MkU1

 -----

 class Generic (a :: Type) where
     type Rep a :: Type
     from :: a -> Rep a
     to :: Rep a -> a

 class PGeneric (a :: Type) where
   type PFrom (x :: a)     :: Rep a
   type PTo   (x :: Rep a) :: a

 class SGeneric k where
   sFrom :: forall (a :: k).     Sing a -> Sing (PFrom a)
   sTo   :: forall (a :: Rep k). Sing a -> Sing (PTo a :: k)
   sTof  :: forall (a :: k).     Sing a -> PTo (PFrom a) :~: a
   sFot  :: forall (a :: Rep k). Sing a -> PFrom (PTo a :: k) :~: a

 -----

 instance Generic () where
   type Rep () = U1
   from () = MkU1
   to MkU1 = ()

 instance PGeneric () where
   type PFrom '()   = MkU1
   type PTo   'MkU1 = '()

 instance SGeneric () where
   sFrom STuple0 = SMkU1
   sTo   SMkU1   = STuple0
   sTof  STuple0 = Refl
   sFot  SMkU1   = Refl

 -----

 class SDecide k where
   -- | Compute a proof or disproof of equality, given two singletons.
   (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
   default (%~) :: forall (a :: k) (b :: k). (SGeneric k, SDecide (Rep k))
                => Sing a -> Sing b -> Decision (a :~: b)
   s1 %~ s2 = case sFrom s1 %~ sFrom s2 of
     Proved (Refl :: PFrom a :~: PFrom b) ->
       let r :: PTo (PFrom a) :~: PTo (PFrom b)
           r = Refl

           sTof1 :: PTo (PFrom a) :~: a
           sTof1 = sTof s1

           sTof2 :: PTo (PFrom b) :~: b
           sTof2 = sTof s2
       in Proved (sym sTof1 `trans` r `trans` sTof2)
     Disproved contra -> Disproved (\Refl -> contra Refl)

 instance SDecide U1 where
   SMkU1 %~ SMkU1 = Proved Refl

 instance SDecide ()
 }}}

 However, it throws a Core Lint error with `-dcore-lint`. The full error is
 absolutely massive, so I'll attach it separately. Here is the top-level
 bit:

 {{{
 *** Core Lint errors : in result of Simplifier ***
 <no location info>: warning:
     In the expression: <elided>
     From-type of Cast differs from type of enclosed expression
     From-type: U1
     Type of enclosed expr: Rep ()
     Actual enclosed expr: PFrom a_a1Fm
     Coercion used in cast: Sym (D:R:Rep()[0])
 }}}

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15346
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler