How do I understand the set of valid inputs to a Haskell type constructor?

Question

Warning: very beginner question.

I'm currently mired in the section on algebraic types in the Haskell book I'm reading, and I've come across the following example:

data Id a =
  MkId a deriving (Eq, Show)

idInt :: Id Integer
idInt = MkId 10

idIdentity :: Id (a -> a)
idIdentity = MkId $ \x -> x

OK, hold on. I don't fully understand the idIdentity example. The explanation in the book is that:

This is a little odd. The type Id takes an argument and the data constructor MkId takes an argument of the corresponding polymorphic type. So, in order to have a value of type Id Integer, we need to apply a -> Id a to an Integer value. This binds the a type variable to Integer and applies away the (->) in the type constructor, giving us Id Integer. We can also construct a MkId value that is an identity function by binding the a to a polymorphic function in both the type and the term level.

But wait. Why only fully polymorphic functions? My previous understanding was that a can be any type. But apparently constrained polymorphic type doesn't work: (Num a) => a -> a won't work here, and the GHC error suggests that only completely polymorphic types or "qualified types" (not sure what those are) are valid:

f :: (Num a) => a -> a
f = undefined

idConsPoly :: Id (Num a) => a -> a
idConsPoly = MkId undefined

Illegal polymorphic or qualified type: Num a => a -> a
Perhaps you intended to use ImpredicativeTypes
In the type signature for ‘idIdentity’:
  idIdentity :: Id (Num a => a -> a)

EDIT: I'm a bonehead. I wrote the type signature below incorrectly, as pointed out by @chepner in his answer below. This also resolves my confusion in the next sentence below...

In retrospect, this behavior makes sense because I haven't defined a Num instance for Id. But then what explains me being able to apply a type like Integer in idInt :: Id Integer?

So in generality, I guess my question is: What specifically is the set of valid inputs to type constructors? Only fully polymorphic types? What are "qualified types" then? Etc...

Answer 1

You just have the type constructor in the wrong place. The following is fine:

idConsPoly :: Num a => Id (a -> a)
idConsPoly = MkId undefined

---

The type constructor Id here has kind * -> *, which means you can give it any value that has kind * (which includes all "ordinary" types) and returns a new value of kind *. In general, you are more concerned with arrow-kinded functions(?), of which type constructors are just one example.

TypeProd is a ternary type constructor whose first two arguments have kind * -> *:

-- Based on :*: from Control.Compose
newtype TypeProd f g a = Prod { unProd :: (f a, g a) }

Either Int is an expression whose value has kind * -> * but is not a type constructor, being the partial application of the type constructor Either to the nullary type constructor Int.

Answer 2

Also contributing to your confusion is that you've misinterpreted the error message from GHC. It means "Num a => a -> a is a polymorphic or qualified type, and therefore illegal (in this context)".

The last sentence that you quoted from the book is not very well worded, and maybe contributed to that misunderstanding. It's important to realize that in Id (a -> a) the argument a -> a is not a polymorphic type, but just an ordinary type that happens to mention a type variable. The thing which is polymorphic is idIdentity, which can have the type Id (a -> a) for any type a.

In standard Haskell polymorphism and qualification can only appear at the outermost level of the type in a type signature.

Answer 3

The type signature is almost correct

idConsPoly :: (Num a) => Id (a -> a)

Should be right, though i have no ghc on my phone to test this. _{Also i think your question is quite broad, thus i deliberately answer only the concrete problem here.}