compiler/typecheck/TcType.hs¶

Note [TcTyVars and TyVars in the typechecker]¶

The typechecker uses a lot of type variables with special properties, notably being a unification variable with a mutable reference. These use the ‘TcTyVar’ variant of Var.Var.

Note, though, that a /bound/ type variable can (and probably should) be a TyVar. E.g

forall a. a -> a

Here ‘a’ is really just a deBruijn-number; it certainly does not have a signficant TcLevel (as every TcTyVar does). So a forall-bound type variable should be TyVars; and hence a TyVar can appear free in a TcType.

The type checker and constraint solver can also encounter /free/ type variables that use the ‘TyVar’ variant of Var.Var, for a couple of reasons:

When typechecking a class decl, say

class C (a :: k) where

foo :: T a -> Int

We have first kind-check the header; fix k and (a:k) to be TyVars, bring ‘k’ and ‘a’ into scope, and kind check the signature for ‘foo’. In doing so we call solveEqualities to solve any kind equalities in foo’s signature. So the solver may see free occurrences of ‘k’.

See calls to tcExtendTyVarEnv for other places that ordinary TyVars are bought into scope, and hence may show up in the types and kinds generated by TcHsType.

The pattern-match overlap checker calls the constraint solver, long afer TcTyVars have been zonked away

It’s convenient to simply treat these TyVars as skolem constants, which of course they are. We give them a level number of “outermost”, so they behave as global constants. Specifically:

Var.tcTyVarDetails succeeds on a TyVar, returning vanillaSkolemTv, as well as on a TcTyVar.
tcIsTcTyVar returns True for both TyVar and TcTyVar variants of Var.Var. The “tc” prefix means “a type variable that can be encountered by the typechecker”.

This is a bit of a change from an earlier era when we remoselessly insisted on real TcTyVars in the type checker. But that seems unnecessary (for skolems, TyVars are fine) and it’s now very hard to guarantee, with the advent of kind equalities.

Note [Coercion variables in free variable lists]¶

There are several places in the GHC codebase where functions like tyCoVarsOfType, tyCoVarsOfCt, et al. are used to compute the free type variables of a type. The “Co” part of these functions’ names shouldn’t be dismissed, as it is entirely possible that they will include coercion variables in addition to type variables! As a result, there are some places in TcType where we must take care to check that a variable is a _type_ variable (using isTyVar) before calling tcTyVarDetails–a partial function that is not defined for coercion variables–on the variable. Failing to do so led to GHC #12785.

See Note [TcTyVars and TyVars in the typechecker]

Note [TcRhoType]¶

A TcRhoType has no foralls or contexts at the top, or to the right of an arrow: YES (forall a. a->a) -> Int NO forall a. a -> Int NO Eq a => a -> a NO Int -> forall a. a -> Int

Note [Signature skolems]¶

A TyVarTv is a specialised variant of TauTv, with the following invarints:

A TyVarTv can be unified only with a TyVar, not with any other type

Its MetaDetails, if filled in, will always be another TyVarTv or a SkolemTv

TyVarTvs are only distinguished to improve error messages. Consider this

data T (a:k1) = MkT (S a)
data S (b:k2) = MkS (T b)

When doing kind inference on {S,T} we don’t want skolems for k1,k2, because they end up unifying; we want those TyVarTvs again.

Note [TyVars and TcTyVars during type checking]¶

The Var type has constructors TyVar and TcTyVar. They are used as follows:

TcTyVar: used /only/ during type checking. Should never appear afterwards. May contain a mutable field, in the MetaTv case.
TyVar: is never seen by the constraint solver, except locally inside a type like (forall a. [a] ->[a]), where ‘a’ is a TyVar. We instantiate these with TcTyVars before exposing the type to the constraint solver.

I have swithered about the latter invariant, excluding TyVars from the constraint solver. It’s not strictly essential, and indeed (historically but still there) Var.tcTyVarDetails returns vanillaSkolemTv for a TyVar.

But ultimately I want to seeparate Type from TcType, and in that case we would need to enforce the separation.

A TyVarDetails is inside a TyVar See Note [TyVars and TcTyVars]

Note [TcLevel and untouchable type variables]¶

Each unification variable (MetaTv) and each Implication has a level number (of type TcLevel)
INVARIANTS. In a tree of Implications,

(ImplicInv) The level number (ic_tclvl) of an Implication is
            STRICTLY GREATER THAN that of its parent

(SkolInv)   The level number of the skolems (ic_skols) of an
            Implication is equal to the level of the implication
            itself (ic_tclvl)

(GivenInv)  The level number of a unification variable appearing
            in the 'ic_given' of an implication I should be
            STRICTLY LESS THAN the ic_tclvl of I

(WantedInv) The level number of a unification variable appearing
            in the 'ic_wanted' of an implication I should be
            LESS THAN OR EQUAL TO the ic_tclvl of I
            See Note [WantedInv]

A unification variable is touchable if its level number is EQUAL TO that of its immediate parent implication, and it is a TauTv or TyVarTv (but /not/ FlatMetaTv or FlatSkolTv)

