flexible contexts and context reduction

[Claus Reinke]

perhaps i'm missing something but, instead of trying to deduce
conditions from conclusions, why can't you just follow ghc's
suggestion, and add the constraints to the constructor?

data Foo a where
   Foo1 :: a -> Foo a
   Foo2 :: (Ord a,Ord b) => Foo a -> Foo b -> Foo (a, b)

(possibly with another constraint on Foo1)

claus

> A closer example to what I was actually doing was this:
> 
> {-# LANGUAGE GADTs #-}
> module Foo where
> 
> data Foo a where
>   Foo1 :: a -> Foo a
>   Foo2 :: Foo a -> Foo b -> Foo (a, b)
> 
> unFoo :: Ord a => Foo a -> a
> unFoo (Foo1 a) = a
> unFoo (Foo2 x y) = (unFoo x, unFoo y)
> 
> [in the real code I did actually use the Ord constraint in the base case]
> 
> The error I get is this:
> 
> Foo.hs:10:20:
>    Could not deduce (Ord a2) from the context ()
>      arising from a use of `unFoo' at Foo.hs:10:20-26
>    Possible fix: add (Ord a2) to the context of the constructor `Foo2'
>    In the expression: unFoo x
>    In the expression: (unFoo x, unFoo y)
>    In the definition of `unFoo': unFoo (Foo2 x y) = (unFoo x, unFoo y)
> 
> Foo.hs:10:29:
>    Could not deduce (Ord b1) from the context ()
>      arising from a use of `unFoo' at Foo.hs:10:29-35
>    Possible fix: add (Ord b1) to the context of the constructor `Foo2'
>    In the expression: unFoo y
>    In the expression: (unFoo x, unFoo y)
>    In the definition of `unFoo': unFoo (Foo2 x y) = (unFoo x, unFoo y)
> 
> Which suggests that GHC has also lost track of the fact that Ord (a, b) is true. But 
> it would certainly be necessary to get from Ord (a, b) to (Ord a, Ord b) to get that
> to work.