[commit: ghc] wip/T15809: Comemnts only (9a902e8)
git at git.haskell.org
git at git.haskell.org
Fri Nov 16 16:54:23 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/T15809
Link : http://ghc.haskell.org/trac/ghc/changeset/9a902e8fbc9ae25996bfabf6849b7543f2f17236/ghc
>---------------------------------------------------------------
commit 9a902e8fbc9ae25996bfabf6849b7543f2f17236
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Wed Nov 7 11:40:50 2018 +0000
Comemnts only
>---------------------------------------------------------------
9a902e8fbc9ae25996bfabf6849b7543f2f17236
compiler/typecheck/TcTyClsDecls.hs | 74 +++++++++++++++++++++++---------------
1 file changed, 46 insertions(+), 28 deletions(-)
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 3f90c42..cefc9ca 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -637,37 +637,55 @@ generaliseTcTyCon tc
{- 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 ::
+Each forall'd type variable in a type or kind is one of
+
+ * Required: an argument must be provided at every call site
+
+ * Specified: the argument can be inferred at call sites, but
+ may be instantiated with visible type/kind application
+
+ * Inferred: the must be inferred at call sites; it
+ is unavailable for use with visible type/kind 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.
+
+Go read Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
+
+The question for this Note is this:
+ given a TyClDecl, how are its quantified type variables classified?
+Much of the debate is memorialized in #15743.
+
+Here is our design choice. When inferring the ordering of variables
+for a TyCl declaration (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
+ 2. Specified variables; in the left-to-right order in which
+ the user wrote them, modified by scopedSort (see below)
+ to put them in depdendency order.
+ 3. Required variables before a top-level ::
+ 4. All variables after a top-level ::
If this ordering does not make a valid telescope, we reject the definition.
+Example:
+ data SameKind :: k -> k -> *
+ data X a (b :: SameKind a b) (c :: k) d
+
+For X:
+ - a, b, c, d are Required; they are explicitly listed by the user
+ as the positional arguments of X
+ - k is Specified; it appears explicitly in a kind signature
+ - k2, the kind of d, is Inferred; it is not mentioned explicitly at all
+
+Putting variables in the order Inferred, Specified, Required gives us
+ Inferred: k2
+ Specified: k (a ::kb
+
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
More information about the ghc-commits
mailing list