Comments about polymorphic recursion

See Trac #11176

2 files changed, 49 insertions, 10 deletions

diff --git a/compiler/hsSyn/HsBinds.hs b/compiler/hsSyn/HsBinds.hs
index 25ce654ecd..79206d717f 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 5c6593a505..96aec1eefe 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 ])