# 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).