TcMType: Add some elementary notes
authorBen Gamari <bgamari.foss@gmail.com>
Tue, 2 Feb 2016 13:50:22 +0000 (14:50 +0100)
committerBen Gamari <ben@smart-cactus.org>
Tue, 2 Feb 2016 18:40:11 +0000 (19:40 +0100)
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

compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPluginM.hs

index 4289035..72052b1 100644 (file)
@@ -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
 
index 3d9e57c..143a392 100644 (file)
@@ -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
index 7ba1f51..c405440 100644 (file)
@@ -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