PmCheck: Unsoundness in provideEvidence

In #18609 (closed), I first realised that provideEvidence is slightly unsound. Consider

{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeOperators #-}

module Lib where

import Data.Type.Equality

data T a where
  TInt :: T Int
  TBool :: T Bool

f :: T a -> a :~: Int -> ()
f TInt Refl = ()

This currently compiles without warnings, despite the fact that f TBool undefined results in a crash in GHCi.

The problem is that in provideEvidence, we consider all match variables as unlifted. Building on !3633 (merged) we could do better, by "instantiating" to a wildcard if we could not find any constructors to instantiate to and ⊥ is still possible.

I expect that change to dig up some test cases in which we are then too imprecise, but we can take care of them afterwards.