Type ambiguity in Haskell type families

Question

I am trying put together the following class Domain and its instance TrivialDomain

{-# LANGUAGE TypeFamilies #-}

data Transition = Transition

class Domain d where
    type Set d
    type Engine d :: * -> *

    top :: Engine d (Set d)

    -- ...
    complement :: Set d -> Engine d (Set d)
    exclude    :: Set d -> Set d -> Engine d (Set d)
    -- ...

data TrivialDomain = TrivialDomain

instance Domain TrivialDomain where
    type Set TrivialDomain = [Int]
    type Engine TrivialDomain = IO

    top = return [0..10]

    -- ...
    complement a = top >>= (flip exclude) a
    exclude a b  = return $ filter (not . (`elem` b)) a
    -- ...

but I keep getting the following error which I fail to understand

test3.hs:25:21:
    Couldn't match type ‘Engine d0’ with ‘IO’
    The type variable ‘d0’ is ambiguous
    Expected type: IO (Set d0)
      Actual type: Engine d0 (Set d0)
    In the first argument of ‘(>>=)’, namely ‘top’
    In the expression: top >>= (flip exclude) a
test3.hs:25:35:
    Couldn't match type ‘Set d1’ with ‘[Int]’
    The type variable ‘d1’ is ambiguous
    Expected type: Set d0 -> [Int] -> IO [Int]
      Actual type: Set d1 -> Set d1 -> Engine d1 (Set d1)
    In the first argument of ‘flip’, namely ‘exclude’
    In the second argument of ‘(>>=)’, namely ‘(flip exclude) a’

I would expect Engine d (Set d) to resolve to IO [Int] in the instance declaration, which does not seem to be the case. At least GHC does not think so. What am I missing?

Answer 1

In your case, associated types aren't enough to infer the types of the methods.

You have class Domain d, and Set and Engine are associated to d. This means that whenever there is a known d in our program with a known Domain d instance, GHC can resolve Set d and Engine d. But this doesn't work backwards. GHC can't resolve d or a Domain instance from the presence of a Set d or an Engine d, since it's entirely possible that there are different Domain instances with the same Set and Engine types.

Since your class methods only mention Set and Engine, Domain d can never be inferred from method use.

You could do a couple of things depending on your goals.

First, you could make d depend on Set and Engine:

class Domain set engine where
  type DomainOf set engine :: *
  -- ...

More generally, FunctionalDependencies gives you much more flexibility to enforce dependencies between types. For example, you can specifically declare that there is only one d for each Set, which is enough to recover good type inference:

class Domain d set engine | d -> set engine, set -> d where

    top        :: engine set
    complement :: set -> engine set
    exclude    :: set -> set -> engine set

data TrivialDomain = TrivialDomain

instance Domain TrivialDomain [Int] IO where

    top = return [0..10]

    complement a = top >>= (flip exclude) a

    exclude a b  = return $ filter (not . (`elem` b)) a

Finally, if you want to use your original class, you have to add Proxy d parameters to your methods, in order to make the instance and the associated types resolvable:

import Data.Proxy

data Transition = Transition

class Domain d where
    type Set d
    type Engine d :: * -> *

    top        :: Proxy d -> Engine d (Set d)
    complement :: Proxy d -> Set d -> Engine d (Set d)
    exclude    :: Proxy d -> Set d -> Set d -> Engine d (Set d)

data TrivialDomain = TrivialDomain

instance Domain TrivialDomain where
    type Set TrivialDomain = [Int]
    type Engine TrivialDomain = IO

    top _ = return [0..10]

    complement d a = top d >>= (flip (exclude d)) a
    exclude d a b  = return $ filter (not . (`elem` b)) a

Here, the purpose of Proxy d is to specify exactly which instance you want to use.

However, this means we have to write top (Proxy :: Proxy d) on each method usage (similarly with other methods), which is rather onerous. With GHC 8 we can omit Proxys and use TypeApplications instead:

{-# language TypeApplications, TypeFamilies #-}

-- ...

instance Domain TrivialDomain where
    type Set TrivialDomain = [Int]
    type Engine TrivialDomain = IO

    top = return [0..10]

    complement a = top @TrivialDomain >>= (flip (exclude @TrivialDomain)) a
    exclude a b = return $ filter (not . (`elem` b)) a