Note [WantedInv]¶

Why is WantedInv important? Consider this implication, where the constraint (C alpha[3]) disobeys WantedInv:

forall[2] a. blah => (C alpha[3])
                     (forall[3] b. alpha[3] ~ b)

We can unify alpha:=b in the inner implication, because ‘alpha’ is touchable; but then ‘b’ has excaped its scope into the outer implication.

Note [Skolem escape prevention]¶

We only unify touchable unification variables. Because of (WantedInv), there can be no occurrences of the variable further out, so the unification can’t cause the skolems to escape. Example:

data T = forall a. MkT a (a->Int) f x (MkT v f) = length [v,x]

We decide (x::alpha), and generate an implication like: [1]forall a. (a ~ alpha[0])

But we must not unify alpha:=a, because the skolem would escape.

For the cases where we DO want to unify, we rely on floating the equality. Example (with same T)

g x (MkT v f) = x && True

We decide (x::alpha), and generate an implication like: [1]forall a. (Bool ~ alpha[0])

We do NOT unify directly, bur rather float out (if the constraint does not mention ‘a’) to get

(Bool ~ alpha[0]) /[1]forall a.()

and NOW we can unify alpha.

The same idea of only unifying touchables solves another problem. Suppose we had

(F Int ~ uf[0]) / [1](forall a. C a => F Int ~ beta[1])

In this example, beta is touchable inside the implication. The first solveSimpleWanteds step leaves ‘uf’ un-unified. Then we move inside the implication where a new constraint

uf ~ beta

emerges. If we (wrongly) spontaneously solved it to get uf := beta, the whole implication disappears but when we pop out again we are left with (F Int ~ uf) which will be unified by our final zonking stage and uf will get unified once more to (F Int).

Note [TcLevel assignment]¶

We arrange the TcLevels like this

0 Top level 1 First-level implication constraints 2 Second-level implication constraints …etc…

Note [Silly type synonym]¶

Consider: type T a = Int

What are the free tyvars of (T x)? Empty, of course!

exactTyCoVarsOfType is used by the type checker to figure out exactly which type variables are mentioned in a type. It only matters occasionally – see the calls to exactTyCoVarsOfType.

Historical note: years and years ago this function was used during generalisation – see #1813. But that code has long since died.

Note [anyRewritableTyVar must be role-aware]¶

anyRewritableTyVar is used during kick-out from the inert set, to decide if, given a new equality (a ~ ty), we should kick out a constraint C. Rather than gather free variables and see if ‘a’ is among them, we instead pass in a predicate; this is just efficiency.

Moreover, consider: work item: [G] a ~R f b inert item: [G] b ~R f a

