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