cvs commit: fptools/ghc/compiler/typecheck TcMonad.lhs TcSimp lify.lhs fptools/ghc/compiler/types FunDeps.lhs Unify.lhs

[Marcin 'Qrczak' Kowalczyk]

Tue, 30 Jan 2001 07:04:29 -0800, Simon Peyton-Jones <simonpj@microsoft.com> pisze:

> Now is this ok?
> 
> 	f :: forall b. C Char b => Char -> b -> Int
> 	f x y = op x y
> 
> Mark J says yes, that's a principlal type for f.  But I just don't
> know how to implement the test.

Perhaps by "simplifying" the provided signature at the beginning,
and then proceeding as currently. The type forall b. C Char b =>
Char -> b -> Int would be completely equivalent to Char -> Bool -> Int.

I see no problem in this.

                                --------

There is a separate question about this:
    f :: forall b. C Char b => Char -> b -> Int
    f x (y::b) = op x (y::b)

Currently ghc doesn't allow to write a type variable in a pattern
signature when the corresponding type is known to be more specific.

OTOH OCaml does allow even
    f (x : 'a) = (x : 'b) + 1
Type signatures are only unified with the inferred type; they can be
more general than the real type.

ghc's behavior is sometimes more convenient (catches an error when
the programmer thinks that a type is more general than it really is),
sometimes less (the programmer must know what exactly can be inferred,
even if he doesn't want to constrain anything at this place but
just get a name of a type of a lambda-bound variable to use it in
a different place, no matter what it really is).

Here it's bad. It should not matter if the type can be inferred to a
concrete type or it's a constrained type variable. All I want is to
bind it to a name.

Perhaps it would make sense to adopt OCaml's treatment of type
signatures, at least for pattern and result type signatures.  Doing it
for all signatures (thus eliminating many needs of using pattern
signatures at all!) is probably too radical...

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK