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?

Does this quantification mean what you think it means? I'm really not sure, myself. I'm thinking it may mean that ShowBox can only be applied to values that are precisely of type Show a => a. I am quite interested to see what is the answer to this question. — Daniel Pratt

Carl Carl · Accepted Answer · 2012-03-19T23:38:44

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.

newtype with RankNTypes

2 Answers