Opened 2 years ago
Last modified 2 years ago
#14694 new bug
Incompleteness in the Coercible constraint solver
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.2.2 |
Keywords: | Roles | Cc: | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
$ ghci -ignore-dot-ghci GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help Prelude> newtype WF f a = WF (f a) Prelude> import Data.Coerce Prelude Data.Coerce> :set -XFlexibleContexts Prelude Data.Coerce> :t coerce :: Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b) <interactive>:1:1: error: • Couldn't match representation of type ‘cat1 a1 b1’ with that of ‘a1 -> WF f1 b1’ arising from a use of ‘coerce’ • In the expression: coerce :: Coercible (cat a b) (a -> f b) => cat a b -> (a -> WF f b)
I'm not sure if I've filed this before or if it's even a bug.
But we know that Coercible (a -> f b) (a -> WF f b)
so why doesn't this work?
Change History (5)
comment:1 Changed 2 years ago by
Keywords: | Roles added |
---|
comment:2 Changed 2 years ago by
Just to be clear about what Richard means when he says "incompleteness", it's this: there is a solution, we don't find it.
Specifically we have
[G] (cat a b) ~R (a -> f b) [W] cat a b ~R (a -> WF f b)
Applying the [G]
transitively with the [W]
wanted, we'd get
[W] (a -> f b) ~R (a -> WF f b)
which we can certainly solve easily. It's annoying that GHC's solver can't spot this.
comment:3 Changed 2 years ago by
I don't remember a place where we collect them, we can make one & I can go through my old tickets in search for examples.
Here is another one maybe:
{-# Language FlexibleContexts #-} import Data.Coerce class Exp repr where int :: Int -> repr Int newtype Coerce f a = Coerce (f a) -- /tmp/Test.hs:13:9: error: -- • Couldn't match representation of type ‘f Int’ with that of ‘Int’ -- arising from a use of ‘coerce’ -- • In the expression: coerce -- In an equation for ‘int’: int = coerce -- In the instance declaration for ‘Exp (Coerce f)’ -- • Relevant bindings include -- int :: Int -> Coerce f Int (bound at /tmp/Test.hs:13:3) -- | -- 13 | int = coerce -- | ^^^^^^ instance Coercible Int (f Int) => Exp (Coerce f) where int = coerce
but it works with int = Coerce . coerce
.
comment:4 Changed 2 years ago by
Summary: | Can't coerce given assumptions → Incompleteness in the Coercible constraint solver |
---|
comment:5 Changed 2 years ago by
The list of tickets on https://ghc.haskell.org/trac/ghc/wiki/Roles is short enough that I don't think it's necessary to specifically catalog the incompletnesses. When/if someone comes along ready to fix all this, we can put it together.
This is yet another incompleteness in the solver. A given like
cat a b ~R (a -> f b)
cannot be decomposed, as the typing rules for roles forbids this. Currently, GHC remembers the given and uses it only if a wanted matches the given exactly. Thus, this ticket.One approach would be to have some structure that remembers
cat a b
maps toa -> f b
and then use this to look up types. Actually, this wouldn't even be all that hard: the left-hand sides would all beAppTy
s (as plain old tyvars already have their own mechanism:CTyEqCan
), and I believe just handling a top-levelAppTy
would be enough to make this approach complete. (I don't believe we'd ever need to look for a nestedAppTy
-- say, as the argument to a tycon -- because we'll decompose larger types until theAppTy
bubbles up to the top.) We could just build aTrieMap
mapping types to types; put a new entry in theTrieMap
on givenAppTy
equalities and look up in theTrieMap
on wanteds. Perhaps there's more to it than this, but I don't really think so.Iceland_jack, do you remember if there's a place where we collect representational incompletenesses? This is not the first.