compiler/iface/IfaceType.hs¶
Note [Free tyvars in IfaceType]¶
Nowadays (since Nov 16, 2016) we pretty-print a Type by converting to an IfaceType and pretty printing that. This eliminates a lot of pretty-print duplication, and it matches what we do with pretty- printing TyThings. See Note [Pretty printing via IfaceSyn] in PprTyThing.
It works fine for closed types, but when printing debug traces (e.g. when using -ddump-tc-trace) we print a lot of /open/ types. These types are full of TcTyVars, and it’s absolutely crucial to print them in their full glory, with their unique, TcTyVarDetails etc.
So we simply embed a TyVar in IfaceType with the IfaceFreeTyVar constructor. Note that:
- We never expect to serialise an IfaceFreeTyVar into an interface file, nor to deserialise one. IfaceFreeTyVar is used only in the “convert to IfaceType and then pretty-print” pipeline.
We do the same for covars, naturally.
Note [Equality predicates in IfaceType]¶
GHC has several varieties of type equality (see Note [The equality types story] in TysPrim for details). In an effort to avoid confusing users, we suppress the differences during pretty printing unless certain flags are enabled. Here is how each equality predicate* is printed in homogeneous and heterogeneous contexts, depending on which combination of the -fprint-explicit-kinds and -fprint-equality-relations flags is used:
|-------------------------------|—————————-|-----------------------------| | Predicate | -fprint-equality-relations | Both flags | |-------------------------------|—————————-|-----------------------------| | a ~ b (homogeneous) | a ~ b | (a :: Type) ~ (b :: Type) | | a ~~ b, homogeneously | a ~~ b | (a :: Type) ~~ (b :: Type) | | a ~~ b, heterogeneously | a ~~ c | (a :: Type) ~~ (c :: k) | | a ~# b, homogeneously | a ~# b | (a :: Type) ~# (b :: Type) | | a ~# b, heterogeneously | a ~# c | (a :: Type) ~# (c :: k) | | Coercible a b (homogeneous) | Coercible a b | Coercible @Type a b | | a ~R# b, homogeneously | a ~R# b | (a :: Type) ~R# (b :: Type) | | a ~R# b, heterogeneously | a ~R# b | (a :: Type) ~R# (c :: k) | ——————————————————————————————–
(* There is no heterogeneous, representational, lifted equality counterpart to (~~). There could be, but there seems to be no use for it.)
This table adheres to the following rules:
With -fprint-equality-relations, print the true equality relation.
- Without -fprint-equality-relations:
- If the equality is representational and homogeneous, use Coercible.
- Otherwise, if the equality is representational, use ~R#.
- If the equality is nominal and homogeneous, use ~.
- Otherwise, if the equality is nominal, use ~~.
With -fprint-explicit-kinds, print kinds on both sides of an infix operator, as above; or print the kind with Coercible.
Without -fprint-explicit-kinds, don’t print kinds.
A hetero-kinded equality is used homogeneously when it is applied to two identical kinds. Unfortunately, determining this from an IfaceType isn’t possible since we can’t see through type synonyms. Consequently, we need to record whether this particular application is homogeneous in IfaceTyConSort for the purposes of pretty-printing.
See Note [The equality types story] in TysPrim.
Note [Holes in IfaceCoercion]¶
When typechecking fails the typechecker will produce a HoleCo to stand in place of the unproven assertion. While we generally don’t want to let these unproven assertions leak into interface files, we still need to be able to pretty-print them as we use IfaceType’s pretty-printer to render Types. For this reason IfaceCoercion has a IfaceHoleCo constructor; however, we fails when asked to serialize to a IfaceHoleCo to ensure that they don’t end up in an interface file.
%************************************************************************ %* *
Functions over IFaceTypes
Note [Substitution on IfaceType]¶
Substitutions on IfaceType are done only during pretty-printing to construct the result type of a GADT, and does not deal with binders (eg IfaceForAll), so it doesn’t need fancy capture stuff.
Note [Suppressing invisible arguments]¶
We use the IfaceAppArgs data type to specify which of the arguments to a type should be displayed when pretty-printing, under the control of -fprint-explicit-kinds. See also Type.filterOutInvisibleTypes. For example, given
T :: forall k. (k->*) -> k -> * -- Ordinary kind polymorphism
'Just :: forall k. k -> 'Maybe k -- Promoted
we want
T * Tree Int prints as T Tree Int
'Just * prints as Just *
For type constructors (IfaceTyConApp), IfaceAppArgs is a quite natural fit, since the corresponding Core constructor:
data Type
= ...
| TyConApp TyCon [Type]
Already puts all of its arguments into a list. So when converting a Type to an IfaceType (see toIfaceAppArgsX in ToIface), we simply use the kind of the TyCon (which is cached) to guide the process of converting the argument Types into an IfaceAppArgs list.
We also want this behavior for IfaceAppTy, since given:
data Proxy (a :: k)
f :: forall (t :: forall a. a -> Type). Proxy Type (t Bool True)
We want to print the return type as Proxy (t True) without the use of -fprint-explicit-kinds (#15330). Accomplishing this is trickier than in the tycon case, because the corresponding Core constructor for IfaceAppTy:
data Type
= ...
| AppTy Type Type
Only stores one argument at a time. Therefore, when converting an AppTy to an IfaceAppTy (in toIfaceTypeX in ToIface), we:
- Flatten the chain of AppTys down as much as possible
- Use typeKind to determine the function Type’s kind
- Use this kind to guide the process of converting the argument Types into an IfaceAppArgs list.
By flattening the arguments like this, we obtain two benefits:
- We can reuse the same machinery to pretty-print IfaceTyConApp arguments as we do IfaceTyApp arguments, which means that we only need to implement the logic to filter out invisible arguments once.
- Unlike for tycons, finding the kind of a type in general (through typeKind) is not a constant-time operation, so by flattening the arguments first, we decrease the number of times we have to call typeKind.
Note [Pretty-printing invisible arguments]¶
Note [Suppressing invisible arguments] is all about how to avoid printing invisible arguments when the -fprint-explicit-kinds flag is disables. Well, what about when it’s enabled? Then we can and should print invisible kind arguments, and this Note explains how we do it.
As two running examples, consider the following code:
{-# LANGUAGE PolyKinds #-}
data T1 a
data T2 (a :: k)
When displaying these types (with -fprint-explicit-kinds on), we could just do the following:
T1 k a T2 k a
That certainly gets the job done. But it lacks a crucial piece of information: is the k argument inferred or specified? To communicate this, we use visible kind application syntax to distinguish the two cases:
T1 @{k} a
T2 @k a
Here, @{k} indicates that k is an inferred argument, and @k indicates that k is a specified argument. (See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep for a lengthier explanation on what “inferred” and “specified” mean.)
Note [Defaulting RuntimeRep variables]¶
RuntimeRep variables are considered by many (most?) users to be little more than syntactic noise. When the notion was introduced there was a signficant and understandable push-back from those with pedagogy in mind, which argued that RuntimeRep variables would throw a wrench into nearly any teach approach since they appear in even the lowly ($) function’s type,
($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
which is significantly less readable than its non RuntimeRep-polymorphic type of
($) :: (a -> b) -> a -> b
Moreover, unboxed types don’t appear all that often in run-of-the-mill Haskell programs, so it makes little sense to make all users pay this syntactic overhead.
For this reason it was decided that we would hide RuntimeRep variables for now (see #11549). We do this by defaulting all type variables of kind RuntimeRep to LiftedRep. This is done in a pass right before pretty-printing (defaultRuntimeRepVars, controlled by -fprint-explicit-runtime-reps)
This applies to /quantified/ variables like ‘w’ above. What about variables that are /free/ in the type being printed, which certainly happens in error messages. Suppose (#16074) we are reporting a mismatch between two skolems
(a :: RuntimeRep) ~ (b :: RuntimeRep)
We certainly don’t want to say “Can’t match LiftedRep ~ LiftedRep”!
- But if we are printing the type
- (forall (a :: Type r). blah
- we do want to turn that (free) r into LiftedRep, so it prints as
- (forall a. blah)
Conclusion: keep track of whether we we are in the kind of a binder; ohly if so, convert free RuntimeRep variables to LiftedRep.
Note [When to print foralls]¶
We opt to explicitly pretty-print `forall`s if any of the following criteria are met:
- -fprint-explicit-foralls is on.
- A bound type variable has a polymorphic kind. E.g.,
forall k (a::k). Proxy a -> Proxy a
Since a's kind mentions a variable k, we print the foralls.
- A bound type variable is a visible argument (#14238). Suppose we are printing the kind of:
T :: forall k -> k -> Type
The "forall k ->" notation means that this kind argument is required.
That is, it must be supplied at uses of T. E.g.,
f :: T (Type->Type) Monad -> Int
So we print an explicit “T :: forall k -> k -> Type”, because omitting it and printing “T :: k -> Type” would be utterly misleading.
See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep.
N.B. Until now (Aug 2018) we didn’t check anything for coercion variables.
Note [Printing foralls in type family instances]¶
We use the same criteria as in Note [When to print foralls] to determine whether a type family instance should be pretty-printed with an explicit forall. Example:
type family Foo (a :: k) :: k where
Foo Maybe = []
Foo (a :: Type) = Int
Foo a = a
Without -fprint-explicit-foralls enabled, this will be pretty-printed as:
- type family Foo (a :: k) :: k where
- Foo Maybe = [] Foo a = Int forall k (a :: k). Foo a = a
Note that only the third equation has an explicit forall, since it has a type variable with a non-Type kind. (If -fprint-explicit-foralls were enabled, then the second equation would be preceded with forall a..)
There is one tricky point in the implementation: what visibility do we give the type variables in a type family instance? Type family instances only store type variables, not type variable binders, and only the latter has visibility information. We opt to default the visibility of each of these type variables to Specified because users can’t ever instantiate these variables manually, so the choice of visibility is only relevant to pretty-printing. (This is why the k in forall k (a :: k). … above is printed the way it is, even though it wasn’t written explicitly in the original source code.)
We adopt the same strategy for data family instances. Example:
data family DF (a :: k)
data instance DF '[a, b] = DFList
That data family instance is pretty-printed as:
data instance forall j (a :: j) (b :: j). DF '[a, b] = DFList
This is despite that the representation tycon for this data instance (call it $DF:List) actually has different visibilities for its binders. However, the visibilities of these binders are utterly irrelevant to the programmer, who cares only about the specificity of variables in DF’s type, not $DF:List’s type. Therefore, we opt to pretty-print all variables in data family instances as Specified.
Note [Printing promoted type constructors]¶
- Consider this GHCi session (#14343)
> _ :: Proxy ‘[ ‘True ] error:
Found hole: _ :: Proxy ‘[‘True]
This would be bad, because the ‘[‘ looks like a character literal. Solution: in type-level lists and tuples, add a leading space if the first type is itself promoted. See pprSpaceIfPromotedTyCon.
