Constructing concrete types for typeclasses with GADTs

The inspiration for this is creating a list of values that are instances of Show. I found the following snippet that uses GADTs to create a concrete Showable type.

data Showable where Showable :: Show a => a -> Showable

instance Show Showable where
    show (Showable x) = show x

list :: [Showable]
list = [Showable 4, Showable "hello", Showable 'a']

Then, I tried to make Showable more general by creating a type that could make any typeclass concrete.

data Concrete a where Concrete :: a b => b -> Concrete a

instance Show (Concrete Show) where
    show (Concrete x) = show x

list :: [Concrete Show]
list = [Concrete 4, Concrete "hello", Concrete 'a']

This works with the ConstraintKinds and FlexibleInstances language extensions, but in order to use Concrete to make concrete types for other typeclasses, each one would require a new instance.

Is there a way to create something similar to Concrete such that, for example, Concrete Show is automatically an instance of Show?

Solution

It is not possible. Consider this:

instance Monoid (Concrete Monoid) where
   mappend (Concrete x) (Concrete y) = Concrete (mappend x y) -- type error!

This is a type error since x and y come from two different existential quantifications. There is no guarantee that x and y can be added together.

In other words, [Concrete [1,2], Concrete ["hello"]] has type [Concrete Monoid] but can not be summed (mconcat).

This is precisely the same problem for which, in OOP, the following base class/interface does not work:

interface Vector {
   Vector scale(double x);
   Vector add(Vector v);
}
class Vec2D implements Vector { ... }
class Vec3D implements Vector { ... }

The interface implies that a 2D vector is addable to any other vector, including a 3D one, which makes no sense. For an OOP solution, see F-bounded quantification and its related popularization callled curiously recurring template pattern.

In Haskell, we often do not need such techniques since there is no subtyping, hence two types in, say, a Vector type class are already not mixable.

class Vector a where
   scale :: Double -> a -> a
   add :: a -> a -> a
instance Vector (Vec2D) where ...
instance Vector (Vec3D) where ...