#14694: Can't coerce given assumptions -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: 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 goldfire): * keywords: => Roles Comment: 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 to `a -> 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 be `AppTy`s (as plain old tyvars already have their own mechanism: `CTyEqCan`), and I believe just handling a top-level `AppTy` would be enough to make this approach complete. (I don't believe we'd ever need to look for a nested `AppTy` -- say, as the argument to a tycon -- because we'll decompose larger types until the `AppTy` bubbles up to the top.) We could just build a `TrieMap` mapping types to types; put a new entry in the `TrieMap` on given `AppTy` equalities and look up in the `TrieMap` 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14694#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14694: Can't coerce given assumptions -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: 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 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: {{{#!hs {-# 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`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14694#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14694: Incompleteness in the Coercible constraint solver -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Resolution: | Keywords: 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): 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14694#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler