I’ve got a GADT, say something like this:
type data P1 = P1A | P1B | ...
type data P2 = P2A | P2B | ...
type data P3 = P3A | P3B | ...
data T (a :: P1) (b :: P2) (c :: P3) where
SomeCon1 :: ... -> T a b c
SomeCon2 :: ... -> T P1A b c
SomeCon3 :: ... -> T a P2b c
...
The nice thing is that the GHC exhaustive checker does a great job at checking whether I’ve missed a constructor on a pattern match, like if I’ve got a function that takes T P1B b c
, then I don’t have to match against SomeCon2
.
But, whilst I want to expose all these constructors for pattern matching, I want to hide (at least some of them) from being used directly, as there are some invariants I want to maintain.
I guess one way to do this would be to hide all the constructors in exchange for pattern synonyms, being unidirectional or bidirectional as appropriate, perhaps in combination with some smart constructors.
I’d be happy to do this, but the only issue is that the only way I know to have exhaustiveness checking on pattern synonyms is {-# COMPLETE #-}
pragmas.
The only way around this I can think of is have a separate set of pattern synonyms with a particular complete pattern for each combination of P1
, P2
and P3
. Not only is this very messy, but I don’t think even works, because it doesn’t cover the cases where P1
, P2
or P3
are free.
I don’t mind making smart constructors for everything, and ONLY using the defined constructors for pattern matching NOT creation.
But, is there a way to expose constructors ONLY for pattern matching and not for creation? So I can get the goodness of GADT pattern matching whilst still being able to enforce the required invariants? Or is there any other way to achieve what I’m looking for?