[GHC] #14694: Can't coerce given assumptions

[GHC]

#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