[GHC] #15725: Core Lint error: Trans coercion mis-match
#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]
#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
Resolution: | 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: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
It appears that `simplCoercion` is the thing that's producing this ill-
formed coercion. Here is the input coercion:
{{{
Sym (Nth:2
(Inst (forall (x1 :: Sym (Bug.D:R:Rep1Identity[0]) <a>_N).
(Bug.Sing
(Sym (Bug.D:R:Rep1Identity[0]) <a>_N)
(GRefl nominal x1 (Sym (Bug.D:R:Rep1Identity[0])
<a>_N)))_R
->_R (Bug.Sing
(Sym (Bug.D:R:Rep1Identity[0]) <a>_N)
(Sym (Bug.D:R:MethTYPEPar1px[0] <a>_N <x1>_N) ;
(Bug.Meth
<*>_N
(Sym (Bug.D:R:Rep1Identity[0]))
<a>_N
(GRefl nominal x1
(Sym (Bug.D:R:Rep1Identity[0]) <a>_N)))_N))_R) (Sym (GRefl nominal
(Bug.From1
x)
(Sym (Sym (Bug.D:R:Rep1Identity[0]) <a>_N))))))
}}}
And here is the output coercion:
{{{
Nth:2
((Bug.Sing
(Bug.D:R:Rep1Identity[0] <a>_N)
(Sym (GRefl nominal (Bug.From1 x)
((Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym
(Bug.D:R:Rep1Identity[0]) <a>_N)) ; Sym (Bug.D:R:Rep1Identity[0])
<a>_N))))_R
->_R (Bug.Sing
(Bug.D:R:Rep1Identity[0] <a>_N)
((Bug.Meth
<*>_N
(Bug.D:R:Rep1Identity[0])
<a>_N
(Sym (GRefl nominal (Bug.From1 x)
((Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym
(Bug.D:R:Rep1Identity[0]) <a>_N)) ; Sym (Bug.D:R:Rep1Identity[0])
<a>_N))))_N ; Bug.D:R:MethTYPEPar1px[0]
<a>_N
(GRefl nominal (Bug.From1
x)
(Bug.D:R:Rep1Identity[0] <a>_N ; Sym (Sym (Bug.D:R:Rep1Identity[0])
<a>_N)))))_R)
}}}
I haven't dug deeper than that.
--
Ticket URL:
#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
Resolution: | 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: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
Some slightly more precise tracing reveals the following:
{{{
opt_co4_wrap }
Co: GRefl nominal x_X1Gk (Sym (D:R:Rep1Identity[0])
#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
Resolution: | 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: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
After much digging this morning, I've finally found my way out of this
rabbit hole. It turns out that the culprit is the
[http://git.haskell.org/ghc.git/blob/d728c3c578cc9e9205def2c1e96934487b364b7b...
InstCo] case of `opt_co4`:
{{{#!hs
-- See Note [Optimising InstCo]
opt_co4 env sym rep r (InstCo co1 arg)
-- forall over type...
| Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
= opt_co4_wrap (extendLiftingContext env tv
(mkCoherenceRightCo Nominal t2 (mkSymCo kind_co)
arg'))
-- kind_co :: k1 ~ k2
-- arg' :: (t1 :: k1) ~ (t2 :: k2)
-- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co))
:: k1)
sym rep r co_body
}}}
In particular, the bug lies within an optimization where `co1` is of the
form `forall (tv :: kind_co). co_body`, as explained in `Note [Optimising
InstCo]`. As explained in the comment, we need to extend the
`LiftingContext` such that `tv` maps to `(t1 :: k1) ~ (((t2 :: k2) |> (sym
kind_co)) :: k1)`, which we accomplish by way of `mkCoherenceRightCo`.
The
[http://git.haskell.org/ghc.git/blob/4eeeb51d5f51083d0ae393009a7fd246223e9791...
Haddocks] state that given `mkCoherenceRightCo r ty co co2`, the following
invariants must hold:
{{{
ty :: k1
co :: k1 ~ k2
co2 :: ty' ~ ty
}}}
That is, it must be the case that `typeKind ty ~ fst (coercionKind co)`
and `ty ~ snd (coercionKind co2)`.
Through some `pprTrace` sleuthing, I discovered that these were the things
being used to instantiate `ty`, `co`, and `co2`, respectively:
{{{
ty = t2 = (From1 Identity a x |> D:R:Rep1Identity[0] <a>_N)
:: Par1 a
co = mkSymCo kind_co = Sym (Sym (D:R:Rep1Identity[0]) <a>_N)
:: Rep1 Identity a ~ Par1 a
co2 = arg' = GRefl nominal (From1 Identity a x)
(D:R:Rep1Identity[0] <a>_N) :: From1 Identity a x ~ (From1 Identity a x |>
D:R:Rep1Identity[0] <a>_N)
}}}
This does uphold the invariant that `ty ~ snd (coercionKind co2)`, but it
does //not// uphold the invariant that `typeKind ty ~ fst (coercionKind
co)`, since:
* `typeKind ty ~ Par1 a`
* `fst (coercionKind co) ~ Rep1 Identity a`
My best guess as to why this happens is that `arg'` is computed
[http://git.haskell.org/ghc.git/blob/d728c3c578cc9e9205def2c1e96934487b364b7b:/compiler/types/OptCoercion.hs#l414
like so]:
{{{#!hs
arg' = opt_co4_wrap env sym False Nominal arg
}}}
In particular, we pass `opt_co4_wrap` the `sym` flag which, in the program
above, happens to be `True`, so an outer `Sym` is applied to the result of
the whole optimized coercion. `mkSymCo kind_co`, on the other hand, was
not the result of calling `opt_co4_wrap env sym` (since it comes from
`co1`, not `co1'`), which means that it does //not// have the same outer
`Sym` that `arg'` has. This causes a "polarity mismatch" between the two,
leading to disaster.
Here is one way to fix this issue:
{{{#!diff
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 8a44b86..c52e11e 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -377,7 +377,7 @@ opt_co4 env sym rep r (InstCo co1 arg)
-- forall over type...
| Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
= opt_co4_wrap (extendLiftingContext env tv
- (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co)
arg'))
+ (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co)
sym_arg'))
-- kind_co :: k1 ~ k2
-- arg' :: (t1 :: k1) ~ (t2 :: k2)
-- tv |-> (t1 :: k1) ~ (((t2 :: k2) |> (sym kind_co))
:: k1)
@@ -396,14 +396,14 @@ opt_co4 env sym rep r (InstCo co1 arg)
-- forall over type...
| Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
= opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
- (mkCoherenceRightCo Nominal t2 (mkSymCo kind_co')
arg'))
+ (mkCoherenceRightCo Nominal t2' (mkSymCo kind_co')
arg'))
False False r' co_body'
-- forall over coercion...
| Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
- , CoercionTy h1 <- t1
- , CoercionTy h2 <- t2
- = let new_co = mk_new_co cv' kind_co' h1 h2
+ , CoercionTy h1' <- t1'
+ , CoercionTy h2' <- t2'
+ = let new_co = mk_new_co cv' kind_co' h1' h2'
in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv'
new_co)
False False r' co_body'
@@ -412,7 +412,9 @@ opt_co4 env sym rep r (InstCo co1 arg)
co1' = opt_co4_wrap env sym rep r co1
r' = chooseRole rep r
arg' = opt_co4_wrap env sym False Nominal arg
- Pair t1 t2 = coercionKind arg'
+ sym_arg' = wrapSym sym arg'
+ Pair t1 t2 = coercionKind sym_arg'
+ Pair t1' t2' = coercionKind arg'
mk_new_co cv kind_co h1 h2
= let -- h1 :: (t1 ~ t2)
}}}
Essentially, we wrap `arg'` with another `Sym` to cancel out an extra
`Sym` that `opt_co4_wrap env sym` might provide. Of course, this should
only apply to the two cases where we inspect `co1` (which did not come
from `opt_co4_wrap`); for the two cases where we instead inspect `co1'`,
we continue to use plain old `arg'`.
Patch incoming.
--
Ticket URL:
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => patch * differential: => Phab:D5217 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15725#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Great sleuthing! Is the bug in [https://www.microsoft.com/en-us/research/publication /evidence-normalization-system-fc-2/ the paper], or just in the implementation? If the former we should fix the paper. I have not studied the details of your patch, but I'm sure Richard will. Thank you for doing this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15725#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:5 simonpj]:
Is the bug in [https://www.microsoft.com/en-us/research/publication /evidence-normalization-system-fc-2/ the paper], or just in the implementation?
I'm not sure. Having skimmed the paper, it looks like the code I changed roughly corresponds to the RedInstTy reduction rule from Figure 7 (when you have `InstCo (ForAllCo (a:eta). gamma) phi`). But the RedInstTy rule that is shown in the paper is much simpler than the thing that's actually implemented in GHC, since the paper doesn't distinguish between the cases where `a` is a type variable or coercion variable, nor does it include any details of the "lifting context" business from //System FC with Explicit Kind Equality//. So I can't really make any kind of judgment on whether //Evidence Normalisation in System FC// is correct or not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15725#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: | 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Comment (by monoidal): If this helps, I reduced to {{{ #!hs {-# LANGUAGE GADTs #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where import Data.Kind (Type) newtype Identity a = Identity a newtype Par1 a = Par1 a data family Sing :: forall k. k -> Type data instance Sing :: forall k. k -> Type type family Rep1 (f :: Type -> Type) :: Type -> Type type instance Rep1 Identity = Par1 type family From1 (z :: f a) :: Rep1 f a type instance From1 ('Identity x) = 'Par1 x und :: a und = und f :: forall (a :: Type) (x :: Identity a). Sing x f = g where g :: forall (a :: Type) (f :: Type -> Type) (x :: f a). Sing x g = seq (und :: Sing (From1 x)) und }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15725#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15725: Core Lint error: Trans coercion mis-match
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.6.1
Resolution: | 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): Phab:D5217
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
Thanks for your tireless efforts to minimize these bugs, monoidal. They're
very much appreciated.
In this particular example, I think you might have minimized it too well!
That's because that program trips up Core Lint even with the patch in
Phab:D5217. In fact, I think this program has an entirely different bug
from the one described in this ticket.
Here is the Core Lint error for your program:
{{{
*** Core Lint errors : in result of Simplifier ***
Bug.hs:25:1: warning:
[in body of lambda with binder x_a19R :: Identity a_a19Q]
Kind application error in
coercion ‘(Sing
(D:R:Rep1Identity[0]
#15725: Core Lint error: Trans coercion mis-match
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: patch
Priority: normal | Milestone: 8.8.1
Component: Compiler | Version: 8.6.1
Resolution: | 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): Phab:D5217
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Krzysztof Gogolewski
#15725: Core Lint error: Trans coercion mis-match -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.8.1 Component: Compiler | Version: 8.6.1 Resolution: fixed | 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): Phab:D5217 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: patch => closed * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15725#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC