decideMonoTyVars should take injectivity into account

Suppose I have

{-# LANGUAGE TypeFamilies #-}
module Bug where

type family F a

inject :: a -> F a
inject = undefined

x = 5

f y = [inject y, x]

Important: the monomorphism restriction (MR) is in effect.

When inferring the type of f at level 1, we have

x :: alpha[0]
[W] Num alpha[0]

y :: beta[1]
f :: beta[1] -> [alpha[0]]
[W] F beta[1] ~ alpha[0]

We now must decide what type to infer for f. GHC proceeds first by deciding the so-called mono tyvars (decideMonoTyVars). This works by taking all the type variables free in the environment (alpha[0], in our case) and looking for any type variables used in an equality constraint with them. Because beta[1] is indeed in an equality constraint with alpha[0], beta[1] is labeled as monomorphic, and thus is promoted to beta[0]. GHC then falls over because it won't default alpha[0] with the constraint F beta[0] ~ alpha[0] around, as that disrupts the rules for defaulting.

Instead, GHC should not label beta[1] as mono, because its appearance in the constraint is not an injective appearance.

I will fix in !5899 (closed).