How to write `HasC` as a newtype with a pattern synonym.

HasC.hs

{-# LANGUAGE GHC2021, RoleAnnotations, DeriveAnyClass #-}
{-# LANGUAGE UnboxedTuples, PatternSynonyms, ViewPatterns #-}

{- |
This module implements (for empty 'C'):

> data HasC a where
>   HasC :: C a => !a -> HasC a

as an opaque newtype with a pattern synonym.
-}
module HasC (
  C,
  HasC(HasC),
) where

import Unsafe.Coerce (unsafeCoerce)

data Dict c = c => Dict


class C a

type role HasC nominal
newtype HasC a = UnsafeHasC{ extract :: a }

dict :: HasC a -> Dict (C a)
dict !_ = unsafeCoerce (Dict @())
--   ^ Necessary for soundness!
-- In particular, `_shouldExplode2` fails without it.

view :: HasC a -> (# Dict (C a), a #)
view x = (# dict x, extract x #)

{-# COMPLETE HasC #-}
pattern HasC :: () => C a => a -> HasC a
pattern HasC x <- (view -> (# Dict, x #))
  where HasC x = UnsafeHasC x


_shouldCompile :: HasC a -> Dict (C a)
_shouldCompile (HasC _) = Dict
-- does

-- _shouldn't :: a -> HasC a
-- _shouldn't x = HasC x
-- doesn't

data Foo deriving C

_shouldExplode1, _shouldExplode2 :: ()
_shouldExplode1 = HasC (undefined :: Foo) `seq` ()
_shouldExplode2 = case undefined :: HasC Foo of HasC _ -> ()
-- both do