[commit: ghc] master: Comments about polymorphic recursion (6c794c3)

[git at git.haskell.org]

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

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/6c794c311d5312ba3f92434ee6f35040d3b69353/ghc

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

commit 6c794c311d5312ba3f92434ee6f35040d3b69353
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Tue Dec 8 13:11:42 2015 +0000

    Comments about polymorphic recursion
    
    See Trac #11176


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

6c794c311d5312ba3f92434ee6f35040d3b69353
 compiler/hsSyn/HsBinds.hs     | 54 ++++++++++++++++++++++++++++++++++++-------
 compiler/typecheck/TcBinds.hs |  5 ++--
 2 files changed, 49 insertions(+), 10 deletions(-)

diff --git a/compiler/hsSyn/HsBinds.hs b/compiler/hsSyn/HsBinds.hs
index 25ce654..79206d7 100644
--- a/compiler/hsSyn/HsBinds.hs
+++ b/compiler/hsSyn/HsBinds.hs
@@ -263,7 +263,7 @@ Note [AbsBinds]
 ~~~~~~~~~~~~~~~
 The AbsBinds constructor is used in the output of the type checker, to record
 *typechecked* and *generalised* bindings.  Consider a module M, with this
-top-level binding
+top-level binding, where there is no type signature for M.reverse,
     M.reverse []     = []
     M.reverse (x:xs) = M.reverse xs ++ [x]
 
@@ -282,8 +282,8 @@ Notice that 'M.reverse' is polymorphic as expected, but there is a local
 definition for plain 'reverse' which is *monomorphic*.  The type variable
 'a' scopes over the entire letrec.
 
-That's after desugaring.  What about after type checking but before desugaring?
-That's where AbsBinds comes in.  It looks like this:
+That's after desugaring.  What about after type checking but before
+desugaring?  That's where AbsBinds comes in.  It looks like this:
 
    AbsBinds { abs_tvs     = [a]
             , abs_exports = [ABE { abe_poly = M.reverse :: forall a. [a] -> [a],
@@ -305,11 +305,11 @@ you were defining) appears in the abe_poly field of the
 abs_exports. The bindings in abs_binds are for fresh, local, Ids with
 a *monomorphic* Id.
 
-If there is a group of mutually recursive functions without type
-signatures, we get one AbsBinds with the monomorphic versions of the
-bindings in abs_binds, and one element of abe_exports for each
-variable bound in the mutually recursive group.  This is true even for
-pattern bindings.  Example:
+If there is a group of mutually recursive (see Note [Polymoprhic
+recursion]) functions without type signatures, we get one AbsBinds
+with the monomorphic versions of the bindings in abs_binds, and one
+element of abe_exports for each variable bound in the mutually
+recursive group.  This is true even for pattern bindings.  Example:
         (f,g) = (\x -> x, f)
 After type checking we get
    AbsBinds { abs_tvs     = [a]
@@ -319,6 +319,44 @@ After type checking we get
                                   , abe_mono = g :: a -> a }]
             , abs_binds = { (f,g) = (\x -> x, f) }
 
+Note [Polymoprhic recursion]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   Rec { f x = ...(g ef)...
+
+       ; g :: forall a. [a] -> [a]
+       ; g y = ...(f eg)...  }
+
+These bindings /are/ mutually recursive (f calls g, and g calls f).
+But we can use the type signature for g to break the recursion,
+like this:
+
+  1. Add g :: forall a. [a] -> [a] to the type environment
+
+  2. Typecheck the definition of f, all by itself,
+     including generalising it to find its most general
+     type, say f :: forall b. b -> b -> [b]
+
+  3. Extend the type environment with that type for f
+
+  4. Typecheck the definition of g, all by itself,
+     checking that it has the type claimed by its signature
+
+Steps 2 and 4 each generate a separate AbsBinds, so we end
+up with
+   Rec { AbsBinds { ...for f ... }
+       ; AbsBinds { ...for g ... } }
+
+This approach allows both f and to call each other
+polymoprhically, even though only g has a signature.
+
+We get an AbsBinds that encompasses multiple source-program
+bindings only when
+ * Each binding in the group has at least one binder that
+   lacks a user type signature
+ * The group forms a strongly connected component
+
+
 Note [AbsBinds wrappers]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 5c6593a..96aec1e 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -442,6 +442,7 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
         -- strongly-connected-component analysis, this time omitting
         -- any references to variables with type signatures.
         -- (This used to be optional, but isn't now.)
+        -- See Note [Polymorphic recursion] in HsBinds.
     do  { traceTc "tc_group rec" (pprLHsBinds binds)
         ; when hasPatSyn $ recursivePatSynErr binds
         ; (binds1, thing) <- go sccs
@@ -502,10 +503,10 @@ tc_single top_lvl sig_fn prag_fn lbind thing_inside
        ; return (binds1, thing) }
 
 ------------------------
-mkEdges :: TcSigFun -> LHsBinds Name -> [Node BKey (LHsBind Name)]
-
 type BKey = Int -- Just number off the bindings
 
+mkEdges :: TcSigFun -> LHsBinds Name -> [Node BKey (LHsBind Name)]
+-- See Note [Polymorphic recursion] in HsBinds.
 mkEdges sig_fn binds
   = [ (bind, key, [key | n <- nameSetElems (bind_fvs (unLoc bind)),
                          Just key <- [lookupNameEnv key_map n], no_sig n ])