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.