Core Lint error: Trans coercion mis-match
I discovered this when debugging #15703. The following code fails to compile with -dcore-lint:
{-# 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 }Trac metadata
| Trac field | Value |
|---|---|
| Version | 8.6.1 |
| Type | Bug |
| TypeOfFailure | OtherFailure |
| Priority | normal |
| Resolution | Unresolved |
| Component | Compiler |
| Test case | |
| Differential revisions | |
| BlockedBy | |
| Related | |
| Blocking | |
| CC | |
| Operating system | |
| Architecture |