[GHC] #15351: QuantifiedConstraints ignore FunctionalDependencies

[GHC]

#15351: QuantifiedConstraints ignore FunctionalDependencies
-------------------------------------+-------------------------------------
        Reporter:  aaronvargo        |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.5
  checker)                           |             Keywords:
      Resolution:                    |  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 goldfire):

 I've created #15354 about the documentation oversight -- you're absolutely
 right.

 I agree with your analysis in comment:4. By the constraint `forall a. C (f
 a) Int` (and the fundep), we know that any instance that begins with `C (f
 a)` ends with `Int`. Let's name different variables differently:

 {{{#!hs
 bar :: (forall b. C (f b) Int) => f a -> String
 bar = show . foo
 }}}

 So, since the usage of `foo` induces a `C (f a) alpha` constraint (for
 some unknown `alpha`) we can conclude that `alpha` must be `Int` by the
 fundep.

 Here is a related example, with the same `C`:

 {{{#!hs
 blah :: C Int Double => Int -> String
 blah = show . foo
 }}}

 This is accepted (even with no instances for `C`), because GHC can figure
 out that the result of `foo` must be `Double`. I don't see how quantified
 constraints should change that.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15351#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler