#11282: Injectivity annotation fails in the presence of higher-rank use of constraint family -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.11 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Yes, this is unfortunate. Here's a bit more detail. The ambiguity check does a subsumption check {{{ forall a. (G a => F a) -> () <= forall b. (G b => F b) -> () }}} So we skolemise `b` and instantiate `b` to `beta`: {{{ forall a. ( (G a => F a) -> () <= (G beta => F beta) -> () ) }}} Now we do co/contravariance (see `Note [Co/contra-variance of subsumption checking]` in TcUnify) to get {{{ forall a. (G beta => F beta) <= (G a -> F a) }}} Now we skolemise and instantiate again (in this case there are no foralls, but we still get an implication constraint: {{{ forall a. (forall. G beta => (F a ~ F beta)) }}} Now as you point out beta is untouchable, and we can't float out the equality because `G beta` might have equalities in it. Alas. I'm not sure what to do about this. But that's what's happening. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11282#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler