Skip to content

Instantly share code, notes, and snippets.

@LSLeary
Last active January 15, 2025 02:35
Show Gist options
  • Save LSLeary/ef0f75468938fa6ff505331171bb011c to your computer and use it in GitHub Desktop.
Save LSLeary/ef0f75468938fa6ff505331171bb011c to your computer and use it in GitHub Desktop.
How to write `HasC` as a newtype with a pattern synonym.
{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment