[GHC] #15497: Coercion Quantification
#15497: Coercion Quantification -------------------------------------+------------------------------------- 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: Differential Rev(s): | Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2 -------------------------------------+------------------------------------- As described in [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2]. We would like to have coercion quantifications back in Haskell Core language. This means in Core we can define types like {{{#!hs \/ (a: k1) . \/ (co : k1 ~ k2) -- an explicit quantification for the coercion -> (a |> co) -- use the name for an explicit cast -> ... }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) 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: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Changes (by simonpj): * differential: => Phab:D5054 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) 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: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"ea5ade34788f29f5902c5475e94fbac13110eea5/ghc" ea5ade34/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="ea5ade34788f29f5902c5475e94fbac13110eea5" Coercion Quantification This patch corresponds to #15497. According to https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2, we would like to have coercion quantifications back. This will allow us to migrate (~#) to be homogeneous, instead of its current heterogeneous definition. This patch is (lots of) plumbing only. There should be no user-visible effects. An overview of changes: - Both `ForAllTy` and `ForAllCo` can quantify over coercion variables, but only in *Core*. All relevant functions are updated accordingly. - Small changes that should be irrelevant to the main task: 1. removed dead code `mkTransAppCo` in Coercion 2. removed out-dated Note Computing a coercion kind and roles in Coercion 3. Added `Eq4` in Note Respecting definitional equality in TyCoRep, and updated `mkCastTy` accordingly. 4. Various updates and corrections of notes and typos. - Haddock submodule needs to be changed too. Acknowledgments: This work was completed mostly during Ningning Xie's Google Summer of Code, sponsored by Google. It was advised by Richard Eisenberg, supported by NSF grant 1704041. Test Plan: ./validate Reviewers: goldfire, simonpj, bgamari, hvr, erikd, simonmar Subscribers: RyanGlScott, monoidal, rwbarton, carter GHC Trac Issues: #15497 Differential Revision: https://phabricator.haskell.org/D5054 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- 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: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Changes (by ningning): * owner: (none) => ningning -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- 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: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Changes (by ningning): * status: new => closed * resolution: => fixed -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) 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: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Changes (by simonpj): * owner: ningning => (none) * status: closed => new * resolution: fixed => Comment: I came across `Note [Emitting the residual implication in simplifyInfer]` in `TcSimplify`. It says “We can't form types like (forall co. blah), so we can't generalise over the coercion variable, …” But when you commit coercion quantification, we ''can'' quantify over coercions in types. So it is possible that this bit of cruft could be tidied up, with a significant simplification. I'll re-open the ticket to keep this idea on the radar. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeInType -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by ningning): I have looked through TcSimplify and 14584, but I am unsure I have understood fully the details. The logic seems delicate there. I know the motivation is {{{ forall x[2]. [W] co1: alpaha[1] ~ ty |> co2 [W] co2: k1 ~ * }}} where we have the scope problem cause `co2` could mention `x` and `co1` depends on `co2`. What's the goal after we have coercion quantifications comparing to the current strategy?? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => fixed Comment: comment:5 really seems to be asking for #15710. Closing this ticket in favor of that one. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by simonpj): On coercion quantification, I think it would be helpful to update [wiki:DependentHaskell/Phase2] * Under "Why homogeneous equality is good" explain how homogeneous equality can help the simplifier (in `exprIsConApp_maybe`). * On the same page, under "A small wrinkle: we need coercion quantification back", remove or rephrase the stuff about `(~~)`; perhaps use the ''data type'' `:~~:` rather than the ''class'' `(~~)`. * Promote "Another approach" for the class `(~~)` which appears lower down. It may be another approach but it is Our Plan for solving a Real Problem in introducing homogeneous equality at the moment, and as time goes on it is really helpful to know what The Plan is, with other approaches being discussed later. TL;DR: make the page reflect our current thinking as directly as possible. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by simonpj): One other thing. As I said in our call today, it's striking how narrow are the use-cases for a coercion-quantified type: * We can't ''declare'' a function with type `f :: (t1 ~# t2) => blah`, because currently `(t1 ~# t2)` is not a constraint (see Trac #15648) and is never implicitly instantiated. * We can't ''infer'' a function with type `f :: (t1 ~# t2) => blah`. And if we did, it wouldn't be instantiated implicitly. And so ''a fortiori'' we can't have coercion-quantified variants of such types. '''So the ''only'' functions that can have these coercion-quantified types are the workers of data constructors'''. Am I right? If so, can we say so explicitly on the wiki page? That seems like a lot of work for a narrow use-case! And yet, and yet... it's a very important case. Note also that we cannot write an exactly-equivalent type signature with GADT-syntax, because we don't have source-syntax of `t1 ~# t2`, let alone for `forall (co:t1~#t2). blah`. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by goldfire): I've done these wiki updates. Thanks for the concrete suggestions. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#15497: Coercion Quantification -------------------------------------+------------------------------------- Reporter: ningning | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: Resolution: fixed | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D5054 Wiki Page: | https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Phase2| -------------------------------------+------------------------------------- Comment (by Ningning Xie <xnningxie@…>): In [changeset:"3905c3c07ba2735e5b3d2dc3389272d5dbb1c503/ghc" 3905c3c/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="3905c3c07ba2735e5b3d2dc3389272d5dbb1c503" Update core-spec for Coercion Quantification Summary: Update details for `ForAllTy` and `ForAllCo` in core-spec, as they can now quantify over coercion variables. Test Plan: Please read core-spec.pdf Reviewers: goldfire, simonpj, bgamari Reviewed By: goldfire Subscribers: rwbarton, carter GHC Trac Issues: #15497, #15589 Differential Revision: https://phabricator.haskell.org/D5247 }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15497#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC