GADT confusion with custom data types?

Question

I have the following custom data types:

data FirstPair' a b = FirstPair a b deriving (Show, Ord, Eq)
type FirstPair a = FirstPair' a a 

data SecondPair' a b = SecondPair a b deriving (Show, Ord, Eq)
type SecondPair a = SecondPair' a a

I'm trying to create a GADT structure for my function:

data Generator a where
  Success :: FirstPair a -> Generator (SecondPair a)
  Fail :: FirstPair a -> Generator Bool

myFunction :: Generator a -> a
myFunction (Success fp) = SecondPair "21" "24"
myFunction (Fail fp) = False

The role of 'Generator' type is to enable me to force 'myFunction' to return an instance of 'SecondPair' if 'Success' is passed to it, and 'False' if 'Fail' is passed to it.

However, I'm getting this error:

"Could not deduce: a1 ~ [Char] from the context: a ~ SecondPair' a1 a1 bound by a pattern with constructor: Success :: forall a. FirstPair a -> Generator (SecondPair a)"

What am I doing wrong here?

It looks like your question is missing some code. Your error references ContextaPair', but you don't mention that. Can you post your actual code? — crockeea
You still aren't running the same code that you've posted. There are no [Char] values in your code. — chepner

luqui luqui · Accepted Answer · 2016-11-06T23:10:04

myFunction :: Generator a -> a
myFunction (Success fp) = SecondPair "21" "24"
myFunction (Fail fp) = False

The problem is here. The type signature is shorthand for

myFunction :: forall a. Generator a -> a

That is, no matter what type a I pick, if I give myFunction a Generator a, it will give me back an a. So if I gave it a Generator Int, it should give me back an Int.

So I can construct

successval :: Generator (SecondPair Int)
successval = Success (FirstPair 42 42 :: FirstPair Int)

And then pass it to myFunction, and according to the type signature I should get

myFunction successVal :: SecondPair Int

However, the way myFunction is defined, it will always give back a SecondPair String no matter what type I pass it, and that's the problem it's complaining about.

You need to somehow use the argument you are given if you want this kind of polymorphism. E.g.

myFunction (Success (FirstPair x y)) = SecondPair x y

would do the trick, because the x and y going out are the same type as the x and y coming in (and FirstPair and SecondPair match the way the GADT says they should).

If you need to return a SecondPair String no matter what, then either myFunction's type signature is wrong, needing to be something like

 myFunction :: Generator a -> SecondPair String

(which doesn't act correctly in the case of Fail -- I have more to say if this is the route you actually want to go, but it's a bit more involved than I want to write for a shot-in-the-dark guess)

or the GADT needs to say that the result will be a SecondPair String.

 data Generator a where
     Success :: FirstPair a -> Generator (SecondPair String)
     ...

I don't think these are terribly likely scenarios, I just thought they might help your understanding of the problem.

GADT confusion with custom data types?

1 Answers