#9117: Coercible constraint solver misses one -------------------------------------+------------------------------------ Reporter: goldfire | Owner: nomeata Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): It strikes me that what we have here is a nice little programming- languages problem that would probably submit to standard techniques. Specifically, we have a specification of what things are coercible -- the typing rules for representational coercions -- and an algorithm for checking whether two things are coercible. The algorithm is straightforward and could be formalized beyond its Haskell implementation. Then, we could verify if the algorithm is sound and/or complete w.r.t. the specification. If it's not sound, we have the possibility of a Core Lint error. If it's not complete, we have the possibility of failing inappropriately. To be clear, I'm not quite volunteering to do this tonight or saying that it's an essential step, but it might be a nice thing to try if we want to understand this better. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9117#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler