#15347: QuantifiedConstraints: Implication constraints with type families don't work -------------------------------------+------------------------------------- Reporter: aaronvargo | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints 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): Consider this: {{{ type family F a type instance F Int = Bool instance Eq a => Eq (F a) where ... }}} Should we allow this? Obviously not. It's like allowing {{{ map f (xs ++ ys) = map f xs ++ map f ys map f [] = [] }}} where we have a function call in the pattern match. All manner of overlaps a chaos would result. So generally GHC does not allow type family calls in the head of an instance declaration. And I've made that same rule apply to quantified constraints, which are really just local instance declarations. But, you say, how are these two different? {{{ foo :: forall a b. (a => F b, a) => Dict (F b) qux :: forall a b c. (a => c, c ~ F b, a) => Dict (F b) }}} Very different, I say! Suppose that quantified constraint had looked like this {{ foo :: forall a b. (forall t. a => F t b, ...) => Dict (F b) }} Notice that the locally-quantified `t` is one of the arguments to `F`. Now, all the bad things could happen. What is different about your example is that '''the function call is independent of any of the forall'd variables of the quantified constraint'''. You expressed that by floating it out of the quantified constraint with you `c ~ F b`. And because it is independent of the forall'd variables, it is really constant so far as the instance is concerned, and doesn't lead to problems. Here's another variant: {{{ foo :: forall b. (forall t. C b t => C (F b) [t], ...) => Dict (F b) }}} Now the head of the quantified constraint does mention the forall'd `t`, but the call to `F` does not, so we can float thus: {{{ foo :: forall b c. (c ~ F b, forall t. C b t => C c [t], ...) => Dict (F b) }}} This directly expresses the fact that the first parameter to `C` in the head of the quantified constraint is independent of `t`. Now, you want this floating business to happen automatically, but I think it is much too complicated to do behind the scenes. If that's what you want, you can say it. I would be reluctant to introduce a significant (and unprecedented) implicit translation, based on a free-variable analysis, without plenty of evidence that it was going to have major benefit for a significant constituency. I don't think we are close to that point yet. But it ''is'' a nice observation that, by expressing the independence with an equality constraint, you can say just what you mean, and get just what you want. (I doubt that fundeps would be any help here.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler