Note [Defaulting during simplifyInfer]
When we are inferring a type, we simplify the constraint, and then use
approximateWC to produce a list of candidate constraints. Then we MUST
a) Promote any meta-tyvars that have been floated out by
approximateWC, to restore invariant (WantedInv) described in
Note [TcLevel invariants] in GHC.Tc.Utils.TcType.
b) Default the kind of any meta-tyvars that are not mentioned in
in the environment.
To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
should! If we don't solve the constraint, we'll stupidly quantify over
(C (a->Int)) and, worse, in doing so skolemiseQuantifiedTyVar will quantify over
(b:*) instead of (a:OpenKind), which can lead to disaster; see #7332.
#7641 is a simpler example. References 1
- TcLevel invariants GHC.Tc.Utils.TcType
Referenced by 1
- GHC.Tc.Solver call site