We use anyRewritableTyVar to decide whether to kick out the inert item, on the grounds that the work item might rewrite it. Well, ‘a’ is certainly free in [G] b ~R f a. But because the role of a type variable (‘f’ in this case) is nominal, the work item can’t actually rewrite the inert item. Moreover, if we were to kick out the inert item the exact same situation would re-occur and we end up with an infinite loop in which each kicks out the other (#14363).

Note [Expanding superclasses]¶

When we expand superclasses, we use the following algorithm:

transSuperClasses( C tys ) returns the transitive superclasses: of (C tys), not including C itself
For example: class C a b => D a b class D b a => C a b
Then: transSuperClasses( Ord ty ) = [Eq ty] transSuperClasses( C ta tb ) = [D tb ta, C tb ta]

Notice that in the recursive-superclass case we include C again at the end of the chain. One could exclude C in this case, but the code is more awkward and there seems no good reason to do so. (However C.f. TcCanonical.mk_strict_superclasses, which /does/ appear to do so.)

The algorithm is expand( so_far, pred ):

If pred is not a class constraint, return empty set
      Otherwise pred = C ts
If C is in so_far, return empty set (breaks loops)
Find the immediate superclasses constraints of (C ts)
For each such sc_pred, return (sc_pred : expand( so_far+C, D ss )

Notice that

With normal Haskell-98 classes, the loop-detector will never bite, so we’ll get all the superclasses.

We need the loop-breaker in case we have UndecidableSuperClasses on

Since there is only a finite number of distinct classes, expansion must terminate.

The loop breaking is a bit conservative. Notably, a tuple class could contain many times without threatening termination:

(Eq a, (Ord a, Ix a))

And this is try of any class that we can statically guarantee as non-recursive (in some sense). For now, we just make a special case for tuples. Something better would be cool.

See also TcTyDecls.checkClassCycles.

Note [Lift equality constaints when quantifying]¶

We can’t quantify over a constraint (t1 ~# t2) because that isn’t a predicate type; see Note [Types for coercions, predicates, and evidence] in Type.hs.

So we have to ‘lift’ it to (t1 ~ t2). Similarly (~R#) must be lifted to Coercible.

This tiresome lifting is the reason that pick_me (in pickQuantifiablePreds) returns a Maybe rather than a Bool.

Note [Quantifying over equality constraints]¶

Should we quantify over an equality constraint (s ~ t)? In general, we don’t. Doing so may simply postpone a type error from the function definition site to its call site. (At worst, imagine (Int ~ Bool)).

However, consider this: forall a. (F [a] ~ Int) => blah

Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call site we will know ‘a’, and perhaps we have instance F [Bool] = Int. So we do quantify over a type-family equality where the arguments mention the quantified variables.

Note [Inheriting implicit parameters]¶

Consider this:

f x = (x::Int) + ?y

where f is not a top-level binding. From the RHS of f we’ll get the constraint (?y::Int). There are two types we might infer for f:

f :: Int -> Int

(so we get ?y from the context of f’s definition), or

f :: (?y::Int) => Int -> Int

At first you might think the first was better, because then ?y behaves like a free variable of the definition, rather than having to be passed at each call site. But of course, the WHOLE IDEA is that ?y should be passed at each call site (that’s what dynamic binding means) so we’d better infer the second.

BOTTOM LINE: when inferring types you must quantify over implicit parameters, even if they don’t mention the bound type variables. Reason: because implicit parameters, uniquely, have local instance declarations. See pickQuantifiablePreds.

Note [Quantifying over equality constraints]¶

Should we quantify over an equality constraint (s ~ t)? In general, we don’t. Doing so may simply postpone a type error from the function definition site to its call site. (At worst, imagine (Int ~ Bool)).

However, consider this: forall a. (F [a] ~ Int) => blah

Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call site we will know ‘a’, and perhaps we have instance F [Bool] = Int. So we do quantify over a type-family equality where the arguments mention the quantified variables.

Note [AppTy and ReprEq]¶

Consider a ~R# b a: a ~R# a b
The former is /not/ a definite error; we might instantiate ‘b’ with Id: newtype Id a = MkId a

but the latter /is/ a definite error.

On the other hand, with nominal equality, both are definite errors

Note [Visible type application]¶

GHC implements a generalisation of the algorithm described in the “Visible Type Application” paper (available from http://www.cis.upenn.edu/~sweirich/publications.html). A key part of that algorithm is to distinguish user-specified variables from inferred variables. For example, the following should typecheck:

f :: forall a b. a -> b -> b
f = const id

g = const id

x = f @Int @Bool 5 False
y = g 5 @Bool False

The idea is that we wish to allow visible type application when we are instantiating a specified, fixed variable. In practice, specified, fixed variables are either written in a type signature (or annotation), OR are imported from another module. (We could do better here, for example by doing SCC analysis on parts of a module and considering any type from outside one’s SCC to be fully specified, but this is very confusing to users. The simple rule above is much more straightforward and predictable.)

So, both of f’s quantified variables are specified and may be instantiated. But g has no type signature, so only id’s variable is specified (because id is imported). We write the type of g as forall {a}. a -> forall b. b -> b. Note that the a is in braces, meaning it cannot be instantiated with visible type application.

Tracking specified vs. inferred variables is done conveniently by a field in TyBinder.

Note [Foreign import dynamic]¶

A dynamic stub must be of the form ‘FunPtr ft -> ft’ where ft is any foreign type. Similarly, a wrapper stub must be of the form ‘ft -> IO (FunPtr ft)’.

We use isFFIDynTy to check whether a signature is well-formed. For example, given a (illegal) declaration like:

foreign import ccall “dynamic”: foo :: FunPtr (CDouble -> IO ()) -> CInt -> IO ()

isFFIDynTy will compare the ‘FunPtr’ type ‘CDouble -> IO ()’ with the curried result type ‘CInt -> IO ()’, and return False, as they are not equal.

These chaps do the work; they are not exported¶

Note [Marshalling void]¶

We don’t treat State# (whose PrimRep is VoidRep) as marshalable. In turn that means you can’t write

foreign import foo :: Int -> State# RealWorld

Reason: the back end falls over with panic “primRepHint:VoidRep”;: and there is no compelling reason to permit it

Note [Paterson conditions on PredTypes]¶

We are considering whether class constraints terminate (see Note [Paterson conditions]). Precisely, the Paterson conditions would have us check that “the constraint has fewer constructors and variables (taken together and counting repetitions) than the head.”.

However, we can be a bit more refined by looking at which kind of constraint this actually is. There are two main tricks:

1. It seems like it should be OK not to count the tuple type constructor
   for a PredType like (Show a, Eq a) :: Constraint, since we don't
   count the "implicit" tuple in the ThetaType itself.

In fact, the Paterson test just checks each component of the top level ThetaType against the size bound, one at a time. By analogy, it should be OK to return the size of the largest tuple component as the size of the whole tuple.

2. Once we get into an implicit parameter or equality we
   can't get back to a class constraint, so it's safe
   to say "size 0".  See #4200.

NB: we don’t want to detect PredTypes in sizeType (and then call sizePred on them), or we might get an infinite loop if that PredType is irreducible. See #5581.

Fork me on GitHub