Commit 871c96f1 authored by Ben Gamari's avatar Ben Gamari Committed by Ben Gamari

TcMType: Add some elementary notes

It's astoundingly difficult to find a good description of zonking. Given
that there is a Stack Overflow question on the matter, I'm clearly not
the only one who feels this way. Hopefully this will clarify the issue.

Test Plan: Read it

Reviewers: goldfire, austin, simonpj

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D1859
parent db97ed9f
......@@ -19,9 +19,12 @@ module TcHsSyn (
shortCutLit, hsOverLitName,
conLikeResTy,
-- re-exported from TcMonad
-- * re-exported from TcMonad
TcId, TcIdSet,
-- * Zonking
-- | For a description of "zonking", see Note [What is zonking?]
-- in TcMType
zonkTopDecls, zonkTopExpr, zonkTopLExpr,
zonkTopBndrs, zonkTyBndrsX,
emptyZonkEnv, mkEmptyZonkEnv,
......@@ -172,6 +175,7 @@ It's all pretty boring stuff, because HsSyn is such a large type, and
the environment manipulation is tiresome.
-}
-- Confused by zonking? See Note [What is zonking?] in TcMType.
type UnboundTyVarZonker = TcTyVar -> TcM Type
-- How to zonk an unbound type variable
-- Note [Zonking the LHS of a RULE]
......@@ -187,6 +191,8 @@ type UnboundTyVarZonker = TcTyVar -> TcM Type
-- Ids. It is knot-tied. We must be careful never to put coercion variables
-- (which are Ids, after all) in the knot-tied env, because coercions can
-- appear in types, and we sometimes inspect a zonked type in this module.
--
-- Confused by zonking? See Note [What is zonking?] in TcMType.
data ZonkEnv
= ZonkEnv
UnboundTyVarZonker
......@@ -1570,6 +1576,7 @@ zonk_tycomapper = TyCoMapper
, tcm_hole = zonkCoHole
, tcm_tybinder = \env tv _vis -> zonkTyBndrX env tv }
-- Confused by zonking? See Note [What is zonking?] in TcMType.
zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
zonkTcTypeToType = mapType zonk_tycomapper
......
......@@ -975,6 +975,55 @@ skolemiseUnboundMetaTyVar tv details
; return final_tv }
{-
Note [What is a meta variable?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A "meta type-variable", also know as a "unification variable" is a placeholder
introduced by the typechecker for an as-yet-unknown monotype.
For example, when we see a call `reverse (f xs)`, we know that we calling
reverse :: forall a. [a] -> [a]
So we know that the argument `f xs` must be a "list of something". But what is
the "something"? We don't know until we explore the `f xs` a bit more. So we set
out what we do know at the call of `reverse` by instantiate its type with a fresh
meta tyvar, `alpha` say. So now the type of the argument `f xs`, and of the
result, is `[alpha]`. The unification variable `alpha` stands for the
as-yet-unknown type of the elements of the list.
As type inference progresses we may learn more about `alpha`. For example, suppose
`f` has the type
f :: forall b. b -> [Maybe b]
Then we instantiate `f`'s type with another fresh unification variable, say
`beta`; and equate `f`'s result type with reverse's argument type, thus
`[alpha] ~ [Maybe beta]`.
Now we can solve this equality to learn that `alpha ~ Maybe beta`, so we've
refined our knowledge about `alpha`. And so on.
If you found this Note useful, you may also want to have a look at
Section 5 of "Practical type inference for higher rank types" (Peyton Jones,
Vytiniotis, Weirich and Shields. J. Functional Programming. 2011).
Note [What is zonking?]
~~~~~~~~~~~~~~~~~~~~~~~
GHC relies heavily on mutability in the typechecker for efficient operation.
For this reason, throughout much of the type checking process meta type
variables (the MetaTv constructor of TcTyVarDetails) are represented by mutable
variables (known as TcRefs).
Zonking is the process of ripping out these mutable variables and replacing them
with a real TcType. This involves traversing the entire type expression, but the
interesting part of replacing the mutable variables occurs in zonkTyVarOcc.
There are two ways to zonk a Type:
* zonkTcTypeToType, which is intended to be used at the end of type-checking
for the final zonk. It has to deal with unfilled metavars, either by filling
it with a value like Any or failing (determined by the UnboundTyVarZonker
used).
* zonkTcType, which will happily ignore unfilled metavars. This is the
appropriate function to use while in the middle of type-checking.
Note [Zonking to Skolem]
~~~~~~~~~~~~~~~~~~~~~~~~
We used to zonk quantified type variables to regular TyVars. However, this
......
......@@ -150,7 +150,7 @@ newFlexiTyVar = unsafeTcPluginTcM . TcM.newFlexiTyVar
isTouchableTcPluginM :: TcTyVar -> TcPluginM Bool
isTouchableTcPluginM = unsafeTcPluginTcM . TcM.isTouchableTcM
-- Confused by zonking? See Note [What is zonking?] in TcMType.
zonkTcType :: TcType -> TcPluginM TcType
zonkTcType = unsafeTcPluginTcM . TcM.zonkTcType
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment