[Haskell-cafe] Quantification in Instance Contexts

[Julian K. Arni]

Hi Cafe,

I'm playing around with simple logic-programming at the type level. For 
instance, encoding trees:

>> {-# LANGUAGE MultiParamTypeClasses
>> , FunctionalDependencies
>> , FlexibleInstances
>> , UndecidableInstances
>> , FlexibleContexts
>> , OverlappingInstances #-}
>> {-# OPTIONS_GHC -fcontext-stack=100 #-}
>> 
>> 
>> --     *A
>> --    / \
>> --  B*   *C
>> --   |
>> --  D*
>> 
>> 
>> data A
>> data B
>> data C
>> data D
>> class Child a b bool | a b -> bool
>> instance Child A B TrueT
>> instance Child B D TrueT
>> instance Child B C TrueT
>> class Path a b bool | a b -> bool

Now the following obviously doesn't work (never mind for now that 'Path' needs 
a recursive definition, and that this is really just 'Grandchild'):

>> instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT

Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep, 
because 'b' *is* in fact ambiguous. What I want to tell the compiler is that 
it's really okay, since the RHS side (and any possible 'where' expressions) 
doesn't depend on what is instantiated for 'b'.  

I know I could switch to a class 'Children a bs bool' and encode all children 
of as a type-level list, and then have a fundep between 'a' and 'bs'. That's 
not a *bad* solution: it does give a good sense of the intention. But it's not 
very extensible; really I'd rather be using something like 'forall' 
- something, I would guess, along the lines of:

>> instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) => Path 
>> a c TrueT

That, however, fails with:

    Malformed instance head: (forall b.
                              (Child a b TrueT, Child b c TrueT))
                             -> Path a c TrueT
    In the instance declaration for ‘Path a c TrueT’


So: is there a way (presumably with 'forall') of telling the compiler that the 
ambiguous type 'b' actually won't "leak through" to the RHS, so stop bugging me 
about ambiguity?

Thanks,
  Julian