#10651: Type checking issue with existential quantification, rank-n types and constraint kinds -------------------------------------+------------------------------------- Reporter: Roboguy | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.1 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 Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): The error message is not great, but I think it's right. To show that the type of `constrMap_` is unambiguous, GHC needs to prove that {{{ (forall a. c a => a -> m b) ~ (forall a. c a => a -> m beta) }}} where `beta` is a unification variable. If GHC guessed (unified) `beta := b`, all would be well, but `beta` is "untouchable" underneath the constraint `c a`. Why? Because what if `c a` later got instantiate to `b ~ Int`; then `beta := Int` might be a valid substitution. In general, GHC doesn't unify underneath an equality, ''or'' something that might turn into an equality. See Section 5 in the [http://research.microsoft.com/~simonpj/papers/constraints/jfp- outsidein.pdf OutsideIn paper]. I don't know how to improve this. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10651#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler