flexible contexts and context reduction

[Claus Reinke]

> Because I want to be able to make Foo values where the parameter type isn't in Ord, too. I just 
> want unFoo to work on specific Foo values where it is.

but your recursive function requires a recursive constraint,
which your data type does not guarantee by construction,
and which the Ord instances do not guarantee due to lack
of closed classes.

a rather pedestrian approach would record during construction
whether or not all parts are in Ord (see below).

i really wanted to record that information only in the leaf, using
the type family and the commented-out parts to propagate the
information through Foo2, but unfortunately, ghc does not see
that the only case for which And returns True requires both
parameters to be True (closed families/classes would help,
again?), so i had to split up Foo2 as well.

not pretty, but might get you a step further? perhaps some of
Oleg's workarounds for closed classes and context-based
overloading might help to merge the four constructors into two
again. that would get rid of the junk (you can't promise too
much, but you can promise too little by using the wrong
constructor version below).

claus

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
module Foo where

data True  = T
data False = F

type family And a b :: *
type instance And True True   = True
type instance And True False  = False
type instance And False True  = False
type instance And False False = False

data Foo ord a where
   Foo1  ::          a -> Foo False a
   Foo1o :: Ord a => a -> Foo True a
-- Foo2  :: And oa ob ~ ord => ord -> Foo oa a -> Foo ob b -> Foo ord (a, b)
   Foo2  ::                           Foo oa a -> Foo ob b -> Foo False (a, b)
   Foo2o ::                           Foo True a -> Foo True b -> Foo True (a, b)

unFoo :: Foo True a -> a
unFoo (Foo1o a)    = if a>a then a else a
-- unFoo (Foo2 T x y) = (unFoo x, unFoo y)
unFoo (Foo2o x y) = (unFoo x, unFoo y)



>> 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]