RE: Mutually recursive bindings

Tom Pledger writes:
 > [...]
 > 
 > For example, with FLAMV = free variables which will be lambda-bound,
 > and FLETV = free variables which will be let-bound, and ! marking the
 > alleged innovations:
 > 
 >     h = \x -> (x==x) || h True || h "hello"
 >               [...]
 >         -----------------------------------
 >         Eq b => (b -> Bool;
 >                  FLETV: h_1st::Bool -> Bool, h_2nd::[Char] -> Bool)
 >     ---------------------------------------
 >     (Tentatively give h its quantified type)
 >     h :: forall b . Eq b => b -> Bool
 >   ! (Discharge the h_1st requirement, by unifying Bool -> Bool
 >   !  with a fresh instance of forall b . Eq b => b -> Bool)
 >   ! (Discharge the h_2nd requirement, by unifying [Char] -> Bool
 >   !  with another fresh instance of forall b . Eq b => b -> Bool)
 > 
 > [...] technique of deferring unification for uses of let-bound
 > variables until after quantification.

The quantification over the type variables which are free inside the
declaration but not outside it, that is.

So, in cases like this (more or less as seen in section 4.5.4 of the
Haskell 98 report), we still get the proper behaviour:

    f x = let g y z = ([x, y], z) in (g True, g 'c')

              -------------------
              g :: forall b . a -> b -> ([a], b)
                                     ---------------
                                     Free vars which will be let-bound:
                                     g_1st :: Bool -> c
                                     g_2nd :: Char -> d
              --------------------------------------
              Discharge the g_1st requirement by unifying
                  a -> e -> ([a], e)  with  Bool -> c
              Now  g :: forall b . Bool -> b -> ([Bool], b)
              Fail to discharge the g_2nd requirement, because we can't
                  unify  Bool -> f -> ([Bool], f)  with  Char -> d

It seems reasonable that when there is no explicit type signature, we
should first infer one from how the parameters are used, and only then
check that any recursive uses make sense.  I'm not sure whether this
is a departure from Hindley-Milner norms.  Will someone who knows
please comment?

Regards,
Tom