Nail down the Required/Inferred/Specified story

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 (closed) esp #15743 (closed) (order of Inferred type variables)
• #15592 (closed)
• #15591 (closed) #15743ff

(All following discussion with RAE Friday 12 Oct.)

Trac metadata

Trac field	Value
Version	8.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture