Invalid pattern-match warnings related to strictness
Here are three function definitions that shouldn't generate a pattern-match warning:
{-# OPTIONS_GHC -Wincomplete-patterns -fforce-recomp #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyCase #-}
module Lib where
import Data.Type.Equality
import Data.Functor.Identity
import Data.Void
f :: a :~: Int -> a :~: Bool -> ()
f !_ x = case x of {}
g :: Identity (a :~: Int) -> a :~: Bool -> ()
g (Identity _) Refl = ()
data SMaybe a = SNothing
| SJust !a
-- | Exhaustive. Note how in addition to @{(a,b) | b /~ True}@, the value set
-- @{(a,b) | y /~ SNothing, b ~ True}@ flows into the next equation, but @y@ is
-- no longer in scope. Normally, we have no way of matching on that without a
-- wildcard match, but in this case we refute @y ~ SJust z@ by unleashing type
-- evidence saying that @z@ must be 'Void' by matching on 'Void'.
h :: forall a. a :~: Void -> Bool -> ()
h _ True | let y = undefined :: SMaybe a, SNothing <- y = ()
h Refl False = ()
Here's the current output:
test.hs:18:1: warning: [-Woverlapping-patterns]
Pattern match has inaccessible right hand side
In an equation for ‘g’: g (Identity _) Refl = ...
|
18 | g (Identity _) Refl = ()
| ^^^^^^^^^^^^^^^^^^^^^^^^
I think we can properly solve this after #17248 (closed) (strictness of newtypes) and #17215 (long distance info) is settled. (Note that even with !1975 (closed), which fixes #17248 (closed), g
generates a warning, because we assume that there's a non-void constraint on every variable we have facts about in the oracle.)