Haskell type inference with GADTs and typeclass constraints on type variables

Question

I defined a custom GADT where the type constructor has a type class constraint on the type variable, like this:

data MyGadt x where
  Sample :: Show a => a -> MyGadt a

Now, if I define the following two functions:

foo (Sample a) = show a

bar a = Sample a

GHC infers types for them that are a bit irritating to me. foo :: MyGadt x -> [Char] doesn't mention the Show constraint for x, while bar :: Show a => a -> MyGadt a does require the constraint to be mentioned explicitly.

I was assuming that I don't have to mention the constraint because it is declared in the GADT definition. The only thing I can think of being part of the reason is the position of the GADT in the function. I'm not super deep into that but as far as I understand it, MyGadt is in positive position in foo and in negative position in bar.

When do I have to mention the type class constraints explicitly, and when does GHC figure it out itself based on the constraint on the GADTs type constructor?

Constraints must be provided by the context on construction, and are instead added to the context on pattern matching. I don't understand the source of your confusion. Try pretending that constraints are just another argument to the constructor e.g. Sample :: ShowDict a -> a -> MyGadt a: you have to pass the extra argument on construction, and you get that value back on pattern matching. Constraints work in exactly the same way. — chi
bar :: a -> MyGadt a claims that you can construct MyGadt T regardless of T, even if T is not in Show, but that’s not true because Sample requires a Show instance. Whereas bar :: Show a => a -> MyGadt a explicitly specifies that bar @T requires T to be in Show. — Jon Purdy

leftaroundabout leftaroundabout · Accepted Answer · 2021-07-26T11:48:41

It's the whole point of using a GADT that you want the constraint to show up in the signature of bar, instead of foo. If you don't want that, then you can use a plain old newtype instead:

newtype MyAdt = Sample a

foo :: Show a => MyAdt a -> String
foo (Sample a) = show a

bar :: a -> MyAdt a
bar = Sample

Having the constraint in neither foo nor bar clearly can't work, because then you would be able to e.g.

showFunction :: (Integer -> Integer) -> String
showFunction = foo . bar

Haskell type inference with GADTs and typeclass constraints on type variables

1 Answers