[Haskell-cafe] type families and type signatures

[Martin Sulzmann]

Lennart Augustsson wrote:
> On Wed, Apr 9, 2008 at 8:53 AM, Martin Sulzmann 
> <martin.sulzmann at gmail.com <mailto:martin.sulzmann at gmail.com>> wrote:
>
>
>     Lennart, you said
>
>         (It's also pretty easy to fix the problem.)
>
>
>     What do you mean? Easy to fix the type checker, or easy to fix the
>     program by inserting annotations
>     to guide the type checker?
>
>     Martin
>
>  
> I'm referring to the situation where the type inferred by the type 
> checker is illegal for me to put into the program.
> In our example we can fix this in two ways, by making foo' illegal 
> even when it has no signature, or making foo' legal even when it has a 
> signature.
>
> To make it illegal:  If foo' has no type signature, infer a type for 
> foo', insert this type as a signature and type check again.  If this 
> fails, foo' is illegal.
>
> To make it legal: If foo' with a type signature doesn't type check, 
> try to infer a type without a signature.  If this succeeds then check 
> that the type that was inferred is alpha-convertible to the original 
> signature.  If it is, accept foo'; the signature doesn't add any 
> information.
>
> Either of these two option would be much preferable to the current 
> (broken) situation where the inferred signature is illegal.

I understand now what you meant. See my earlier reply to Claus' email.

Regarding your request to take into account alpha-convertibility when 
checking signatures.
We know that in GHC the check

 (forall a, b. Foo a b => a) <= (forall a, c. Foo a c => a)    (**)

fails cause when testing the constraint/formula derived from the above 
subsumption check

  forall a, b. Foo a b implies exists c. Foo a c

GHC simply drops the exists c bit and clearly

   Foo a b does NOT imply Foo a c

We need to choose c to be equal to b. I call this process "matching" but 
it's of course
a form of alpha-conversion.
(We convince GHC to accept such signatures but encoding System F style
type application via redundant type proxy arguments)

The point I want to make is that in Chameleon I've implemented a 
subsumption check
which takes into account matching. Therefore, (**) is checkable in 
Chameleon.
BUT matching can be fairly expensive, exponential in the worst case, for 
example
consider cases such as Foo x_i x_i+1
So maybe there's good reason why GHC's subsumption check doesn't take 
into account matching.

The slightly odd thing is that GHC uses a "pessimistic" subsumption 
check (no matching) in combination
with an "optimistic" ambiguity check (see my earlier message on this topic).
I'd say it's better to be pessimistic/pessimistic and 
optimistic/optimistic, maybe this could be
a compiler switch?

Martin