What is the assumption made in "Learn You a Haskell" when deducing the kind?

Question

This question is not subjective. A very specific verb is used in the referenced book, and I'd like to understand what the implication of that phrasing is, because I'm afraid I'm misunderstanding something.

From Learn You a Haskell, the following paragraph is the third and last one containing "we assume *".

data Barry t k p = Barry { yabba :: p, dabba :: t k }  

And now we want to make it an instance of Functor. Functor wants types of kind * -> * but Barry doesn't look like it has that kind. What is the kind of Barry? Well, we see it takes three type parameters, so it's going to be something -> something -> something -> *. It's safe to say that p is a concrete type and thus has a kind of *. For k, we assume * and so by extension, t has a kind of * -> *. Now let's just replace those kinds with the somethings that we used as placeholders and we see it has a kind of (* -> *) -> * -> * -> *.

Why are we assuming anything at all? Upon reading "we assume X (i.e. we assume that X is true)" it is natural for me to think that we should also consider the case that X is false. In the specific case of the example, couldn't t be of kind (* -> *) -> * and k of kind (* -> *)? If this was the case, whatever t and k actually were, t k would still be a concrete type, no?

I see that the whole line of reasoning is then checked against the compiler, but I don't think the compiler assumes. If it does, I'd like to know what, if it doesn't then again I'm afraid I'm missing the meaning of the paragraph.

Answer 1

In fact, the compiler does assume! But you can ask it not to with the PolyKinds extension. You can read about it in more detail here. With that extension turned on, the kind of Barry will be forall k. (k -> *) -> k -> * -> *.