PatternSynonyms on data family and COMPLETE signature lead to incorrect warning
Note that the original test case below is fixed in !1903 (closed). There's a more obscure test case in #17207 (comment 227180), that's why this ticket is still open.
Here's a whitebox test I came up with that shouldn't produce any warnings:
{-# OPTIONS_GHC -Wincomplete-patterns -Wno-missing-methods -fforce-recomp #-}
{-# LANGUAGE GADTs, TypeFamilies, PatternSynonyms #-}
module Lib where
data family T a
data instance T () where
A :: T ()
B :: T ()
pattern C :: T ()
pattern C = B
{-# COMPLETE A, C #-}
g :: T () -> ()
g A = ()
g C = ()
h :: T () -> ()
h C = ()
h A = ()
Yet it currently (after !963 (closed)) produces the following warning:
testcases/LateInitOfShapes.hs:16:1: warning: [-Wincomplete-patterns]
Pattern match(es) are non-exhaustive
In an equation for ‘g’: Patterns not matched: B
|
16 | g A = ()
| ^^^^^^^^...
This is loosely related to the observation in #14059 (comment 140372): The first match of g
commits the type of the value abstraction to the representation TyCon of T ()
, at which point we don't see the COMPLETE set that is attached to the family T
. To my knowledge there is no way to get back to T ()
from the representation TyCon (Edit: yes, there is. tyConFamInst_maybe
, which !1903 (closed) does), so the only way to recover this would be to make sense of the CoPat
surrounding the match on A
. There was a ticket where we discussed how to adding a CoPat
variant to PmPat
, but I couldn't find it. It's #14899 (closed), but I no longer think the CoPat
idea is relevant.