Dear Cafe, I have a data type with a bidirectional pattern {-# LANGUAGE PatternSynonyms #-} newtype T f t = C (f Double) pattern T :: Double -> T Identity t pattern T x = C (Identity x) Note that pattern T is the only way to construct something of type (T Identity t) for any phantom parameter t. When using the pattern to match in a where clause, the Wincomplete-uni-pattern warns me about non-exhaustive pattern matches that are in fact matched: f a = x where T x = g a :: T Identity () warning: [-Wincomplete-uni-patterns] Pattern match(es) are non- exhaustive in a pattern binding: Patterns not matched: C (Identity _) Minimal complete example is attached. How can I teach GHC 9 that the pattern is indeed exhaustive? GHC seems to have only three issues involving incomplete-uni-patterns, only one of them open, none of which matches my observations. Thanks Olaf