Apologies for the somewhat contrived example. I've tried to simplify this to the extent that I can without losing the justification:
Suppose I have a multi-parameter typeclass Relation:
class Relation r a b where ....
And a function which is existentially quantified over such a type:
neighbours :: forall r a b. Relation r a b => a -> r -> Graph -> [b]
Now I introduce a couple of instances of Relation:
data Person = Person String
data Pet = Pet String
data Owns = Owns
data Desires = Desires
instance Relation Owns Person Pet
instance Relation Desires Person Pet
Now I would like to write a method which fetches all the pets associated with a given person through some means, without exposing the complexity of implementation:
data PetAttachment = AttachOwns | AttachDesires
personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att g =
neighbours person r g
where
r = case PetAttachment of
AttachOwns -> Owns
AttachDesires -> Desires
My question is: how do I appropriately type r. With no hints, it will try to type as Owns and hence fail. I can alternatively hint that it should be existentially typed:
r :: forall r. Relation r Person Pet => r
But the compiler does not seem able to deduce that Relation r0 Person Pet, saying that r0 is ambiguous:
relation.hs:26:5: No instance for (Relation r0 Person Pet) arising from a use of ‘neighbours’
The type variable ‘r0’ is ambiguous
Can I persuade r to type in such a way as to let this compile?
Full compilable example:
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
data Graph = Graph
class Relation r a b where
relation :: (r,a,b) -> Int
neighbours :: forall r a b. Relation r a b => a -> r -> Graph -> [b]
neighbours = undefined
data Person = Person String
data Pet = Pet String
data Owns = Owns
data Desires = Desires
instance Relation Owns Person Pet where
relation _ = 1
instance Relation Desires Person Pet where
relation _ = 2
data PetAttachment = AttachOwns | AttachDesires
personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att =
neighbours person r
where
r :: forall r. Relation r Person Pet => r
r = case att of
AttachOwns -> Owns
AttachDesires -> Desires
main :: IO ()
main = undefined
Here are two approaches to writing this, one using a GADT and one using a Rank 2 Type.
A GADT can capture the constraint on r that there must exist an instance for Relation r Person Pet. To use a GADT you'll need to add
{-# LANGUAGE GADTs #-}
RelationOf a b will capture the Relation r a b instance in the constructor RelationOf due to the Relation r a b => constraint on the constructor.
data RelationOf a b where
RelationOf :: Relation r a b => r -> RelationOf a b
personPets can then be written much as you desire as
personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att =
case r of (RelationOf r') -> neighbours person r'
where
r :: RelationOf Person Pet
r = case att of
AttachOwns -> RelationOf Owns
AttachDesires -> RelationOf Desires
The case on what was the neighbors person r line is required to get the captured Relation r Person Pet instance from the RelationOf constructor. The instances captured by existentially qualified GADTs can only be recovered by pattern matching against them.
To use a Rank 2 Type, you will need to add one of the following
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE RankNTypes #-}
With a Rank 2 Type, we can split personPets into two parts. The first will figure out what r is, either Owns or Desires, and pass that to a universally quantified function in continuation passing style.
withAttachment :: PetAttachment -> (forall r. Relation r Person Pet => r -> c) -> c
withAttachment AttachOwns f = f Owns
withAttachment AttachDesires f = f Desires
personPets will call withAttachment, passing it a partially applied neighbours as the continuation.
personPets :: Person -> PetAttachment -> Graph -> [Pet]
personPets person att = withAttachment att (neighbours person)