compiler/hsSyn/HsTypes.hs¶
Note [HsBSig binder lists]¶
- Consider a binder (or pattern) decorated with a type or kind,
- (x :: a -> a). blah forall (a :: k -> *) (b :: k). blah
Then we use a LHsBndrSig on the binder, so that the renamer can decorate it with the variables bound by the pattern (‘a’ in the first example, ‘k’ in the second), assuming that neither of them is in scope already See also Note [Kind and type-variable binders] in RnTypes
Note [HsType binders]¶
The system for recording type and kind-variable binders in HsTypes is a bit complicated. Here’s how it works.
- In a HsType,
- HsForAllTy represents an /explicit, user-written/ ‘forall’
- e.g. forall a b. {…} or
forall a b -> {…}
- HsQualTy represents an /explicit, user-written/ context
e.g. (Eq a, Show a) => …
The context can be empty if that’s what the user wrote
These constructors represent what the user wrote, no more and no less.
The ForallVisFlag field of HsForAllTy represents whether a forall is invisible (e.g., forall a b. {…}, with a dot) or visible (e.g., forall a b -> {…}, with an arrow).
HsTyVarBndr describes a quantified type variable written by the user. For example
f :: forall a (b :: *). blah
here ‘a’ and ‘(b::*)’ are each a HsTyVarBndr. A HsForAllTy has a list of LHsTyVarBndrs.
HsImplicitBndrs is a wrapper that gives the implicitly-quantified kind and type variables of the wrapped thing. It is filled in by the renamer. For example, if the user writes
f :: a -> a
the HsImplicitBinders binds the ‘a’ (not a HsForAllTy!). NB: this implicit quantification is purely lexical: we bind any
type or kind variables that are not in scope. The type checker may subsequently quantify over further kind variables.
HsWildCardBndrs is a wrapper that binds the wildcard variables of the wrapped thing. It is filled in by the renamer
f :: _a -> _
The enclosing HsWildCardBndrs binds the wildcards _a and _.
The explicit presence of these wrappers specifies, in the HsSyn, exactly where implicit quantification is allowed, and where wildcards are allowed.
LHsQTyVars is used in data/class declarations, where the user gives explicit type variable bindings, but we need to implicitly bind kind variables. For example
class C (a :: k -> *) where …
The ‘k’ is implicitly bound in the hsq_tvs field of LHsQTyVars
Note [The wildcard story for types]¶
Types can have wildcards in them, to support partial type signatures, like f :: Int -> (_ , _a) -> _a
A wildcard in a type can be
- An anonymous wildcard,
written ‘_’
In HsType this is represented by HsWildCardTy. The renamer leaves it untouched, and it is later given fresh meta tyvars in the typechecker.
- A named wildcard,
written ‘_a’, ‘_foo’, etc
In HsType this is represented by (HsTyVar “_a”) i.e. a perfectly ordinary type variable that happens
to start with an underscore
Note carefully:
When NamedWildCards is off, type variables that start with an underscore really /are/ ordinary type variables. And indeed, even when NamedWildCards is on you can bind _a explicitly as an ordinary type variable:
data T _a _b = MkT _b _a
- Or even:
f :: forall _a. _a -> _b
Here _a is an ordinary forall’d binder, but (With NamedWildCards) _b is a named wildcard. (See the comments in #10982)
Named wildcards are bound by the HsWildCardBndrs construct, which wraps types that are allowed to have wildcards. Unnamed wildcards however are left unchanged until typechecking, where we give them fresh wild tyavrs and determine whether or not to emit hole constraints on each wildcard (we don’t if it’s a visible type/kind argument or a type family pattern). See related notes Note [Wildcards in visible kind application] and Note [Wildcards in visible type application] in TcHsType.hs
After type checking is done, we report what types the wildcards got unified with.
Note [Ordering of implicit variables]¶
Since the advent of -XTypeApplications, GHC makes promises about the ordering of implicit variable quantification. Specifically, we offer that implicitly quantified variables (such as those in const :: a -> b -> a, without a forall) will occur in left-to-right order of first occurrence. Here are a few examples:
const :: a -> b -> a -- forall a b. ...
f :: Eq a => b -> a -> a -- forall a b. ... contexts are included
type a <-< b = b -> a
g :: a <-< b -- forall a b. ... type synonyms matter
- class Functor f where
- fmap :: (a -> b) -> f a -> f b – forall f a b. … – The f is quantified by the class, so only a and b are considered in fmap
This simple story is complicated by the possibility of dependency: all variables must come after any variables mentioned in their kinds.
typeRep :: Typeable a => TypeRep (a :: k) -- forall k a. ...
The k comes first because a depends on k, even though the k appears later than the a in the code. Thus, GHC does a stable topological sort on the variables. By “stable”, we mean that any two variables who do not depend on each other preserve their existing left-to-right ordering.
Implicitly bound variables are collected by the extract- family of functions (extractHsTysRdrTyVars, extractHsTyVarBndrsKVs, etc.) in RnTypes. These functions thus promise to keep left-to-right ordering. Look for pointers to this note to see the places where the action happens.
Note that we also maintain this ordering in kind signatures. Even though there’s no visible kind application (yet), having implicit variables be quantified in left-to-right order in kind signatures is nice since:
- It’s consistent with the treatment for type signatures.
- It can affect how types are displayed with -fprint-explicit-kinds (see #15568 for an example), which is a situation where knowing the order in which implicit variables are quantified can be useful.
- In the event that visible kind application is implemented, the order in which we would expect implicit variables to be ordered in kinds will have already been established.
Note [Representing type signatures]¶
HsSigType is used to represent an explicit user type signature such as f :: a -> a
or g (x :: a -> a) = x
- A HsSigType is just a HsImplicitBndrs wrapping a LHsType.
- The HsImplicitBndrs binds the /implicitly/ quantified tyvars
- The LHsType binds the /explicitly/ quantified tyvars
- E.g. For a signature like
- f :: forall (a::k). blah
- we get
- HsIB { hsib_vars = [k]
- , hsib_body = HsForAllTy { hst_bndrs = [(a::*)]
- , hst_body = blah }
The implicit kind variable ‘k’ is bound by the HsIB; the explicitly forall’d tyvar ‘a’ is bound by the HsForAllTy
Note [HsForAllTy tyvar binders]¶
- After parsing:
- Implicit => empty Explicit => the variables the user wrote
- After renaming
- Implicit => the type variables free in the type Explicit => the variables the user wrote (renamed)
Qualified currently behaves exactly as Implicit, but it is deprecated to use it for implicit quantification. In this case, GHC 7.10 gives a warning; see Note [Context quantification] in RnTypes, and #4426. In GHC 8.0, Qualified will no longer bind variables and this will become an error.
- The kind variables bound in the hsq_implicit field come both
- from the kind signatures on the kind vars (eg k1)
- from the scope of the forall (eg k2)
Example: f :: forall (a::k1) b. T a (b::k2)
Note [Unit tuples]¶
- Consider the type
- type instance F Int = ()
- We want to parse that “()”
- as HsTupleTy HsBoxedOrConstraintTuple [],
NOT as HsTyVar unitTyCon
Why? Because F might have kind (* -> Constraint), so we when parsing we don’t know if that tuple is going to be a constraint tuple or an ordinary unit tuple. The HsTupleSort flag is specifically designed to deal with that, but it has to work for unit tuples too.
Note [Promotions (HsTyVar)]¶
- HsTyVar: A name in a type or kind.
- Here are the allowed namespaces for the name.
- In a type:
- Var: not allowed Data: promoted data constructor Tv: type variable TcCls before renamer: type constructor, class constructor, or promoted data constructor TcCls after renamer: type constructor or class constructor
- In a kind:
- Var, Data: not allowed Tv: kind variable TcCls: kind constructor or promoted type constructor
The 'Promoted' field in an HsTyVar captures whether the type was promoted in
the source code by prefixing an apostrophe.
Note [HsStarTy]¶
When the StarIsType extension is enabled, we want to treat ‘*’ and its Unicode variant identically to ‘Data.Kind.Type’. Unfortunately, doing so in the parser would mean that when we pretty-print it back, we don’t know whether the user wrote ‘*’ or ‘Type’, and lose the parse/ppr roundtrip property.
As a workaround, we parse ‘*’ as HsStarTy (if it stands for ‘Data.Kind.Type’) and then desugar it to ‘Data.Kind.Type’ in the typechecker (see tc_hs_type). When ‘*’ is a regular type operator (StarIsType is disabled), HsStarTy is not involved.
Note [Promoted lists and tuples]¶
- Notice the difference between
- HsListTy HsExplicitListTy HsTupleTy HsExplicitListTupleTy
E.g. f :: [Int] HsListTy
g3 :: T '[] All these use
g2 :: T '[True] HsExplicitListTy
g1 :: T '[True,False]
g1a :: T [True,False] (can omit ' where unambiguous)
kind of T :: [Bool] -> * This kind uses HsListTy!
- E.g. h :: (Int,Bool) HsTupleTy; f is a pair
- k :: S ‘(True,False) HsExplicitTypleTy; S is indexed by
- a type-level pair of booleans
kind of S :: (Bool,Bool) -> * This kind uses HsExplicitTupleTy
Note [Distinguishing tuple kinds]¶
Apart from promotion, tuples can have one of three different kinds:
x :: (Int, Bool) -- Regular boxed tuples
f :: Int# -> (# Int#, Int# #) -- Unboxed tuples
g :: (Eq a, Ord a) => a -- Constraint tuples
For convenience, internally we use a single constructor for all of these, namely HsTupleTy, but keep track of the tuple kind (in the first argument to HsTupleTy, a HsTupleSort). We can tell if a tuple is unboxed while parsing, because of the #. However, with -XConstraintKinds we can only distinguish between constraint and boxed tuples during type checking, in general. Hence the four constructors of HsTupleSort:
HsUnboxedTuple -> Produced by the parser HsBoxedTuple -> Certainly a boxed tuple HsConstraintTuple -> Certainly a constraint tuple HsBoxedOrConstraintTuple -> Could be a boxed or a constraint
tuple. Produced by the parser only, disappears after type checking
Note [ConDeclField passs]¶
A ConDeclField contains a list of field occurrences: these always include the field label as the user wrote it. After the renamer, it will additionally contain the identity of the selector function in the second component.
Due to DuplicateRecordFields, the OccName of the selector function may have been mangled, which is why we keep the original field label separately. For example, when DuplicateRecordFields is enabled
data T = MkT { x :: Int }
gives
ConDeclField { cd_fld_names = [L _ (FieldOcc "x" $sel:x:MkT)], ... }.
Note [Scoping of named wildcards]¶
- Consider
f :: _a -> _a f x = let g :: _a -> _a
g = …in …
Currently, for better or worse, the “_a” variables are all the same. So although there is no explicit forall, the “_a” scopes over the definition. I don’t know if this is a good idea, but there it is.
Note [Printing KindedTyVars]¶
#3830 reminded me that we should really only print the kind signature on a KindedTyVar if the kind signature was put there by the programmer. During kind inference GHC now adds a PostTcKind to UserTyVars, rather than converting to KindedTyVars as before.
(As it happens, the message in #3830 comes out a different way now, and the problem doesn’t show up; but having the flag on a KindedTyVar seems like the Right Thing anyway.)
Printing works more-or-less as for Types
