Implement the Haskell' proposal for polymorphic pattern bindings

[simonmar]

After discussion on the Haskell' mailing list, it was decided that Haskell' will keep polymorphic pattern bindings, with static semantics defined by a translation.

 http://hackage.haskell.org/trac/haskell-prime/wiki/SpecifyPatternBindingSemantics

[simonpj]

See also #2187

[simonpj@…]

commit 49dbe60558deee5ea6cd2c7730b7c591d15559c8

Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Tue Aug 16 10:23:52 2011 +0100

    Major improvement to pattern bindings
    
    This patch makes a number of related improvements
    
    a) Implements the Haskell Prime semantics for pattern bindings
       (Trac #2357).  That is, a pattern binding p = e is typed
       just as if it had been written
            t = e
            f = case t of p -> f
            g = case t of p -> g
            ... etc ...
       where f,g are the variables bound by p. In paricular it's
       ok to say
          (f,g) = (\x -> x, \y -> True)
       and f and g will get propertly inferred types
          f :: a -> a
          g :: a -> Int
    
    b) Eliminates the MonoPatBinds flag altogether.  (For the moment
       it is deprecated and has no effect.)  Pattern bindings are now
       generalised as per (a).  Fixes Trac #2187 and #4940, in the
       way the users wanted!
    
    c) Improves the OutsideIn algorithm generalisation decision.
       Given a definition without a type signature (implying "infer
       the type"), the published algorithm rule is this:
          - generalise *top-level* functions, and
          - do not generalise *nested* functions
       The new rule is
          - generalise a binding whose free variables have
            Guaranteed Closed Types
          - do not generalise other bindings
    
       Generally, a top-level let-bound function has a Guaranteed
       Closed Type, and so does a nested function whose free vaiables
       are top-level functions, and so on. (However a top-level
       function that is bitten by the Monomorphism Restriction does
       not have a GCT.)
    
       Example:
         f x = let { foo y = y } in ...
       Here 'foo' has no free variables, so it is generalised despite
       being nested.
    
    d) When inferring a type f :: ty for a definition f = e, check that
       the compiler would accept f :: ty as a type signature for that
       same definition.  The type is rejected precisely when the type
       is ambiguous.
    
       Example:
          class Wob a b where
            to :: a -> b
            from :: b -> a
    
          foo x = [x, to (from x)]
       GHC 7.0 would infer the ambiguous type
          foo :: forall a b. Wob a b => b -> [b]
       but that type would give an error whenever it is called; and
       GHC 7.0 would reject that signature if given by the
       programmer.  The new type checker rejects it up front.
    
       Similarly, with the advent of type families, ambiguous types are
       easy to write by mistake.  See Trac #1897 and linked tickets for
       many examples.  Eg
          type family F a :: *
          f ::: F a -> Int
          f x = 3
       This is rejected because (F a ~ F b) does not imply a~b.  Previously
       GHC would *infer* the above type for f, but was unable to check it.
       Now even the inferred type is rejected -- correctly.
    
    The main implemenation mechanism is to generalise the abe_wrap
    field of ABExport (in HsBinds), from [TyVar] to HsWrapper. This
    beautiful generalisation turned out to make everything work nicely
    with minimal programming effort.  All the work was fiddling around
    the edges; the core change was easy!

 compiler/deSugar/DsBinds.lhs        |   62 +++-----
 compiler/deSugar/DsExpr.lhs         |    6 +-
 compiler/hsSyn/HsBinds.lhs          |   28 +++-
 compiler/hsSyn/HsUtils.lhs          |   32 +++--
 compiler/main/DynFlags.hs           |   13 +-
 compiler/rename/RnBinds.lhs         |    6 +-
 compiler/typecheck/TcBinds.lhs      |  282 ++++++++++++++++++++--------------
 compiler/typecheck/TcClassDcl.lhs   |   12 +-
 compiler/typecheck/TcEnv.lhs        |  117 +++++++++------
 compiler/typecheck/TcErrors.lhs     |   32 +++--
 compiler/typecheck/TcHsSyn.lhs      |   14 +-
 compiler/typecheck/TcInstDcls.lhs   |   19 ++-
 compiler/typecheck/TcMType.lhs      |    6 +-
 compiler/typecheck/TcRnDriver.lhs   |   14 +-
 compiler/typecheck/TcRnMonad.lhs    |    2 +-
 compiler/typecheck/TcRnTypes.lhs    |   11 +-
 compiler/typecheck/TcSimplify.lhs   |   57 +++++---
 compiler/typecheck/TcTyClsDecls.lhs |    4 +-
 compiler/typecheck/TcType.lhs       |   28 ++--
 19 files changed, 439 insertions(+), 306 deletions(-)

[simonpj]

Free at last, free at last. This long standing change is finally done!

Simon

[simonpj]

Concerning (c) see  http://www.haskell.org/pipermail/glasgow-haskell-users/2011-June/020489.html

[simonmar]

Great, thanks Simon!

[MartijnVanSteenbergen]

Thank you, that's great news!

Just yesterday I wrote three programs which used -XNoMonoPatBinds and respectively caused the type-checker to hang, to panic and compiled fine but (seemed to) have wrong behaviour, using GHC 7.0.3.

I've made the panic program as small as I could:

{-# LANGUAGE NoMonoPatBinds #-}

f :: Show a => a
(f, _) = undefined

g :: Show a => a
g = f

Perhaps you can use it as a test case for the new algorithm.

If I manage to make the other programs smaller too, I'll post them here.

[MartijnVanSteenbergen]

It also panicks in 7.2.1. Here are the error messages:

ghc: panic! (the 'impossible' happened)
  (GHC version 7.0.3 for i386-apple-darwin):
	applyTypeToArgs
    f{v ait} [lid] $dShow{v aiz} [lid]
    a{tv aiy} [sk]

ghc: panic! (the 'impossible' happened)
  (GHC version 7.2.1 for x86_64-apple-darwin):
    applyTypeToArgs
    f{v ahK} [lid] $dShow{v ahQ} [lid]
    a{tv ahP} [sk]

[simonpj]

Works in HEAD!

Incidentally, always use -dcore-lint when you get weird crashes. It often picks up the error earlier.

If you make other test cases we can add them too.

Simon

[MartijnVanSteenbergen]

Awesome! Will do.