#16365: Inconsistency in quantified constraint solving -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: | 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 RyanGlScott): I'm still not convinced. You say: Replying to [comment:3 simonpj]:
From superclass expansion we get {{{ [G] forall z. C (F a z) -- From superclass expansion [W] C (F a b) }}} And now we are stuck. What `z` would make `C (F a z)` match `C (F a b)`? Well, yes, `b` would, but maybe also lots of other things. GHC simply doesn't support matching involving type families.
I don't really see why `F` being a type family has anything to do with this. Recall the definition of `F`: {{{#!hs type family F a :: Type -> Type }}} Note that `F`'s second argument is //matchable//. This means that given an equality between `F`s, we can easily decompose it into their second type arguments, as demonstrated by the fact that this function typechecks: {{{#!hs f :: Proxy a -> F a b :~: F a c -> b :~: c f _ Refl = Refl }}} Now recall what things we are trying to solve: {{{ [G] forall z. C (F a z) -- From superclass expansion [W] C (F a b) }}} These two constraints only differ in their second argument. But as we just established above, `F` is matchable in its second argument. Therefore, GHC should have no trouble concluding that `z` equals `b`. In other words, `b` is the only sensible choice here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16365#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler