[commit: ghc] master: TcMType: Add some elementary notes (871c96f)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/871c96f10edecbf6107d4a930dfaa8596ad08b8d/ghc

>---------------------------------------------------------------

commit 871c96f10edecbf6107d4a930dfaa8596ad08b8d
Author: Ben Gamari <bgamari.foss at gmail.com>
Date:   Tue Feb 2 14:50:22 2016 +0100

    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


>---------------------------------------------------------------

871c96f10edecbf6107d4a930dfaa8596ad08b8d
 compiler/typecheck/TcHsSyn.hs   |  9 +++++++-
 compiler/typecheck/TcMType.hs   | 49 +++++++++++++++++++++++++++++++++++++++++
 compiler/typecheck/TcPluginM.hs |  2 +-
 3 files changed, 58 insertions(+), 2 deletions(-)

diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 4289035..72052b1 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -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
 
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 3d9e57c..143a392 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -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
diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs
index 7ba1f51..c405440 100644
--- a/compiler/typecheck/TcPluginM.hs
+++ b/compiler/typecheck/TcPluginM.hs
@@ -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