#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 aaronvargo): Replying to [comment:20 simonpj]:
Not allowing functions in the instance head not to do with ambiguity; it's to do with coherence
But is this an issue for QCs, which can't introduce incoherence? Does it matter if two QCs might overlap, as long as locally we can't tell that they do? Suppose we had: {{{#!hs type family F a = r | r -> a type family G a = r | r -> a foo :: forall b. (forall a. Eq (F a), forall a. Eq (G a)) => Dict (Eq (F b)) foo = Dict }}} While `F b` and `G b` might overlap for some particular `b`, locally only one instance can be used to solve `Eq (F b)`, since we don't know whether `G b ~ F b`. Since the two instances are guaranteed to be coherent, wouldn't it be fine to simply pick the one that matches? (If both were to match then the program would still be rejected). Likewise for the case with non-injective independent type families: {{{#!hs foo :: forall b. (forall t. C (F b) [t], forall t. C (G b) [t]) => Dict (C (F b) [Int]) }}} The first instance should just be used, since it's the only one that matches given the knowledge available locally. How does the compiler currently deal with type families in non-quantified constraints? What makes it more difficult to allow them in QCs?
Can you distil a small example that shows the utility of having a function in the head?
For now I have no use case for the injective type family case, and only really care about the independent family case. I'll try and come up with a simpler example than the category one.
So, maybe a quantified constraint with a function in the head is just "parked", but it wakes up if the function can be reduced.
This is much less useful than what I want, though I suppose it might help in some small minority of cases. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15347#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler