Does <- implicitly coerce types in a Haskell do block?

Question

My question relates to the answer to another question: https://stackoverflow.com/a/11766789/3212958

In his answer, ertes writes the following type signature

select :: [a] -> [(a, [a])]

However, when select is actually used, ertes writes the following inside of a do block

(y, ys) <- select xs

Please help me shed some light on how the tuple (y, ys) matches the return type of select, namely [(a, [a])]. Is Haskell coercing the types at some point? (Does Haskell ever coerce types?) Is <- extracting a tuple of type (a, [a]) from the list monad that select returns?

Thanks, Max

--- EDIT: ---

@Lee reminds newbs to desugar before trying to reason about types. After making >>= explicit, it's more clear what's going on. After desugaring, the function in question looks like:

select xs >>= \(y, ys) -> fmap (y:) (perms (n - 1) ys)

And for lists, xs >>= f = concat (map f xs). So a better reading of (y, ys) in this context is as the signature of the function to map over the list.

Answer 1

In do notation,

do x1 <- action1
   action2

is translated into action1 >>= \x1 -> action2

This means that if action1 has type m a for some monad m, then x1 has type a. It's not really coercing types, but rather 'unpacking' the value from the monadic action action1 and binding it to x1.

Answer 2

(y, ys) is of type (b, c)

The return type of select is of type [(a, [a])]

In <- the types are actually d and Monad m => m d. So we can write the following type equalities:

(b, c) ~ d
[(a, [a])] ~ Monad m => m d

Solving is easy. First substitute d from first equation into second equation:

[(a, [a])] ~ Monad m => m (b, c)

Now to see what's going on I will use a prefix form of [] type constructor (it's not valid haskell but you should get the idea):

[] (a, [a]) ~ Monad m => m ( b, c)

So

m ~ []
(a, [a]) ~ (b, c)

At this point the compiler checks that instance Monad [a] exists. The rest is easy:

a ~ b
[a] ~ c