[GHC] #15725: Core Lint error: Trans coercion mis-match

9 Oct 2018


      #15725: Core Lint error: Trans coercion mis-match
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.6.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #15703
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I discovered this when debugging #15703. The following code fails to
 compile with `-dcore-lint`:

 {{{#!hs
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 module Bug where

 import Data.Functor.Identity (Identity(..))
 import Data.Kind (Type)
 import GHC.Exts (Any)

 -----
 -- The important bits
 -----

 type instance Meth (x :: Identity a) = GenericMeth x
 instance SC Identity

 -------------------------------------------------------------------------------

 data family Sing :: forall k. k -> Type
 data instance Sing :: forall a. Identity a -> Type where
   SIdentity :: Sing x -> Sing ('Identity x)

 newtype Par1 p = Par1 p
 data instance Sing :: forall p. Par1 p -> Type where
   SPar1 :: Sing x -> Sing ('Par1 x)

 type family Rep1 (f :: Type -> Type) :: Type -> Type

 class PGeneric1 (f :: Type -> Type) where
   type From1 (z :: f a)      :: Rep1 f a
   type To1   (z :: Rep1 f a) :: f a

 class SGeneric1 (f :: Type -> Type) where
   sFrom1 :: forall (a :: Type) (z :: f a).      Sing z -> Sing (From1 z)
   sTo1   :: forall (a :: Type) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f
 a)

 type instance Rep1 Identity = Par1

 instance PGeneric1 Identity where
   type From1 ('Identity x) = 'Par1 x
   type To1   ('Par1 x)     = 'Identity x

 instance SGeneric1 Identity where
   sFrom1 (SIdentity x) = SPar1 x
   sTo1 (SPar1 x) = SIdentity x

 type family GenericMeth (x :: f a) :: f a where
   GenericMeth x = To1 (Meth (From1 x))

 type family Meth (x :: f a) :: f a

 class SC f where
   sMeth         :: forall a (x :: f a).
                    Sing x -> Sing (Meth x)
   default sMeth :: forall a (x :: f a).
                    ( SGeneric1 f, SC (Rep1 f)
                    , Meth x ~ GenericMeth x
                    )
                 => Sing x -> Sing (Meth x)
   sMeth sx = sTo1 (sMeth (sFrom1 sx))

   dummy :: f a -> ()
   dummy _ = ()

 type instance Meth (x :: Par1 p) = x
 instance SC Par1 where
   sMeth x = x
 }}}
 {{{
 $ /opt/ghc/8.6.1/bin/ghc -fforce-recomp Bug.hs -dcore-lint
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )
 *** Core Lint errors : in result of Simplifier ***
 <no location info>: warning:
     [in body of letrec with binders x_s1Nw :: Sing (From1 x_a1Jc)]
     Trans coercion mis-match: D:R:Rep1Identity[0] <a_a1Jb>_N ; Sym (Sym
 (D:R:Rep1Identity[0]) <a_a1Jb>_N)
       Rep1 Identity a_a1Jb
       Par1 a_a1Jb
       Rep1 Identity a_a1Jb
       Par1 a_a1Jb
 *** Offending Program ***

 <elided>

 $csMeth_a1J9 [Occ=LoopBreaker]
   :: forall a (x :: Identity a). Sing x -> Sing (Meth x)
 [LclId,
  Unf=Unf{Src=<vanilla>, TopLvl=True, Value=False, ConLike=False,
          WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 100 60}]
 $csMeth_a1J9
   = \ (@ a_a1Jb) (@ (x_a1Jc :: Identity a_a1Jb)) ->
       case heq_sel
              @ (Identity a_a1Jb)
              @ (Identity a_a1Jb)
              @ (Meth x_a1Jc)
              @ (GenericMeth x_a1Jc)
              (($d~_s1Nz @ a_a1Jb @ x_a1Jc)
               `cast` (((~)
                          <Identity a_a1Jb>_N
                          ((To1
                              <Identity>_N
                              <a_a1Jb>_N
                              (Coh (Sym (D:R:MethTYPEPar1px[0]
                                             <a_a1Jb>_N
                                             (Coh (Sym (Coh <From1
 x_a1Jc>_N
 (D:R:Rep1Identity[0] <a_a1Jb>_N)))
                                                  (D:R:Rep1Identity[0]
 <a_a1Jb>_N))))
                                   (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ;
 (Meth
 <*>_N
 (Sym (D:R:Rep1Identity[0]))
 <a_a1Jb>_N
 (Coh <From1 x_a1Jc>_N
 (D:R:Rep1Identity[0] <a_a1Jb>_N)))_N))_N ; (Sym (D:R:GenericMeth[0]
 <Identity>_N
 <a_a1Jb>_N
 <x_a1Jc>_N) ; Sym (D:R:MethTYPEIdentityax[0]
 <a_a1Jb>_N
 <x_a1Jc>_N)))
                          ((To1
                              <Identity>_N
                              <a_a1Jb>_N
                              (Coh (Sym (Coh (Sym (Coh <From1 x_a1Jc>_N
                                                       (D:R:Rep1Identity[0]
 <a_a1Jb>_N)))
                                             (D:R:Rep1Identity[0]
 <a_a1Jb>_N)))
                                   (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ;
 (Sym (D:R:MethTYPEPar1px[0]
 <a_a1Jb>_N
 (Coh (Sym (Coh <From1
 x_a1Jc>_N
 (D:R:Rep1Identity[0] <a_a1Jb>_N)))
 (D:R:Rep1Identity[0] <a_a1Jb>_N))) ; (Meth
 <*>_N
 (Sym (D:R:Rep1Identity[0]))
 <a_a1Jb>_N
 (Coh <From1
 x_a1Jc>_N
 (D:R:Rep1Identity[0] <a_a1Jb>_N)))_N)))_N ; Sym (D:R:GenericMeth[0]
 <Identity>_N
 <a_a1Jb>_N
 <x_a1Jc>_N)))_R ; N:~[0]
 <Identity
 a_a1Jb>_N <Meth
 x_a1Jc>_N <GenericMeth
 x_a1Jc>_N
                       :: (To1 (From1 x_a1Jc) ~ To1 (From1 x_a1Jc))
                          ~R# (Meth x_a1Jc ~~ GenericMeth x_a1Jc)))
       of co_a1Kd
       { __DEFAULT ->
       (\ (sx_aEZ :: Sing x_a1Jc) ->
          let {
            x_s1Nw :: Sing (From1 x_a1Jc)
            [LclId]
            x_s1Nw = $csFrom1_a1Jz @ a_a1Jb @ x_a1Jc sx_aEZ } in
          case x_s1Nw
               `cast` ((Sing
                          (D:R:Rep1Identity[0] <a_a1Jb>_N)
                          (Coh (Sym (Coh <From1 x_a1Jc>_N
                                         (D:R:Rep1Identity[0] <a_a1Jb>_N ;
 Sym (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N))))
                               (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)))_R ;
 (Nth:3
 (Inst (forall (x :: Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N).
 (Sing
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)
 (Sym (Coh <x>_N
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N))))_R
 ->_R (Sing
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)
 (Sym (D:R:MethTYPEPar1px[0]
 <a_a1Jb>_N
 <x>_N) ; (Meth
 <*>_N
 (Sym (D:R:Rep1Identity[0]))
 <a_a1Jb>_N
 (Sym (Coh <x>_N
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N))))_N))_R) (Coh <From1
 x_a1Jc>_N
 (Sym (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)))) ; ((Sing
 (D:R:Rep1Identity[0] <a_a1Jb>_N))_R ; D:R:SingPar10[0]
 <a_a1Jb>_N) (Sym (Coh <Meth
 (From1
 x_a1Jc)>_N
 (D:R:Rep1Identity[0] <a_a1Jb>_N))))
                       :: Sing (From1 x_a1Jc |> Sym (D:R:Rep1Identity[0])
 <a_a1Jb>_N)
                          ~R# R:SingPar1
                                a_a1Jb (Meth (From1 x_a1Jc) |>
 D:R:Rep1Identity[0] <a_a1Jb>_N))
          of
          { SPar1 @ x_a1JZ co_a1K0 x_a195 ->
          ($WSIdentity @ a_a1Jb @ x_a1JZ x_a195)
          `cast` ((Sing
                     <Identity a_a1Jb>_N
                     (Sym (D:R:To1IdentityaPar1[0] <a_a1Jb>_N <x_a1JZ>_N) ;
 (To1
 <Identity>_N
 <a_a1Jb>_N
 (Sym (Coh (Sym (Coh <'Par1
 x_a1JZ>_N
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)))
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N)) ; (Coh <'Par1
 x_a1JZ>_N
 (Sym (D:R:Rep1Identity[0]) <a_a1Jb>_N) ; (Sym co_a1K0 ; Coh <Meth
 (From1
 x_a1Jc)>_N
 (D:R:Rep1Identity[0] <a_a1Jb>_N)))))_N))_R
                  :: Sing ('Identity x_a1JZ) ~R# Sing (To1 (Meth (From1
 x_a1Jc))))
          })
       `cast` (<Sing x_a1Jc>_R
               ->_R (Sing
                       <Identity a_a1Jb>_N
                       (Sym (D:R:GenericMeth[0]
                                 <Identity>_N <a_a1Jb>_N <x_a1Jc>_N) ; Sym
 co_a1Kd))_R
               :: (Sing x_a1Jc -> Sing (To1 (Meth (From1 x_a1Jc))))
                  ~R# (Sing x_a1Jc -> Sing (Meth x_a1Jc)))
       }
 end Rec }
 }}}

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