#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]