[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=compsci_pubs/ 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
#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