Understanding type constraints

Question

My particular problem may have something to do with existential types but I'm not sure so I won't put it in the title.

Anyways, here's what I'm trying to do.

Have an Entity type that wraps over a heterogeneous list of components. Then, I have a HasComponent a b typeclass that denotes that the list b has a component of the type a. Here's how I've written it, and the classes instances.

data Entity c = Entity c

data CompNode c n = CompNode c n
data CompEnd = CompEnd

class HasComponent a b where
    getComponent :: b -> a

instance HasComponent a (CompNode a n) where
    getComponent (CompNode a _) = a

instance HasComponent a n => HasComponent a (CompNode b n) where
    getComponent (CompNode _ n) = getComponent n

instance HasComponent a b => HasComponent a (Entity b) where
    getComponent (Entity b) = getComponent b

There's also a HasComponent instance for Entity. That's just for convenience.

So far, everything compiles.

Now, I'd like to try this out. I've made a DisplayData a type that holds some data of type a that's meant to be displayed. This is one of the components. Then I've made Displayer a that is a wrapper around a function of the type a -> IO (). This component is meant to provide a way to show the data.

data DisplayData a = DisplayData a
data Displayer a = Displayer (a -> IO ())

Now these two components should play nicely together. I wanted to write a function display that takes an Entity that satisfies some constraints and displays it.

This is my attempt

display :: (HasComponent (DisplayData a) c, HasComponent (Displayer a) c) => Entity c -> IO ()
display e = f a
    where Displayer f = getComponent e :: Displayer a
          DisplayData a = getComponent e :: DisplayData a

What I would like this to mean is: "If there exists some type a such that (HasComponent (DisplayData a) c, HasComponent (Displayer a) c) is true, then display can take an Entity c and produce an IO action."

What I think this might mean instead is: "If (HasComponent (DisplayData a) c, HasComponent (Displayer a) c) is true for any and every type a, then display can take an Entity c and produce an IO action.

The error I get is this

Could not deduce (HasComponent (DisplayData a0) c)
  arising from the ambiguity check for `display'
from the context (HasComponent (DisplayData a) c,
                  HasComponent (Displayer a) c)
  bound by the type signature for
             display :: (HasComponent (DisplayData a) c,
                         HasComponent (Displayer a) c) =>
                        Entity c -> IO ()
  at Components.hs:24:12-94
The type variable `a0' is ambiguous
In the ambiguity check for:
  forall c a.
  (HasComponent (DisplayData a) c, HasComponent (Displayer a) c) =>
  Entity c -> IO ()
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for `display':
  display :: (HasComponent (DisplayData a) c,
              HasComponent (Displayer a) c) =>
             Entity c -> IO ()

How do I do what I want here?

Answer 1

First of all, to reference type variables in the type signature from the body of the function, you need to enable ScopedTypeVariables, and add a forall to the type:

{-# LANGUAGE ScopedTypeVariables #-}

display :: forall a c . (HasComponent (DisplayData a) c, HasComponent (Displayer a) c) 
        => Entity c -> IO ()
display e = f a
    where 
      Displayer f = getComponent e :: Displayer a
      DisplayData a = getComponent e :: DisplayData a

But this will still produce an error. The issue is that the type a is only mentioned in the context, not the actual type. There will be no way for the compiler to ever instantiate this type. You have several options.

You can add a "dummy" parameter which contains that type:

display :: forall a c proxy . 
             (HasComponent (DisplayData a) c, HasComponent (Displayer a) c) 
        => proxy a -> Entity c -> IO ()
display _ e = f a where ...

Or, you can add a functional dependency to your class, and some pragmas:

{-# LANGUAGE OverlappingInstances, UndecidableInstances #-}

class HasComponent a b | b -> a where

which says that the type a is determined by the type b. In this case, the first form will compile.