RankNTypes and pattern matching

Question

Is there a way in haskell to erase type information/downcast to a polymorphic value ?

In the example I have a boxed type T which can contain either an Int or a Char And I want to write a function which extract this value without knowing which type it is.

{#- LANGUAGE RankNTypes -#}

data T = I Int | C Char

-- This is not working because GHC cannot bind "a"
-- with specific type Int and Char at the same time. 
-- I just want a polymorphic value back ;(
getValue :: T -> (forall a. a)
getValue (I val) = val
getValue (C val) = val

-- This on the other hand works, because the function
-- is local to the pattern matching expression
onValue :: T -> (forall a. a -> a) -> T
onValue (I val) f = I $ f val 
onValue (C val) f = C $ f val

Is there a way to write a function that can extract this value without forcing a type at the end ?

a getValue function like the first one ?

Let me know if it is not clear enough.

Answer

So the question was stupid as AndrewC (in the comment) and YellPika pointed out. An infinite type has no meaning.

J. Abrahamson provides an explanation for what I am looking for, so I put his answer as the solution.

P.S: I do not want to use GADT as I do not want a new type each time.

Answer 1

What you probably want is not to return a value (forall a . a) as it is wrong on several fronts. For one, you do not have any value but instead just one of two. For two, such a type cannot exist in a well-behaved program: it corresponds to the type of infinite loops and exceptions, e.g. bottom.

Finally, such a type allows the person who owns it to make the choice to instantiate it more concretely. Since you're giving it to the caller of your function that means that they would get to choose which of an Int or Char you had. Clearly that doesn't make sense.

Instead, what you most likely want is to make a demand of the user of your function: "you have to work regardless of what this type is".

foo :: (forall a . a -> r) -> (T -> r)
foo f (I i) = f i
foo f (C c) = f c

You'll find this function to be really similar to the following

bar :: r -> T -> r
bar x (I _) = x
bar x (C _) = x

In other words, if you force the consumer of your function to disregard all type information then, well, actually nothing at all remains: e.g. a constant function.

Answer 2

If you turn on ExistentialTypes, you can write:

data Anything = forall a. Anything a

getValue :: T -> Anything
getValue (I val) = Anything val
getValue (C val) = Anything val

However, this is pretty useless. Say we pattern match on an Anything:

doSomethingWith (Anything x) = ?

We don't know anything about x other than that it exists... (well, not even - it might be undefined). There's no type information, so we can't do anything with it.

Answer 3

You can use GADTs:

{-# LANGUAGE GADTs #-}

data T a where
    I :: Int -> T Int
    C :: Char -> T Char

getValue :: T a -> a
getValue (I i) = i
getValue (C c) = c