Wingman uses dataConCannotMatch from GHC to check when it should filter out GADT data cons. But dataConCannotMatch only checks if two type indices certainly can't match. But if one of them is a skolem, GHC doesn't know this, and thinks it's merely a type variable. In which case, it could match, but we know better.