[GHC] #14333: GHC doesn't use the fact that Coercible is symmetric
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 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: -------------------------------------+------------------------------------- {{{#!hs {-# Language ScopedTypeVariables, GADTs, DeriveGeneric #-} import GHC.Generics import Data.Type.Coercion data AB = A | B deriving (Generic) data XY = X | Y deriving (Generic) data This ab xy where At :: This AB XY foo :: This ab xy -> Coercion (Rep ab a) (Rep xy a) foo At = Coercion bar :: forall ab xy a. This ab xy -> Coercion (Rep ab a) (Rep xy a) bar at | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a) = Coercion }}} This compiles on 8.2.1 and 8.3.20170920 but flipping the arguments to `Coercion` fails {{{#!hs -- ... -- • Could not deduce: Coercible (Rep xy a) (Rep ab a) -- arising from a use of ‘Coercion’ -- from the context: Coercible (Rep ab a) (Rep xy a) -- bound by a pattern with constructor: bar :: forall ab xy a. This ab xy -> Coercion (Rep xy a) (Rep ab a) bar at | Coercion <- foo at :: Coercion (Rep ab a) (Rep xy a) = Coercion }}} Conceptually there should be an (`Undecidable`) superclass constraint for `Coercible` {{{#!hs class Coercible b a => Coercible a b }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * cc: RyanGlScott (added) * keywords: => TypeFamilies Comment: Indeed, something funny is going on here. Here's a simplified version of this program. Notice that this typechecks: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} import Data.Type.Coercion type family F a b :: * f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b) f Coercion = Coercion }}} However, if you change the kind of `F`: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} import Data.Type.Coercion type family F a :: * -> * f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b) f Coercion = Coercion }}} Then it no longer typechecks: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/ryanglscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:10:14: error: • Could not deduce: Coercible (F c d) (F a b) arising from a use of ‘Coercion’ from the context: Coercible (F a b) (F c d) bound by a pattern with constructor: Coercion :: forall k (a :: k) (b :: k). Coercible a b => Coercion a b, in an equation for ‘f’ at Bug.hs:10:3-10 NB: ‘F’ is a type function, and may not be injective • In the expression: Coercion In an equation for ‘f’: f Coercion = Coercion • Relevant bindings include f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b) (bound at Bug.hs:10:1) | 10 | f Coercion = Coercion | ^^^^^^^^ }}} Of course, it's quite easy to actually construct an implementation of `f` which does typecheck: {{{#!hs {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} import Data.Type.Coercion type family F a :: * -> * f :: Coercion (F a b) (F c d) -> Coercion (F c d) (F a b) f = sym }}} So the mystery is why GHC gets tripped up on this particular incarnation of `F`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): This is a good point. The problem is that `(a b) ~R# (c d)` tells you nothing at all about the relationship between any of the variables `a`, `b`, `c`, and `d`. This isn't a restriction in the solver, but simply a truism of representational equality. So when GHC knows `(a b) ~R# (c d)`, it is too stupid to figure out `(c d) ~R# (a b)`. I can thus boil down the problem even further: {{{#!hs bad :: Coercible (a b) (c d) => c d -> a b bad = coerce }}} will fail to type-check. (The version with argument & result swapped works fine.) Could the solver work around this? Maybe, with sufficient cleverness. (Unlike my concerns around recursive newtypes, I think this may be an engineering issue, not undecidability.) I don't think it would be easy though, requiring some kind of flattening logic akin to what GHC does for type families. Do you have a concrete use case? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: TypeFamilies => TypeFamilies, Roles -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:2 goldfire]:
Do you have a concrete use case?
My use case is [https://github.com/Icelandjack/deriving- via/blob/master/examples/Generics.hs this] where `swap` is required to express symmetry. I use this to witness a coercion between `Rep a x` and `Rep b x` {{{#!hs sameRep :: SameRep a b :- (Rep a x `Coercible` Rep b x) }}} but I also need {{{#!hs SameRep a b :- (Rep b x `Coercible` Rep a x) }}} for which I use `swap` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Could you include the full code of the concrete use case? I followed the link, but that's a non-trivial and not-self-contained file. GHC accepts {{{#!hs f :: Coercible b a => a x -> b x f = coerce }}} So, if `SameRep a b` implies `Coercible (Rep a) (Rep b)`, then the final implication above should hold. If, on the other hand, `SameRep a b` implies `forall x. Coercible (Rep a x) (Rep b x)`, then you're in trouble (at least with the current implementation). It occurs to me that you do not necessarily need to do anything clever with `a b ~R# c d`, but instead `F a b ~R# F c d`, where `F` has an arity of 1. Tackling the special case where we have a type function at the head, instead of any variable, might be easier than the general case. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * Attachment "SelfContained.hs" added. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I attached an example, I found another need for this: encoding that the opposite category is coercible to the current: {{{#!hs type Cat obj = obj -> obj -> Type class (forall xx yy. Coercible (cat xx yy) (Op cat yy xx)) => Category (cat :: Cat obj) where type Op cat :: Cat obj }}} The use case is similar as the other one but I can elaborate if needed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I found I could do this quite easily. (I happened to be in the area.) Patch coming. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Good news! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:7 simonpj]:
I found I could do this quite easily. (I happened to be in the area.) Patch coming.
Ooh. I'm curious. I'm not yet ready to backtrack from my opinion that this would be hard. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric
-------------------------------------+-------------------------------------
Reporter: Iceland_jack | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 8.2.1
Resolution: | Keywords: TypeFamilies,
| Roles
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
Ooh. I'm curious.
OK, take a look. Most of the patch is good regardless. If you disagree with the payload of the change (matching either way round) it'd be one- line change to take it out again. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14323 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: => #14323 Comment: Commit 5a66d574890ed09859ca912c9e0969dba72f4a23 fixed #14323 as well, so if the payload of that commit is reverted, make sure to re-open #14323 as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14323 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Your patch solves a smaller problem than I was thinking of... but now I can't seem to think of it again. Regardless, your patch looks correct to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14323, #15431 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * related: #14323 => #14323, #15431 Comment: Is this bug fixed? (Also, see #15431 for a possibly related issue.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14333: GHC doesn't use the fact that Coercible is symmetric -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: fixed | Keywords: TypeFamilies, | Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T14333 Blocked By: | Blocking: Related Tickets: #14323, #15431 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => typecheck/should_compile/T14333 * resolution: => fixed Comment: Yes I believe this is fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14333#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC