[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:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.1
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  dependent/should_fail/T15743[cd],
                                     |  dependent/should_compile/T15743{,e},
                                     |  ghci/scripts/T15743b
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by goldfire):

 * testcase:   =>
     dependent/should_fail/T15743[cd], dependent/should_compile/T15743{,e},
     ghci/scripts/T15743b
 * status:  new => closed
 * resolution:   => fixed


Comment:

 The design decisions are written in

 {{{
 {- Note [Required, Specified, and Inferred for types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We have some design choices in how we classify the tyvars bound
 in a type declaration. (Here, I use "type" to refer to any TyClDecl.)
 Much of the debate is memorialized in #15743. This Note documents
 the final conclusion.

 First, a reminder:
   * a Required argument is one that must be provided at every call site
   * a Specified argument is one that can be inferred at call sites, but
     may be instantiated with visible type application
   * an Inferred argument is one that must be inferred at call sites; it
     is unavailable for use with visible type application.

 Why have Inferred at all? Because we just can't make user-facing promises
 about the ordering of some variables. These might swizzle around even
 between
 minor released. By forbidding visible type application, we ensure users
 aren't caught unawares. See also
 Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.

 When inferring the ordering of variables (that is, for those
 variables that he user has not specified the order with an explicit
 `forall`)
 we use the following order:

  1. Inferred variables from an enclosing class (associated types only)
  2. Specified variables from an enclosing class (associated types only)
  3. Inferred variables not from an enclosing class
  4. Specified variables not from an enclosing class
  5. Required variables before a top-level ::
  6. All variables after a top-level ::

 If this ordering does not make a valid telescope, we reject the
 definition.

 This idea is implemented in the generalise function within kcTyClGroup
 (for
 declarations without CUSKs), and in kcLHsQTyVars (for declarations with
 CUSKs). Note that neither definition worries about point (6) above, as
 this
 is nicely handled by not mangling the res_kind. (Mangling res_kinds is
 done
 *after* all this stuff, in tcDataDefn's call to tcDataKindSig.) We can
 easily tell Inferred apart from Specified by looking at the scoped tyvars;
 Specified are always included there.

 One other small open question here: how to classify variables from an
 enclosing class? Here is an example:

   class C (a :: k) where
     type F a

 In the kind of F, should k be Inferred or Specified? Currently, we mark
 it as Specified, as we can commit to an ordering, based on the ordering
 of class variables in the enclosing class declaration. If k were not
 mentioned
 in the class head, then it would be Inferred. The alternative to this
 approach is to make the Inferred/Specified distinction locally, by just
 looking at the declaration for F. This lowers the availability of type
 application, but makes the reasoning more local. However, this alternative
 also disagrees with the treatment for methods, where all class variables
 are Specified, regardless of whether or not the variable is mentioned in
 the
 method type.

 A few points of motivation for the ordering above:

 * We put the class variables before the local variables in a nod to the
   treatment for class methods, where class variables (and the class
 constraint)
   come first. While this is an unforced design decision, it never rejects
   more declarations, as class variables can never depend on local
 variables.

 * We rigidly require the ordering above, even though we could be much more
   permissive. Relevant musings are at
   https://ghc.haskell.org/trac/ghc/ticket/15743#comment:7
   The bottom line conclusion is that, if the user wants a different
 ordering,
   then can specify it themselves, and it is better to be predictable and
 dumb
   than clever and capricious.

   I (Richard) conjecture we could be fully permissive, allowing all
 classes
   of variables to intermix. We would have to augment ScopedSort to refuse
 to
   reorder Required variables (or check that it wouldn't have). But this
 would
   allow more programs. See #15743 for examples. Interestingly, Idris seems
   to allow this intermixing. The intermixing would be fully specified, in
 that
   we can be sure that inference wouldn't change between versions. However,
   would users be able to predict it? That I cannot answer.

 Test cases (and tickets) relevant to these design decisions:
   T15591*
   T15592*
   T15743*

 -}
 }}}

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