#14860: QuantifiedConstraints: Can't quantify constraint involving type family -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: wontfix | 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): This is tricky in an interesting way. What is the problem with quantified constraints with a type-function in the head? Consider {{{ f :: (forall a. C a => C (F a)) => ... }}} where `F` is a type family. We really, really can't handle this. Suppose we have {{{ type instance F [b] = (b,b) }}} and we are trying to solve `C (t,t)` in `f`'s RHS. Well that's the same as `C (F [t])` and lo, now the quantified constraint matches. It would be utterly different if we had {{{ f :: C (F a) => ... f = ...needs (C (F a))... }}} where the two constraints are patently equal; and it'd be equally fine if we had an enclosing constraint (from a GADT, say) telling us `a ~ [b]`. Then we'd rewrite both the "given" and the "wanted" to `C (F [b])`, and if that in turn rewrites to `C (b,b)` then both will so rewrite. It's all fine. The trouble in the earlier example comes because `F` is applied to a quantified variable. Here's another example it is, by comparison, fine: {{{ type family F2 a :: * -> * f2 :: (forall b. C b => C (F2 x b)) => blah }}} Notice that `F2` has arity 1. And notice that the saturated application `(F2 x)` does not mention the quantified variable `b`. So we could rewrite the signature thus: {{{ f2a :: (y ~ F2 x, forall b. C b => C (y b)) => blah }}} This is fine, and it is accepted today. By binding `F2 x` to `y` ''outside'' the quantification we have shown that the problems described above (about F) can't happen. Alas, `f2` is ''not'' accepted today. Until today I thought that once could always rewrite in the `f2a` style, and that it would be positively good to do so. That's what comment:1 says. But today you have shown me a counter example. I cannot apply that trick to {{{ class (forall b. Show b => Show (T a b)) => C a where type family T a :: * -> * }}} I might try {{{ class (y ~ T a, forall b. Show b => Show (y b)) => C a where type family T a :: * -> * }}} But now `y` is not bound in the class head, and we just don't allow that. (Why not? Because a class turns into a data type declaration {{{ data C a = MkC (..superclass1..) (..superclass2..) etc (..method1..) (..method2..) etc }}} so the superclass types can't mention variables not bound on the left. No we do not want existentials here.) So I am driven to the conclusion: * Perhaps we should allow type-family applications in the head of a quantified constraint, provided that the saturated application of the family does not mention any of the quantified variables. The flattener would have to work a bit harder. Richard, what do you think? Thanks for the example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14860#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler