[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
#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
participants (1)
-
GHC