[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 <forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])>_N (forall (x :: (D:R:S[0] ; D:R:T[0]) ; Sym (D:R:T[0])). <Proxy (x |> D:R:S[0] ; D:R:T[0])>_N))_R :: ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])) :~: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))) ~R# ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])) :~: (forall (x :: T). Proxy (x |> Sym ((D:R:S[0] ; D:R:T[0]) ; Sym (D:R:T[0])) ; (D:R:S[0] ; D:R:T[0]))))) g :: (forall (x :: T). Proxy (x |> D:R:T[0])) :~: (forall (x :: Int). Proxy x) [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)}] g = ($WRefl @ * @ (forall (x :: T). Proxy (x |> D:R:T[0]))) `cast` (((:~:) <*>_N <forall (x :: T). Proxy (x |> D:R:T[0])>_N (forall (x :: D:R:T[0]). <Proxy (x |> D:R:T[0])>_N))_R :: ((forall (x :: T). Proxy (x |> D:R:T[0])) :~: (forall (x :: T). Proxy (x |> D:R:T[0]))) ~R# ((forall (x :: T). Proxy (x |> D:R:T[0])) :~: (forall (x :: Int). Proxy x))) h :: (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])) :~: (forall (x :: Int). Proxy x) [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)}] h = ($WRefl @ * @ (forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0]))) `cast` (((:~:) <*>_N <forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])>_N (forall (x :: D:R:S[0] ; D:R:T[0]). <Proxy (x |> D:R:T[0])>_N))_R :: ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])) :~: (forall (x :: S). Proxy (x |> D:R:T[0]))) ~R# ((forall (x :: S). Proxy (x |> D:R:S[0] ; D:R:T[0])) :~: (forall (x :: Int). Proxy x))) <elided> }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15453#comment:3> 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 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 <krz.gogolewski@…>): In [changeset:"11de4380c2f16f374c6e8fbacf8dce00376e7efb/ghc" 11de438/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="11de4380c2f16f374c6e8fbacf8dce00376e7efb" Fix #15453: bug in ForAllCo case in opt_trans_rule Summary: Given ``` co1 = \/ tv1 : eta1. r1 co2 = \/ tv2 : eta2. r2 ``` We would like to optimize `co1; co2` so we push transitivity inside forall. It should be ``` \/tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1]) ``` It is implemented in the ForAllCo case in opt_trans_rule in OptCoercion. However current implementation is not right: ``` r2' = substCoWithUnchecked [tv2] [TyVarTy tv1] r2 -- ill-kinded! ``` This patch corrects it to be ``` r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2 ``` Test Plan: validate Reviewers: bgamari, goldfire, RyanGlScott Reviewed By: RyanGlScott Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15453 Differential Revision: https://phabricator.haskell.org/D5018 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15453#comment:7> 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: | -------------------------------------+------------------------------------- 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 <simonpj@microsoft.com> Date: Tue Jul 31 13:17:58 2018 +0100 Add the paper "Evidence normalisation in System FC" This is with a view to editing it to include new developments in the coercion infrastructure.
---------------------------------------------------------------
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