Wincomplete-uni-patterns and bidirectional patterns

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

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

{-# LANGUAGE PatternSynonyms #-}
{-# OPTIONS_GHC -Wincomplete-uni-patterns #-}
import Data.Functor.Identity

newtype T f t = C (f Double)
pattern T :: Double -> T Identity t
pattern T x = C (Identity x)

type R = T Identity ()

divide :: R -> R -> Double
divide x y = x'/y' where
    T x' = x -- pattern match is exhaustive, GHC thinks otherwise.
    T y' = y