increase polymorphism, base HVariantF on VariantF

[sheaf]

I found it inconvenient to have to specify the return type in the reduceVariant function, as in certain situations one might want a polymorphic return type, such as forall m. Monad m => m XYZ. I think it makes more sense to let the return type be universally quantified.

I similarly changed some functions dealing with VariantF, which makes them more general.

I also added some functionality to EGADT to make the VF pattern synonym easier to use. I think it wouldn't be much effort now to merge the new :<! with the previous :<. I'm trying to keep the constraints simple and avoid recursive definitions as much as possible, as the type-level lists should be traversed as few times as possible (it can really strain the constraint solver if we start accumulating large expressions arising from folding through a type-level lists).

P.S. I notice that the current implementation of reduceVariant is recursive. Would it make more sense to have something like

class ReduceVariant c (as :: [Type]) where
  reduceVariant :: ( forall a. c a => a -> r ) -> V a -> r

instance ( forall x. (x :< xs) => c x ) => ReduceVariant c xs where
  reduceVariant f (Variant i a) = case someNatVal ( fromIntegral i ) of
    ( SomeNat ( _ :: Proxy i) ) -> f ( unsafeCoerce a :: Index i xs )

(This quantified constraint isn't right due to the way these are resolved, but I think you understand the spirit.)
Similar comments apply to BottomUp (which could be renamed ReduceVariantF).

[xgrommx]

Looks good for me. Also preferable case is reusing VariantF and ApplyAll for EGADTs without creating smth like HApplyAll

[sheaf]

At the moment the EGADT code is still missing an equivalent of PopVariant. However, as that functionality is not needed to define the pattern synonym, I decided to forgo it momentarily.
In the other pull request (#27) I am attempting to unify the type families used. The idea would then be to remove many of the ApplyAll type family applications in the VariantF module, and have as many of the constraints formulated in terms of the unapplied constructors (to make them more general and improve code re-use). In this PR I managed to do the same thing for the EGADT module, including removing HApplyAll.

[hsyl20]

Thanks a lot! Merged in master.

P.S. I notice that the current implementation of reduceVariant is recursive. Would it make more sense to have something like

class ReduceVariant c (as :: [Type]) where
 reduceVariant :: ( forall a. c a => a -> r ) -> V a -> r

instance ( forall x. (x :< xs) => c x ) => ReduceVariant c xs where
 reduceVariant f (Variant i a) = case someNatVal ( fromIntegral i ) of
   ( SomeNat ( _ :: Proxy i) ) -> f ( unsafeCoerce a :: Index i xs )

I tried but I didn't manage to implement it like this. The issue is to deal with the local i type parameter and to make it match the top-level class constraint. But if you manage to implement it this way, I'd be happy to replace the recursive code we currently have!