newtype with RankNTypes

Question

If I want to declare a newtype such that type type of the value is constrained to have an instance for a type-class, it seems like I can do that with:

{-# LANGUAGE RankNTypes #-}

newtype ShowBox = ShowBox (forall a. Show a => a)

GHC compiles that just fine, but when I try and actually use ShowBox with

ShowBox "hello"

I get a compiler error

<interactive>:1:18:
    Could not deduce (a ~ [Char])
    from the context (Show a)
      bound by a type expected by the context: Show a => a
      at <interactive>:1:10-24
      `a' is a rigid type variable bound by
          a type expected by the context: Show a => a at <interactive>:1:10
    In the first argument of `ShowBox', namely `"hello"'
    In the expression: ShowBox "hello"
    In an equation for `a': a = ShowBox "hello"

Is there a way to make this work?

Answer 1

You're promising the compiler that the value you put inside a ShowBox will have the type forall a. Show a => a. There's only one possible value with that type, and it's _|_. I think you probably want an existential type, which looks rather similar, but means something very different.

{-# LANGUAGE ExistentialQuantification #-}

data ShowBox = forall a. Show a => ShowBox a

This must be done with data, rather than newtype. Pattern-matching on the constructor is what brings the Show instance into scope, in this case. Since newtypes have no run-time representation, they have no place to store the polymorphic witness the existential quantification implies.

Answer 2

Well, your Show constructor has this type:

Show :: (forall a. Show a => a) -> ShowBox

You're trying to apply this function to type [Char], which is not of type forall a. Show a => a, because the a is a "Skolem variable" that only be unified with another type under very strict rules (which others will be able to explain better than I can).

Are you sure the following is not what you want (modulo data vs. newtype)? Why did you scope the forall inside the constructor?

-- Show :: Show a => a -> ShowBox
data ShowBox = forall a. Show a => Show a