[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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 In a class/data/type declaration we need to say precisely which
 type variables are Inferred/Specified/Required and, for the specified
 ones, which order they occur in.

 See `Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility]`
 in `TyCoRep`.  Reminder:
 * Required: explicitly-specified arguments to the type constructor, always
   appear in any user-written type.

 * Specified: variables mentioned lexically in the declaration,
   but not positionally.  Available for visible kind application.

 * Inferred: completely invisible in the declaration; always
   implicit and not available for visible kind application.

 The rules for top-level (non-associated) declarations. Running
 example:
 {{{
    data T (b :: (k2 :: k)) c (a :: k)
 }}}

 * Categorisation
   * Required: the positional arguments in the header (`a`, `b`, `c`)
   * Specified: all the variables mentioned in the declaration header,
     that are not Required (`k`, `k2`)
   * Inferred: all the others (the kind of `c`)

 * Order.  We need to specify the order in which the Specfied variables
   are quantified.  Here is the spec:
   * Specified variables are always quantified before Required ones.
     (We could revisit this.)
   * List the specified variables in the textual order in which
     they appear [`k2`, `k`]
   * Sort them into dependency order using ''ScopedSort'' (see below),
     giving [`k`, `k2`]
   * Finally quantify Inferred, then Specified, then Required. In the
     example we get
 {{{
 T :: forall {k1}. forall k k2. k2 -> k1 -> k -> Type
 }}}

 The ''ScopedSort'' algorithm works as follows
 * Do dependency analysis, so for each variable we know what other
   variables it depends on, transitively.  By "depends on" we mean
   after full kind inference, not just what is written in the
   source program.
 * Work left-to-right through the list, with a cursor.
 * If variable `v` at the cursor is depended on by any earlier
   variable `w`, move `v` immediately before the leftmost such `w`.
 The invariant is that the variables to the left of the cursor
 form a valid telescope.

 For associated types, use this running example:
 {{{
   class C (a :: k) where
     type T a (b :: k2)
 }}}
 The rules are elaborated a bit for an associated type like `T`
 * Required: the explicit positional arguments (here `a`, `b`)
 * Specified: any non-Required variable that is
   * mentioned (lexically) in the class header and transitively depended on
 by the Required
   variables (here `k`), listed left-to-right; followed by
   * any other variables mentioned in the type header (here `k2`), again
 listed left-right.
 * Inferred: all the others, as before.

 The Specified variables are sorted exactly as before.


 Relevant tickets
 * #14887 esp comment:10 (order of Inferred type variables)
 * #15592
 * #15591 comment:4ff

 (All following discussion with RAE Friday 12 Oct.)

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