[GHC] #15453: Bug in opt_trans_rule in OptCoercion
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- The ForAllCo case in the definition of opt_trans_rule in OptCoercion is not right: {{{#!hs push_trans tv1 eta1 r1 tv2 eta2 r2 = fireTransRule "EtaAllTy" co1 co2 $ mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2') where is' = is `extendInScopeSet` tv1 r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded! }}} Given {{{co1;co2}}}, where {{{#!hs co1 = \/ tv1 : eta1. r1 co2 = \/ tv2 : eta2. r2 }}} We would like optimize the transitivity coercion. I think what we want is {{{#!hs \/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1]) }}} Namely it should be {{{#!hs r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 }}} If there is any program that could hit the bug it would be better, as we can add it to test cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ningning): * owner: (none) => ningning -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ningning): * milestone: 8.6.1 => -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion
-------------------------------------+-------------------------------------
Reporter: ningning | Owner: ningning
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.4.3
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
I managed to construct program which throws a Core Lint error that (I
believe) is caused by this bug:
{{{#!hs
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where
import Data.Kind
import Data.Proxy
import Data.Type.Equality
type family S :: Type where
S = T
type family T :: Type where
T = Int
f :: (forall (x :: S). Proxy x) :~: (forall (x :: T). Proxy x)
f = Refl
g :: (forall (x :: T). Proxy x) :~: (forall (x :: Int). Proxy x)
g = Refl
h :: (forall (x :: S). Proxy x) :~: (forall (x :: Int). Proxy x)
h = f `trans` g
}}}
{{{
$ ~/Software/ghc4/inplace/bin/ghc-stage2 Bug.hs -dcore-lint -O1 -fforce-
recomp
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:25:1: warning:
[RHS of h :: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
:~: (forall (x :: Int). Proxy x)]
From-kind of Cast differs from kind of enclosed type
From-kind: T
Kind of enclosed type: S
Actual enclosed type: x_a1i3
Coercion used in cast: D:R:T[0]
*** Offending Program ***
f :: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))
:~: (forall (x :: T). Proxy (x |> D:R:T[0]))
[LclIdX,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}]
f = ($WRefl
@ * @ (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])))
`cast` (((:~:)
<*>_N
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by ningning): Replying to [comment:3 RyanGlScott]:
I managed to construct program which throws a Core Lint error that (I believe) is caused by this bug:
Thanks Ryan! Indeed this is a good example. I will add it to the test cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): D5018 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ningning): * differential: => D5018 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ningning): * differential: D5018 => Phab:D5018 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion
-------------------------------------+-------------------------------------
Reporter: ningning | Owner: ningning
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.4.3
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5018
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Krzysztof Gogolewski
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Changes (by monoidal): * status: new => merge -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Great work! We have a paper about `OptCoercion`, [https://www.microsoft.com/en- us/research/publication/evidence-normalization-system-fc-2/ Evidence normalisation in System FC]. It is a million times more comprehensible than `OptCoercion.hs` itself. If I found the sources, would anyone (Ryan?) be willing to * put (a version of) it in the GHC repo * update it to be correct, and to cover `GRefl` Thanks -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Great work indeed. Thanks Ningning! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ningning): Replying to [comment:9 simonpj]:
If I found the sources, would anyone (Ryan?) be willing to * put (a version of) it in the GHC repo * update it to be correct, and to cover `GRefl`
Also let me know if I could help with anything. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): If you (ningning) were willing to put (an updated version of) the paper in the GHC repo, that'd be great. If so I'll dig out the sources. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: merge Priority: normal | Milestone: Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ningning): Replying to [comment:12 simonpj]:
If you (ningning) were willing to put (an updated version of) the paper in the GHC repo, that'd be great. If so I'll dig out the sources.
Yes sure! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion
-------------------------------------+-------------------------------------
Reporter: ningning | Owner: ningning
Type: bug | Status: merge
Priority: normal | Milestone:
Component: Compiler | Version: 8.4.3
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s): Phab:D5018
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by simonpj):
OK done! Here is the original publication: [https://www.microsoft.com/en-
us/research/publication/evidence-normalization-system-fc-2/ Evidence
normalisation in System FC].
{{{
commit 3a065617b168813ec7e356ddd4eb25d125e9ff59
Author: Simon Peyton Jones
---------------------------------------------------------------
3a065617b168813ec7e356ddd4eb25d125e9ff59 docs/opt-coercion/Makefile | 9 + docs/{storage-mgt => opt-coercion}/code.sty | 2 + docs/opt-coercion/denot.sty | 120 + docs/opt-coercion/fc-normalization-rta.bib | 7157 +++++++++++++++++++++++++++ docs/opt-coercion/fc-normalization-rta.tex | 1627 ++++++ docs/opt-coercion/lipics.cls | 647 +++ docs/opt-coercion/prooftree.sty | 347 ++ 7 files changed, 9909 insertions(+) }}} Please edit away! Perhaps you can include a preamble saying "This is an updated version of the published paper. This version is intended to evolve to accurately reflect GHC". If you want use OTT, like `core-spec` then fine. But it may be easier just to work with the formatting as-is. A first step would be to include `GRefl` and anything else that isn't reflected in the paper. Thank you! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed * milestone: => 8.6.1 Comment: comment:7 merged to `ghc-8.6` with eb2b71c55df329570361e78f2f0ecdfcf3fe5974. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by ningning): Replying to [comment:14 simonpj]:
A first step would be to include `GRefl` and anything else that isn't reflected in the paper.
Questions: - In this paper, types and kinds are separated, coercions are between types, and they are homogeneous; while in GHC, types and kinds are merged, coercions can be between kinds. This is important because all GRefl is doing is casts between kinds. Do we want to merge types and kinds in the paper, make coercion heterogeneous and add kinds information? - Do we want to add roles? - If the answer is yes for both questions, I am actually wondering if it might be simpler to add coercion optimization rules in core-spec. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): That paper is from quite a while ago, before all these more recent innovations. I think adding the coercion optimization rules to the core- spec might indeed be the better route. I know Simon's on holiday for next stretch, so don't expect an answer from him soon. In the end, where the rules are isn't nearly as important as just having them written down somewhere. If you're happy adding to core-spec, go for it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15453: Bug in opt_trans_rule in OptCoercion -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5018 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm totally fine with adding the rules to core-spec. They are probably more likely to stay in sync if they are in the same document. But I hope that having the original paper and its Latex source will make the task significantly easier. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15453#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC