Repository : ssh://darcs.haskell.org//srv/darcs/ghc On branch : ghc-kinds
http://hackage.haskell.org/trac/ghc/changeset/e78df68ab23905e5622ca6e095abef91fd7f4123 >--------------------------------------------------------------- commit e78df68ab23905e5622ca6e095abef91fd7f4123 Author: Julien Cretin <g...@ia0.eu> Date: Fri Sep 9 11:40:19 2011 +0200 comments, notes and todos (doesn't compile) >--------------------------------------------------------------- compiler/TODO | 62 +++++++++++++++++++++++++++++++------- compiler/typecheck/TcHsType.lhs | 31 +++++++++---------- compiler/types/TypeRep.lhs | 30 ++++++++++++++++-- 3 files changed, 91 insertions(+), 32 deletions(-) diff --git a/compiler/TODO b/compiler/TODO index e52fb9d..41514b1 100644 --- a/compiler/TODO +++ b/compiler/TODO @@ -1,5 +1,55 @@ ## TODO FIRST +* tcTyClGroup + kind check to find out generalized_env + type check (kind check and desugar) using generalized_env at once + forget about record selectors, and rebuild them when needed (only one place apparently) + +* kind substitution in types, substTyVarBndr + look at CoreSubst, substIdBndr + no_kind_change : verify that kind is closed + +* UserKiVar (in Parser mkHsForAll or renamer) + look at kind annotation to know if a UserTyvar is a kind variable + (UserKiVar) or a type variable (UserTyVar) + forall k f (a :: k). f a -> Int + HsForAll Explicit [UserKiVar k, UserTyVar f, KindedTyVar a k] ... + +* ds_type takes a flag + - either it does defaulting: alpha -> star + - or it zonks to a kind variable: alpha -> k7 + When we kind generalize, we gather the free kind variables and quantify over them. + + +## TODO after merge with no-pred-ty + +* Get rid of (~), make it polymorphic and behave like any other TyCon. + + +## TODO NEXT + +* Promotion of DataCon (and associated AlgTyCon) + In DataCon: + Add field dcPromoted :: Maybe TyCon + A DataCon is promotable if: + - dcVanilla == True + - isPromotableType dataConUserType + - all its siblings are promotable (Just tc) + In AlgTyCon: + Add field algTcPromoted :: Maybe Int + where the Int is the number of kind arguments it takes + A TyCon is promotable if: + - it's kind is promotable * -> * ... -> * + - all its DataCon are promotable + +* Renaming in TcHsType + scDs -> tc + tcHsKindedType -> dsHsKindedType + Explain that: + kc = kind check + ds = desugar + tc = kc + ds + * write a testsuite named kinds with everything I can think of - translate Faking it (Conor) - when translating, add a reference to the thing being translated @@ -9,20 +59,8 @@ describe informally how we can use them -## TODO NEXT - - ## BUGS -* Do some sharing for promoted things, so that when I lookup K in a - type, I verify only once that it is promotable, and I don't build - several identical PromotedDataTyCon. - Add field about promotion: - - in DataCon: Maybe TyCon (the promoted TyCon) - - in AlgTyCon: Maybe Int which means - - T's kind is promotable (Just n) *^n -> * - - all its DataCon are promotable - * Error messages for things like: data T a = K (a K) diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs index d7c98c8..1ba8399 100644 --- a/compiler/typecheck/TcHsType.lhs +++ b/compiler/typecheck/TcHsType.lhs @@ -16,7 +16,7 @@ module TcHsType ( kindGeneralizeKind, -- Sort checking - tcLHsKind, tcLHsMaybeKind, + scDsLHsKind, scDsLHsMaybeKind, -- Typechecking kinded types tcHsKindedContext, tcHsKindedType, tcHsBangType, @@ -541,8 +541,7 @@ kcTyVar name = do -- Could be a tyvar, a tycon, or a datacon ATyVar _ ty -> wrap_mono (typeKind ty) AThing kind -> wrap_mono kind AGlobal (ATyCon tc) -> wrap_poly (tyConKind tc) - AGlobal (ADataCon dc) | Just tc <- promotedDataConTyCon_maybe dc - -> wrap_poly (tyConKind tc) + AGlobal (ADataCon dc) -> kcDataCon dc >>= wrap_poly _ -> wrongThingErr "type" thing name where wrap_mono kind = return (HsTyVar name, kind) @@ -554,8 +553,7 @@ kcTyVar name = do -- Could be a tyvar, a tycon, or a datacon return (HsWrapTy (WpKiApps kvs') (HsTyVar name), ki) where (kvs, ki_body) = splitForAllTys kind -DataCon.promotedDataConTyCon :: DataCon -> Maybe TyCon - +-- IA0_TODO: this function should disapear, and use the dcPromoted field of DataCon kcDataCon :: DataCon -> TcM TcKind kcDataCon dc = do let ty = dataConUserType dc @@ -756,18 +754,19 @@ typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty) %* * %************************************************************************ -\begin{code} -Note [Kind-checking kind-polymorphic types] Julien fix +Note [Kind-checking kind-polymorphic types] IA0_TODO ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider f :: forall k (a::k). a -> a -or (bogus) g :: forall k (a::k). a -> k -or (ok) h :: forall k a. a -> k - -When we encounter the 'forall k' we don't yet know whether 'k' will -turn out to be a kind variable or a type variable. No matter. We -just allocate a fresh meta-variable (kk) for the kind of k, and unify -away. -\end{code} +Consider: + f :: forall k f (a::k). f a -> Int + +The renamer (or parser) already decided for us if k, f or a are type +or kind variables. It did so by clissifying them with the correct data +constructor. + + UserTyVar -> type variable without kind annotation + KindedTyVar -> type variable with kind annotation + UserKiVar -> kind variable (they don't need annotation, + since we only have BOX for a super kind) \begin{code} kcHsTyVars :: [LHsTyVarBndr Name] diff --git a/compiler/types/TypeRep.lhs b/compiler/types/TypeRep.lhs index 7311031..667ed46 100644 --- a/compiler/types/TypeRep.lhs +++ b/compiler/types/TypeRep.lhs @@ -13,7 +13,7 @@ module TypeRep ( Type(..), Pred(..), -- to friends - Kind, SuperKind, + KindOrType, Kind, SuperKind, PredType, ThetaType, -- Synonyms -- Functions over types @@ -162,9 +162,7 @@ data Type deriving (Data.Data, Data.Typeable) -type KindOrType = Type -- See note [Arguments to type constructors] - -- *** Julien write this! - -- NB: only for TyConApp; not AppTy +type KindOrType = Type -- See Note [Arguments to type constructors] -- | The key type representing kinds in the compiler. -- Invariant: a kind is always in one of these forms: @@ -182,6 +180,30 @@ type Kind = Type type SuperKind = Type \end{code} + +Note [Arguments to type constructors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Because of kind polymorphism, in addition to type application we now +have kind instantiation. We reuse the same notations to do so. + +For example: + + Just (* -> *) Maybe + Right * Nat Zero + +are represented by: + + TyConApp (PromotedDataCon Just) [* -> *, Maybe] + TyConApp (PromotedDataCon Right) [*, Nat, (PromotedDataCon Zero)] + +Important note: Nat is used as a *kind* and not as a type. This can be +confusing, since type-level Nat and kind-level Nat are identical. We +use the kind of (PromotedDataCon Right) to know if its arguments are +kinds or types. + +This kind instantiation only happens in TyConApp currently. + + Note [Equality-constrained types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The type forall ab. (a ~ [b]) => blah _______________________________________________ Cvs-ghc mailing list Cvs-ghc@haskell.org http://www.haskell.org/mailman/listinfo/cvs-ghc
