Writing COMPLETE pragma for polymorphic pattern synonyms

I have arrived at this approach of making handling of nested Either's more elegant; it uses pattern synonyms to allow case'ing directly on the inner Either values.

type (:+:) = Either

class a :<: b where
  inj :: a -> b
  pick :: b -> Maybe a

instance a :<: (a :+: b) where
  inj = Left
  pick = either Just (const Nothing)

instance b :<: (a :+: b) where
  inj = Right
  pick = either (const Nothing) Just

instance {-# OVERLAPPABLE #-} a :<: c => a :<: (c :+: b) where
  inj = Left . inj
  pick = either pick (const Nothing)

pattern Member :: x :<: c => x -> c
pattern Member {thing} <-
  (pick -> Just thing)
    Member = inj

type Stuff = Int :+: String :+: Char :+: Text

mkStuff :: Stuff
mkStuff = Member @Int 42

useStuff :: Stuff -> String
useStuff = \case
  Member s -> s
  Member (n :: Int) -> "The number: " <> show n
  Member (c :: Char) -> [c]
  Member (t :: Text) -> toString t

GHC however complains of non-exhaustive patterns:

Foo.hs:(110,12)-(114,34): warning: [-Wincomplete-patterns]
    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: _
110 | useStuff = \case
    |            ^^^^^...

But how would one write a COMPLETE pragma for this polymorphic pattern synonym?

I don’t know how it works, but using {-# COMPLETE Member :: Either #-} will suppress this warning entirely, and will not complain even if there are in fact non-exhaustive patterns. Obviously that’s not ideal.

1 Like

I have been hoping that there would be some way to make this work, but after reading this ghc-devs thread that hope has diminished.

1 Like

Yeah, unfortunately COMPLETE pragmas are attached to a data (family) type constructor, so there is no way to get what you want. Every type that is an instance of :<: will have to write its own {-# COMPLETE Member :: MyType #-} declaration.

There is no conceptual reason (I think) why we couldn’t support COMPLETE pragmas on polymorphic types. It’s just that it was more convenient to attach them to data type constructors and it’s easier to look them up this way. I imagine that someone who really wants this will put in enough elbow grease to make this happen.

And for the record, https://gitlab.haskell.org/ghc/ghc/issues/14422 is the GHC ticket that discusses this.

I actually tried doing this, but couldn’t figure it out (it seems like one can’t put arbitrary type expressions in place of MyType?). How would one declare COMPLETE pragma for the above Stuff type?

it seems like one can’t put arbitrary type expressions in place of MyType ?

Yes, exactly. That’s what I meant by " COMPLETE pragmas are attached to a data (family) type constructor". Unfortunately, this includes type synonyms and type families.
And as far as GHC is concerned, it will normalise type synonyms and type families before attempting to look up the COMPLETE set. So it will try to look up the COMPLETE set for :+:, which is just Either, which explains why your approach works.

Although that’s rather lying to the compiler; f :: Int :+: Bool -> (); f (Member (n :: Int)) = () will certainly crash for f (Right False), so your COMPLETE declaration is quite dubious. See also https://gitlab.haskell.org/ghc/ghc/issues/11224.