[GHC] #10651: Type checking issue with existential quantification, rank-n types and constraint kinds

[GHC]

#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