Opened 14 months ago
Closed 14 months ago
#15431 closed bug (fixed)
Coercible and Existential types don't play nicely
Reported by: | NioBium | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | 8.6.1 |
Component: | Compiler | Version: | 8.4.3 |
Keywords: | Roles | Cc: | |
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: |
Description
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
Change History (5)
comment:1 Changed 14 months ago by
Keywords: | Roles added |
---|---|
Related Tickets: | → #14333 |
comment:2 Changed 14 months ago by
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.
comment:4 Changed 14 months ago by
Status: | new → merge |
---|
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.
comment:5 Changed 14 months ago by
Resolution: | → fixed |
---|---|
Status: | merge → closed |
Merged with 09abd1c420532c4274ddaeb5dfa54d7a9123d172.
Hm, this is interesting. This can be minimized to the following examples, which are slight variations of each other:
g1
typechecks, butg2
doesn't!I'm not sure if this is related to #14333 or not.