#13655: Spurious untouchable type variable in connection with rank-2 type and constraint family -------------------------------------+------------------------------------- Reporter: jeltsch | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1-rc2 checker) | Resolution: | Keywords: 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): I can see that it seems odd. Imagine that you wrote {{{ f :: (forall b . F a b => T b c) -> a f _ = undefined g :: (forall bb . F aa bb => T bb cc) -> aa g x = f x }}} You'd expect that to work: the two signatures are the same. But in the call in g's rhs we have: {{{ Expected type of f's arg: forall b. F a0 b => T b c0) Actual type of x (after instantation): T bb0 cc plus a "wanted" constraint: F aa bb0 }}} where the "0" things are unification variables. Of course this is easily soluble by unifying `bb0=b, a0=aa, c0=cc`. The `a0=aa` is enforced by the result type of the call to `(f x)` but the other two are not. And the "untouchable" bit is because we don't unify under a given equality constraint, or something that might be a given equality, like `(F a0 b)`. (Why: see the OutsideIn paper.) The ambiguity check, which is failing here, is precisely implementing this reasoning. In short: it's all behaving as designed. The error message is unhelpful, but it IS a subtle issue. I wish I could be more helpful. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13655#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler