[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):

 Here is the defining property of `Specified`:

 * All specified arguments have a predictable order. In other words, this
 order is stable regardless of what GHC's solver does.

 As long as we can uphold that property, then we're free to label variables
 as Specified.

 Furthermore, the place where we put Inferred variables is never important
 and needn't be specified.

 Accordingly, we can relax a few restrictions in Simon's description. I
 propose this algorithm instead:

 1. Perform kind inference, getting a fully-settled kind for each variable.
 This process may introduce new kind variables we would like to quantify
 over. The precise process is beyond the scope of this ticket.

 2. Put the variables in this order: first the newly-quantified variables
 never written by the user (the Inferred ones), in any order; then the
 Specified ones in order of first lexical occurrence, reading left-to-
 right; then the Required ones, in their left-to-right order.

 3. Sort all these variables according to ''ScopedSort''. If ''ScopedSort''
 tries to move one Required variable past another, fail.

 This new way of treating the variables relaxes two restrictions imposed
 above: that a Specified can never appear after a Required, and that an
 Inferred can never appear after a Specified. Here is an example:

 {{{
 data SimilarKind :: forall (c :: k) (d :: k). Proxy c -> Proxy d -> Type

 data T k (c :: k) (a :: Proxy c) b (x :: SimilarKind a b)
 }}}

 We will want to quantify over `b`'s kind (call it `Proxy d`), but that
 kind depends on the Required `k`. Simon's approach would reject (where? it
 doesn't say) because we put Inferred before Specified before Required. But
 my approach will infer

 {{{
 T :: forall (k :: Type) -> forall {d :: k}. forall (c :: k) (a :: Proxy c)
 (b :: Proxy d) -> SimilarKind a b -> Type
 }}}

 Note that `d` comes after `k`. This declaration is rejected today, whether
 or not we write down `b`'s kind explicitly.

 I had been loathe to allow such mixed quantification in the past, but now
 that the algorithm is written down (and can be included in the manual), I
 feel comfortable doing it.

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