Note [Do not unify Givens]
Consider this GADT match
data T a where
T1 :: T Int
...
f x = case x of
T1 -> True
...
So we get f :: T alpha[1] -> beta[1]
x :: T alpha[1]
and from the T1 branch we get the implication
forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool
Now, clearly we don't want to unify alpha:=Int! Yet at the moment we
process [G] alpha[1] ~ Int, we don't have any given-equalities in the
inert set, and hence there are no given equalities to make alpha untouchable.
NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that
never happens: invariant (GivenInv) in Note [TcLevel invariants]
in GHC.Tc.Utils.TcType.
Simple solution: never unify in Givens! References 1
- TcLevel invariants GHC.Tc.Utils.TcType
Referenced by 1
- GHC.Tc.Solver.Equality call site