[GHC] #15431: Coercible and Existential types don't play nicely
#15431: Coercible and Existential types don't play nicely -------------------------------------+------------------------------------- Reporter: NioBium | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 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: -------------------------------------+------------------------------------- In the following example, {{{f}}} compiles but {{{g}}} doesn't. {{{ data T t where A :: Show (t a) => t a -> T t B :: Coercible Int (t a) => t a -> T t f :: T t -> String f (A t) = show t g :: T t -> Int g (B t) = coerce t • Couldn't match representation of type ‘Int’ with that of ‘t a’ Inaccessible code in a pattern with constructor: B :: forall k (t :: k -> *) (a :: k). Coercible Int (t a) => t a -> T t, in an equation for ‘g’ • In the pattern: B t In an equation for ‘g’: g (B t) = coerce t }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15431 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15431: Coercible and Existential types don't play nicely -------------------------------------+------------------------------------- Reporter: NioBium | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14333 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: => Roles * related: => #14333 Comment: Hm, this is interesting. This can be minimized to the following examples, which are slight variations of each other: {{{#!hs {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} module Bug where import Data.Coerce import Data.Functor.Identity g1 :: Coercible (t a) Int => t a -> Int g1 = coerce g2 :: Coercible Int (t a) => t a -> Int g2 = coerce }}} `g1` typechecks, but `g2` doesn't! {{{ $ /opt/ghc/8.4.3/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:12:6: error: • Couldn't match representation of type ‘t a’ with that of ‘Int’ arising from a use of ‘coerce’ • In the expression: coerce In an equation for ‘g2’: g2 = coerce • Relevant bindings include g2 :: t a -> Int (bound at Bug.hs:12:1) | 12 | g2 = coerce | ^^^^^^ }}} I'm not sure if this is related to #14333 or not. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15431#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15431: Coercible and Existential types don't play nicely -------------------------------------+------------------------------------- Reporter: NioBium | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14333 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I'm not all that surprised here. GHC has no way of decomposing `Coercible Int (t a)`, and so it just remembers that constraint in case it needs to prove exactly `Coercible Int (t a)`. In this case, it's trying to prove `Coercible (t a) Int`, and so it gives up. I suppose we special-case the lookup to include looking for a symmetrical constraint, but there will always be incompleteness lurking around the corner. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15431#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15431: Coercible and Existential types don't play nicely
-------------------------------------+-------------------------------------
Reporter: NioBium | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.4.3
Resolution: | Keywords: Roles
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: #14333 | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by Simon Peyton Jones
#15431: Coercible and Existential types don't play nicely -------------------------------------+------------------------------------- Reporter: NioBium | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14333 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => merge Comment: There was a palpable bug that meant the constraint was marked as insoluble, when it wasn't. This fixes both the OP and coment:1. The fix in #14333 (comment:10) does the symmetry bit. I agree that incompleteness is still lurking! The fix is a modest one; could be merged. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15431#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#15431: Coercible and Existential types don't play nicely -------------------------------------+------------------------------------- Reporter: NioBium | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.4.3 Resolution: fixed | Keywords: Roles Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14333 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * status: merge => closed * resolution: => fixed Comment: Merged with 09abd1c420532c4274ddaeb5dfa54d7a9123d172. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15431#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC