[GHC] #15743: Nail down the Required/Inferred/Specified story

[GHC]

#15743: Nail down the Required/Inferred/Specified story
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      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 goldfire):

 Why?

 Consider

 {{{#!hs
 class C b where
   meth :: a -> b -> b
 }}}

 The full type for `meth` is `meth :: forall b. C b => forall a. a -> b ->
 b`. Note that `b` comes first, even though it is mentioned lexically
 second in the type of `meth`. I suppose we ''could'' pull the `a` all the
 way out to the front, but I think the current treatment is nice and
 predictable.

 What about

 {{{#!hs
 class C2 a b | a -> b where
   meth2 :: c -> a -> a
 }}}

 Using the same reasoning, we get `meth2 :: forall a b. C2 a b => forall c.
 c -> a -> a`. Note that `b` is Specified in the type of `meth2`.

 Returning to associated types (and the example from comment:12), we want
 associated types to behave somewhat like terms. Let's suppose we have
 Constrained Type Families, as I think that's the right model for all this.
 Then, we would get `T :: forall {k} (a :: k). C @k a => forall (f :: k ->
 Type). f a -> Type`. See now nicely that parallels the term-level
 treatment! Of course, we don't get the `C a` constraint these days, but
 that leaves us with `forall {k} (a :: k) (f :: k -> Type). f a -> Type`,
 as suggested by that Note.

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