GHC fails to quantify over a quantifiable equality constraint
Consider
{-# LANGUAGE TypeFamilies, NoMonoLocalBinds #-}
module NoMonoLocal where
type family F a
inject :: a -> F a
inject = undefined
f x = let g y = [x, inject y] in (g 'x', g True)
I think this should work, but GHC rejects, failing to infer a polymorphic type for g
.
(Red herring: NoMonoLocalBinds
. If it helps, imagine the declaration for F
to occur in another module. The definition for f
does not require -XTypeFamilies
or -XMonoLocalBinds
to be enabled.)
The problem is in inferring the type of g
. Suppose x :: alpha[1]
and y :: beta[2]
. We get
[W] F beta[2] ~ alpha[1]
I would expect, then, for GHC to infer g :: forall b. (F b ~ a) => b -> [a]
, where a
is the type of x
(from an outer scope). Note that GHC does allow quantification over equalities of this shape.
The problem is that the touchabilityTest
, when looking at that Wanted, concludes TouchableOuterLevel
: that is, GHC wants to say alpha[1] := F beta[2]
. Of course, this violates the level invariant, and so GHC promotes beta[2]
to beta'[1]
first (and then unifies). When it comes around to deciding the quantified type variables for g
, beta'[1]
is now at an outer level and is not quantified. It eventually gets monomorphised to Char
-- not what we want.
I think touchabilityTest
should not try to unify variables from outer levels when the RHS has an inner level.
Interestingly, even if this immediate bug is fixed, GHC will still reject, because of #20668 (closed). So perhaps it makes sense to hold off here until #20668 (closed) is fixed, but I claim this is a separable problem.