[GHC] #8541: Coercible should be higher-kinded
#8541: Coercible should be higher-kinded ------------------------------------+------------------------------------- Reporter: nomeata | Owner: nomeata Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- Just discussed with SJP: The Coercible should be higher kinded, and it seems to be straight forward. Given {{{ data T f = T (f Int) newtype List a = [a] }}} we want to be able to derive {{{ Coercible (T (Either Int)) (T (Either Age)) Coercible (T List) (T []) }}} We now allow `Coercible` at a kind `* -> k`, with the following intuition: {{{ Coercible A B ⇐⇒ (forall a. Coercible (A a) (B a)) }}} Note that this is ok independent of the role of `A`’s parameter, as we are not modifying that parameter here. Allowing such constraints, we therefore, we need these constraints exist in theory (but are in fact generated on demand, so only those of the rind kindnessare visible to the constraint solver) for `Either` and `List`: {{{ instance (Coercible a b, Coercible c d) => Coercible (Either a c) (Either b d) -- old instance Coercible a b => Coercible (Either a) (Either b) -- new instance Coercible [a] b => Coercible (List a) b -- old instance Coercible b [a] => Coercible b (List a) -- old instance Coercible a b => Coercible (List a) (List b) -- old instance Coercible [] b => Coercible List b -- new instance Coercible b [] => Coercible b List -- new }}} This solves the cases above. It does not solve all cases, though. Consider {{{ newtype NT1 a = NT1 (a -> Int) newtype NT2 a = NT2 (a -> Int) }}} and we want to solve `Coercible (T NT1) (T NT2)`. Although, by the definition above, `Coercible NT1 NT2` should hold, such a coercion cannot be created (as far as I can see). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8541: Coercible should be higher-kinded -------------------------------------+------------------------------------ Reporter: nomeata | Owner: nomeata Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.6.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by nomeata): Indeed straight forward, see 8959c69104eb032b75ec94dcf9cda3edd2b46423 (ghc) and bbfaff2fa89b21bee058af7e6e6ddd66524524d0 (testsuite); currently on the branch wip/T8541 (I wonder why they were not auto-linked – is that only working for master?). The code did not check saturation of type constructors, so it worked out of the box for the positive examples from here. So let’s see what happens with the negative ones... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8541: Coercible should be higher-kinded -------------------------------------------------+------------------------- Reporter: nomeata | Owner: Type: task | nomeata Priority: normal | Status: patch Component: Compiler | Milestone: Resolution: | Version: 7.6.3 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: TcCoercible, | Unknown/Multiple TcCoercibleFail3 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by nomeata): * status: new => patch * testcase: => TcCoercible, TcCoercibleFail3 Comment: Added a few testcases and avoiding panics for `Coercible (T NT1) (T NT2)`. Please break (or review) my code! Fancy side-by-side-diffs: http://git.haskell.org/ghc.git/commitdiff/refs/heads/wip/T8541?hp=851548d8d1... http://git.haskell.org/testsuite.git/commitdiff/refs/heads/wip/T8541?hp=1862... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
currently on the branch wip/T8541 (I wonder why they were not auto-
#8541: Coercible should be higher-kinded -------------------------------------------------+------------------------- Reporter: nomeata | Owner: Type: task | nomeata Priority: normal | Status: patch Component: Compiler | Milestone: Resolution: | Version: 7.6.3 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: TcCoercible, | Unknown/Multiple TcCoercibleFail3 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (by hvr): Replying to [comment:1 nomeata]: linked – is that only working for master?). yes, it's to avoid having multiple redundant commits attached to the same ticket; so the commit will be linked to this ticket as soon as the commit becomes reachable from master for the first time. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8541: Coercible should be higher-kinded -------------------------------------------------+------------------------- Reporter: nomeata | Owner: Type: task | nomeata Priority: normal | Status: patch Component: Compiler | Milestone: Resolution: | Version: 7.6.3 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: TcCoercible, | Unknown/Multiple TcCoercibleFail3 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (by nomeata): Makes sense, given that `wip/`-branches can be rebased. Thanks for the clarification. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8541: Coercible should be higher-kinded -------------------------------------------------+------------------------- Reporter: nomeata | Owner: Type: task | nomeata Priority: normal | Status: patch Component: Compiler | Milestone: Resolution: | Version: 7.6.3 Operating System: Unknown/Multiple | Keywords: Type of failure: None/Unknown | Architecture: Test Case: TcCoercible, | Unknown/Multiple TcCoercibleFail3 | Difficulty: Blocking: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Comment (by goldfire): The changes certainly look sensible to me... -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8541: Coercible should be higher-kinded
-------------------------------------------------+-------------------------
Reporter: nomeata | Owner:
Type: task | nomeata
Priority: normal | Status: patch
Component: Compiler | Milestone:
Resolution: | Version: 7.6.3
Operating System: Unknown/Multiple | Keywords:
Type of failure: None/Unknown | Architecture:
Test Case: TcCoercible, | Unknown/Multiple
TcCoercibleFail3 | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Joachim Breitner
#8541: Coercible should be higher-kinded
-------------------------------------------------+-------------------------
Reporter: nomeata | Owner:
Type: task | nomeata
Priority: normal | Status: patch
Component: Compiler | Milestone:
Resolution: | Version: 7.6.3
Operating System: Unknown/Multiple | Keywords:
Type of failure: None/Unknown | Architecture:
Test Case: TcCoercible, | Unknown/Multiple
TcCoercibleFail3 | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Joachim Breitner
#8541: Coercible should be higher-kinded
-------------------------------------------------+-------------------------
Reporter: nomeata | Owner:
Type: task | nomeata
Priority: normal | Status: patch
Component: Compiler | Milestone:
Resolution: | Version: 7.6.3
Operating System: Unknown/Multiple | Keywords:
Type of failure: None/Unknown | Architecture:
Test Case: TcCoercible, | Unknown/Multiple
TcCoercibleFail3 | Difficulty:
Blocking: | Unknown
| Blocked By:
| Related Tickets:
-------------------------------------------------+-------------------------
Comment (by Joachim Breitner
#8541: Coercible should be higher-kinded -------------------------------------------------+------------------------- Reporter: nomeata | Owner: Type: task | nomeata Priority: normal | Status: Component: Compiler | closed Resolution: fixed | Milestone: Operating System: Unknown/Multiple | Version: 7.6.3 Type of failure: None/Unknown | Keywords: Test Case: TcCoercible, | Architecture: TcCoercibleFail3 | Unknown/Multiple Blocking: | Difficulty: | Unknown | Blocked By: | Related Tickets: -------------------------------------------------+------------------------- Changes (by nomeata): * status: patch => closed * resolution: => fixed Comment: This has hit master now. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8541#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC