[GHC] #15757: Coercion Variable Almost Devoid Checking in ForAllCo
#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: #15497 Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In [https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1074&context=com... Richard's thesis] Section 5.8.5.2, there is a restriction on where a coercion variable can appear in `ForAllCo` for the sake of consistency: the coercion variable can appear nowhere except in coherence coercions. Currently this restriction is missing in coercion quantification (see #15497). The goal of this ticket is to add the missing restriction. After discussion with Richard, we restate the restriction a little bit: the coercion variable can appear nowhere except in `GRefl` and `Refl`. Allowing it to appear in `Refl` should not break consistency. Notice that this also means `liftCoSubst` might fail when it lifts a `ForAllTy` over a coercion variable to a `ForAllCo`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15757> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15497 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by ningning): * owner: (none) => ningning -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15757#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15497 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Interesting. Before we are done with coercion quantification, it'd be good to update the core-spec.tex document to cover it; with some accompanying text to explain subtle points like this one. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15757#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15497 | Differential Rev(s): Phab:D5231 Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * differential: => Phab:D5231 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15757#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15497 | Differential Rev(s): Phab:D5231 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ningning Xie <xnningxie@…>): In [changeset:"879db5595208fb665ff1a0a2b12b9921d3efae0e/ghc" 879db559/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="879db5595208fb665ff1a0a2b12b9921d3efae0e" Adding almost devoid check for covar in ForAllCo Summary: For the sake of consistency of the dependent core, there is a restriction on where a coercion variable can appear in ForAllCo: the coercion variable can appear nowhere except in coherence coercions. Currently this restriction is missing in Core. The goal of this patch is to add the missing restriction. After discussion, we decide: coercion variables can appear nowhere except in `GRefl` and `Refl`. Relaxing the restriction to include `Refl` should not break consistency, we premuse. Test Plan: ./validate Reviewers: goldfire, simonpj, bgamari Reviewed By: goldfire Subscribers: rwbarton, carter GHC Trac Issues: #15757 Differential Revision: https://phabricator.haskell.org/D5231 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15757#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15757: Coercion Variable Almost Devoid Checking in ForAllCo -------------------------------------+------------------------------------- Reporter: ningning | Owner: ningning Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #15497 | Differential Rev(s): Phab:D5231 Wiki Page: | -------------------------------------+------------------------------------- Changes (by ningning): * status: new => closed * resolution: => fixed Comment: Updating core-spec is a good idea. Will do in the near future. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15757#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC