[commit: ghc] master: Improve comments about CUSKs (56b9e47)
git at git.haskell.org
git at git.haskell.org
Fri Jul 13 16:05:03 UTC 2018
Repository : ssh://git@git.haskell.org/ghc
On branch : master
Link : http://ghc.haskell.org/trac/ghc/changeset/56b9e47096393c7d8cedcde6d11b9203cba3a166/ghc
>---------------------------------------------------------------
commit 56b9e47096393c7d8cedcde6d11b9203cba3a166
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date: Fri Jul 13 10:25:38 2018 +0100
Improve comments about CUSKs
>---------------------------------------------------------------
56b9e47096393c7d8cedcde6d11b9203cba3a166
compiler/hsSyn/HsDecls.hs | 93 +++++++++++++++++++++++++++++++-----------
compiler/typecheck/TcHsType.hs | 4 +-
2 files changed, 72 insertions(+), 25 deletions(-)
diff --git a/compiler/hsSyn/HsDecls.hs b/compiler/hsSyn/HsDecls.hs
index ca8263b..07fa4e1 100644
--- a/compiler/hsSyn/HsDecls.hs
+++ b/compiler/hsSyn/HsDecls.hs
@@ -676,7 +676,7 @@ countTyClDecls decls
isNewTy _ = False
-- | Does this declaration have a complete, user-supplied kind signature?
--- See Note [Complete user-supplied kind signatures]
+-- See Note [CUSKs: complete user-supplied kind signatures]
hsDeclHasCusk :: TyClDecl GhcRn -> Bool
hsDeclHasCusk (FamDecl { tcdFam = fam_decl }) = famDeclHasCusk Nothing fam_decl
hsDeclHasCusk (SynDecl { tcdTyVars = tyvars, tcdRhs = rhs })
@@ -774,34 +774,80 @@ pprTyClDeclFlavour (DataDecl { tcdDataDefn = XHsDataDefn x })
pprTyClDeclFlavour (XTyClDecl x) = ppr x
-{- Note [Complete user-supplied kind signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [CUSKs: complete user-supplied kind signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We kind-check declarations differently if they have a complete, user-supplied
kind signature (CUSK). This is because we can safely generalise a CUSKed
declaration before checking all of the others, supporting polymorphic recursion.
See ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy
and #9200 for lots of discussion of how we got here.
-A declaration has a CUSK if we can know its complete kind without doing any
-inference, at all. Here are the rules:
-
- - A class or datatype is said to have a CUSK if and only if all of its type
-variables are annotated. Its result kind is, by construction, Constraint or *
-respectively.
-
- - A type synonym has a CUSK if and only if all of its type variables and its
-RHS are annotated with kinds.
-
- - A closed type family is said to have a CUSK if and only if all of its type
-variables and its return type are annotated.
-
- - An open type family always has a CUSK -- unannotated type variables (and
-return type) default to *.
-
- - A data definition with a top-level :: must explicitly bind all kind variables
-to the right of the ::. See test dependent/should_compile/KindLevels, which
-requires this case. (Naturally, any kind variable mentioned before the :: should
-not be bound after it.)
+PRINCIPLE:
+ a type declaration has a CUSK iff we could produce a separate kind signature
+ for it, just like a type signature for a function,
+ looking only at the header of the declaration.
+
+Examples:
+ * data T1 (a :: *->*) (b :: *) = ....
+ -- Has CUSK; equivalant to T1 :: (*->*) -> * -> *
+
+ * data T2 a b = ...
+ -- No CUSK; we do not want to guess T2 :: * -> * -> *
+ -- becuase the full decl might be data T a b = MkT (a b)
+
+ * data T3 (a :: k -> *) (b :: *) = ...
+ -- CUSK; equivalent to T3 :: (k -> *) -> * -> *
+ -- We lexically generalise over k to get
+ -- T3 :: forall k. (k -> *) -> * -> *
+ -- The generalisation is here is purely lexical, just like
+ -- f3 :: a -> a
+ -- means
+ -- f3 :: forall a. a -> a
+
+ * data T4 (a :: j k) = ...
+ -- CUSK; equivalent to T4 :: j k -> *
+ -- which we lexically generalise to T4 :: forall j k. j k -> *
+ -- and then, if PolyKinds is on, we further generalise to
+ -- T4 :: forall kk (j :: kk -> *) (k :: kk). j k -> *
+ -- Again this is exactly like what happens as the term level
+ -- when you write
+ -- f4 :: forall a b. a b -> Int
+
+NOTE THAT
+ * A CUSK does /not/ mean that everything about the kind signature is
+ fully specified by the user. Look at T4 and f4: we had do do kind
+ inference to figure out the kind-quantification. But in both cases
+ (T4 and f4) that inference is done looking /only/ at the header of T4
+ (or signature for f4), not at the definition thereof.
+
+ * The CUSK completely fixes the kind of the type constructor, forever.
+
+ * The precise rules, for each declaration form, for whethher a declaration
+ has a CUSK are given in the user manual section "Complete user-supplied
+ kind signatures and polymorphic recursion". BUt they simply implement
+ PRINCIPLE above.
+
+ * Open type families are interesting:
+ type family T5 a b :: *
+ There simply /is/ no accompanying declaration, so that info is all
+ we'll ever get. So we it has a CUSK by definition, and we default
+ any un-fixed kind variables to *.
+
+ * Associated types are a bit tricker:
+ class C6 a where
+ type family T6 a b :: *
+ op :: a Int -> Int
+ Here C6 does not have a CUSK (in fact we ultimately discover that
+ a :: * -> *). And hence neither does T6, the associated family,
+ because we can't fix its kind until we have settled C6. Another
+ way to say it: unlike a top-level, we /may/ discover more about
+ a's kind from C6's definition.
+
+ * A data definition with a top-level :: must explicitly bind all
+ kind variables to the right of the ::. See test
+ dependent/should_compile/KindLevels, which requires this
+ case. (Naturally, any kind variable mentioned before the :: should
+ not be bound after it.)
-}
@@ -1025,6 +1071,7 @@ data FamilyInfo pass
| ClosedTypeFamily (Maybe [LTyFamInstEqn pass])
-- | Does this family declaration have a complete, user-supplied kind signature?
+-- See Note [CUSKs: complete user-supplied kind signatures]
famDeclHasCusk :: Maybe Bool
-- ^ if associated, does the enclosing class have a CUSK?
-> FamilyDecl pass -> Bool
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 1b3ae90..3032e07 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1600,8 +1600,8 @@ tcWildCardBindersX new_wc maybe_skol_info wc_names thing_inside
-- user-supplied kind signature (CUSK), generalise the result.
-- Used in 'getInitialKind' (for tycon kinds and other kinds)
-- and in kind-checking (but not for tycon kinds, which are checked with
--- tcTyClDecls). See also Note [Complete user-supplied kind signatures] in
--- HsDecls.
+-- tcTyClDecls). See Note [CUSKs: complete user-supplied kind signatures]
+-- in HsDecls.
--
-- This function does not do telescope checking.
kcLHsQTyVars :: Name -- ^ of the thing being checked
More information about the ghc-commits
mailing list