[commit: ghc] wip/rae: Clean up comments around kind checking strategies. (a7bb93d)
git at git.haskell.org
git at git.haskell.org
Thu Aug 7 18:08:00 UTC 2014
Repository : ssh://git@git.haskell.org/ghc
On branch : wip/rae
Link : http://ghc.haskell.org/trac/ghc/changeset/a7bb93d00f8d3b6d07a361805d5d7596da459bbc/ghc
>---------------------------------------------------------------
commit a7bb93d00f8d3b6d07a361805d5d7596da459bbc
Author: Richard Eisenberg <eir at cis.upenn.edu>
Date: Thu Aug 7 08:40:21 2014 -0400
Clean up comments around kind checking strategies.
This is all *much* simpler than it was before! (#9200)
>---------------------------------------------------------------
a7bb93d00f8d3b6d07a361805d5d7596da459bbc
compiler/typecheck/TcHsType.lhs | 154 ++--------------------------------------
1 file changed, 5 insertions(+), 149 deletions(-)
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index fef1603..a8df9e5 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -905,155 +905,11 @@ addTypeCtxt (L _ ty) thing
Note [Kind-checking strategies]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There are three main declarations that we have to kind check carefully in the
-presence of -XPolyKinds: classes, datatypes, and data/type families. They each
-have a different kind-checking strategy (labeled in the parentheses above each
-section). This should potentially be cleaned up in the future, but this is how
-it stands now (June 2013).
-
-Classes (ParametricKinds):
- - kind-polymorphic by default
- - each un-annotated type variable is given a fresh meta kind variable
- - every explicit kind variable becomes a SigTv during inference
- - no generalisation is done while kind-checking the recursive group
-
- Taken together, this means that classes cannot participate in polymorphic
- recursion. Thus, the following is not definable:
-
- class Fugly (a :: k) where
- foo :: forall (b :: k -> *). Fugly b => b a
-
- But, because explicit kind variables are SigTvs, it is OK for the kind to
- be forced to be the same kind that is used in a separate declaration. See
- test case polykinds/T7020.hs.
-
-Datatypes:
- Here we have two cases, whether or not a Full Kind Signature is provided.
- A Full Kind Signature means that there is a top-level :: in the definition
- of the datatype. For example:
-
- data T1 :: k -> Bool -> * where ... -- YES
- data T2 (a :: k) :: Bool -> * where ... -- YES
- data T3 (a :: k) (b :: Bool) :: * where ... -- YES
- data T4 (a :: k) (b :: Bool) where ... -- NO
-
- Kind signatures are not allowed on datatypes declared in the H98 style,
- so those always have no Full Kind Signature.
-
- Full Kind Signature (FullKindSignature):
- - each un-annotated type variable defaults to *
- - every explicit kind variable becomes a skolem during type inference
- - these kind variables are generalised *before* kind-checking the group
-
- With these rules, polymorphic recursion is possible. This is essentially
- because of the generalisation step before kind-checking the group -- it
- gives the kind-checker enough flexibility to supply the right kind arguments
- to support polymorphic recursion.
-
- no Full Kind Signature (ParametricKinds):
- - kind-polymorphic by default
- - each un-annotated type variable is given a fresh meta kind variable
- - every explicit kind variable becomes a SigTv during inference
- - no generalisation is done while kind-checking the recursive group
-
- Thus, no polymorphic recursion in this case. See also Trac #6093 & #6049.
-
-Type families:
- Here we have three cases: open top-level families, closed top-level families,
- and open associated types. (There are no closed associated types, for good
- reason.)
-
- Open top-level families (FullKindSignature):
- - All open top-level families are considered to have a Full Kind Signature
- - All arguments and the result default to *
- - All kind variables are skolems
- - All kind variables are generalised before kind-checking the group
-
- This behaviour supports kind-indexed type and data families, because we
- need to have generalised before kind-checking for this to work. For example:
-
- type family F (a :: k)
- type instance F Int = Bool
- type instance F Maybe = Char
- type instance F (x :: * -> * -> *) = Double
-
- Closed top-level families (NonParametricKinds):
- - kind-monomorphic by default
- - each un-annotated type variable is given a fresh meta kind variable
- - every explicit kind variable becomes a skolem during inference
- - all such skolems are generalised before kind-checking; other kind
- variables are not generalised
- - all unconstrained meta kind variables are defaulted to * at the
- end of kind checking
-
- This behaviour is to allow kind inference to occur in closed families, but
- without becoming too polymorphic. For example:
-
- type family F a where
- F Int = Bool
- F Bool = Char
-
- We would want F to have kind * -> * from this definition, although something
- like k1 -> k2 would be perfectly sound. The reason we want this restriction is
- that it is better to have (F Maybe) be a kind error than simply stuck.
-
- The kind inference gives us also
-
- type family Not b where
- Not False = True
- Not True = False
-
- With an open family, the above would need kind annotations in its header.
-
- The tricky case is
-
- type family G a (b :: k) where
- G Int Int = False
- G Bool Maybe = True
-
- We want this to work. But, we also want (G Maybe Maybe) to be a kind error
- (in the first argument). So, we need to generalise the skolem "k" but not
- the meta kind variable associated with "a".
-
- Associated families (FullKindSignature):
- - Kind-monomorphic by default
- - Result kind defaults to *
- - Each type variable is either in the class header or not:
- - Type variables in the class header are given the kind inherited from
- the class header (and checked against an annotation, if any)
- - Un-annotated type variables default to *
- - Each kind variable mentioned in the class header becomes a SigTv during
- kind inference.
- - Each kind variable not mentioned in the class header becomes a skolem during
- kind inference.
- - Only the skolem kind variables are generalised before kind checking.
-
- Here are some examples:
-
- class Foo1 a b where
- type Bar1 (a :: k) (b :: k)
-
- The kind of Foo1 will be k -> k -> Constraint. Kind annotations on associated
- type declarations propagate to the header because the type variables in Bar1's
- declaration inherit the (meta) kinds of the class header.
-
- class Foo2 a where
- type Bar2 a
-
- The kind of Bar2 will be k -> *.
-
- class Foo3 a where
- type Bar3 a (b :: k)
- meth :: Bar3 a Maybe -> ()
-
- The kind of Bar3 will be k1 -> k2 -> *. This only kind-checks because the kind
- of b is generalised before kind-checking.
-
- class Foo4 a where
- type Bar4 a b
-
- Here, the kind of Bar4 will be k -> * -> *, because b is not mentioned in the
- class header, so it defaults to *.
+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 https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference#Proposednewstrategy
+and #9200 for lots of discussion of how we got here.
\begin{code}
data KindCheckingStrategy -- See Note [Kind-checking strategies]
More information about the ghc-commits
mailing list