- go (ForAllTy tv t_ty) b_tvs b_ty = go t_ty b_tvs b_ty -- Rule S-SPEC
- go t_ty b_tvs (ForAllTy tv b_ty) = go t_ty b_tvs' b_ty -- Rule S-SKOL
- where b_tvs' = extendVarSet b_tvs tv
+ go t_tvs t_ty b_tvs b_ty
+ | isSigmaTy t_ty, (tvs, _, t_tau) <- tcSplitSigmaTy t_ty
+ = go (t_tvs `delVarSetList` tvs) t_tau b_tvs b_ty -- Rule S-SPEC
+ -- Under a forall on the left, if there is shadowing,
+ -- do not bind! Hence the delVarSetList.
+ | isSigmaTy b_ty, (tvs, _, b_tau) <- tcSplitSigmaTy b_ty
+ = go t_tvs t_ty (extendVarSetList b_tvs tvs) b_tau -- Rule S-SKOL
+ -- Add to the variables we must not bind to
+ -- NB: it's *important* to discard the theta part. Otherwise
+ -- consider (forall a. Eq a => a -> b) ~<~ (Int -> Int -> Bool)
+ -- and end up with a completely bogus binding (b |-> Bool), by lining
+ -- up the (Eq a) with the Int, whereas it should be (b |-> (Int->Bool)).
+ -- This pre-subsumption stuff can return too few bindings, but it
+ -- must *never* return bogus info.