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 earliervariable
w
, movev
immediately before the leftmost suchw
.
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 |