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)
where
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.
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.
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.