#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