[Haskell] GADT and constraints [Was: Rebindable syntax for monads and arrows]

[oleg at pobox.com]

Simon Peyton-Jones wrote:

|[ data MyVec a where
|[   MkMyVec :: (Foo a) => a -> MyVec a
>
>   f x = case x of
>           MkMyVec x -> <rhs>
>
> constraints are always solved *lazily* when inferring, so we'd infer
>                 f :: Foo [a] => MyVec a -> ...
>                 even without any overlap
>
>         but they are solved *eagerly* when checking against a
> user-supplied type sig
>         so when checking
>                 f :: Eq a => MyVec a => ...
>         we'd accept the program.  (If there were overlapping instances,
> we'd complain about them.)

I can't understand how constraints float at all. In the following code:

> class Foo1 a  where foo1 :: a -> String
> class Foo2 a  where foo2 :: a -> String
>
> instance Foo1 Bool where foo1 _ = "Bool"
> instance Foo2 Char where foo2 _ = "Char"
>
> data U a where
>   Ub :: a -> U a
>   Uc :: a -> U a
>
> foo (Ub a) = foo1 a
> foo (Uc a) = foo2 a

What is the type of foo? GHC snapshot 6.3.20041106 happily accepts
that code, and even infers 
	*M> :t foo
	foo :: forall a. (Foo2 a, Foo1 a) => U a -> String

but that seems odd. In any value of type U a, either Ub alternative is
present, or Uc. They can never be both. Then why do we get the
constraint that is the intersection of the two constraints rather than
the union of them?  BTW, when I tried to do

> data U a where
>   Ub :: Foo1 => a -> U a
>   Uc :: Foo2 => a -> U a


I received a message

>     Couldn't match kind `*' against `k_a1QK -> *'
>     In the class declaration for `Foo2'

which I found quite interesting. 

Anyway, even though GHC accepts the code and infers the type for foo,
the function is unusable. An attempt to evaluate 'foo (Ub True)' ends
up in an error message that there is no instance of Foo2 Bool. Indeed,
there isn't. But why that should matter if I'm only interested in the
Ub alternative? Again, the function 'foo' seems legitimate, and can be
easily expressed either in Martin Sulzmann's interpretation of GRDT
via existentials, or using the typeclass representation of GADT. For
example:

> data Ub a = Ub a
> data Uc a = Uc a
>
> class Foo t where foo:: t -> String
>
> instance Foo1 a => Foo (Ub a) where 
>     foo (Ub a) = foo1 a
> instance Foo2 a => Foo (Uc a) where 
>     foo (Uc a) = foo2 a

Here, the constraint Foo is clearly the `union' of Foo1 and Foo2 (the
discriminated union at that).