#13295: Failure to resolve type parameter determined by type family -------------------------------------+------------------------------------- Reporter: alexvieth | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): It's not just that GHC doesn't do this kind of reasoning; it's also that system FC does not (yet, anyway) have a way to express the evidence. What you want to say is "for any type `t`, `F t` must be equal to `'D s` for some type `s`". But * If `F` has no instances that statement isn't true; `F t` isn't equal to any type other than `F t`. * Even if it does, we'd need an axiom of form {{{ forall t. F t ~ (exists s. 'D s) }}} and we have no such form. So I think this is well out of reach just at the moment. Not wrong; just out of reach. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13295#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler