DataKind Unions
This is getting kind of awful, but I guess you could require a proof that it's either a circle or a square using Data.Type.Equality
:
test1 :: Either (s :~: Circle') (s :~: Square') -> Shape s -> Int
Now the user has to give an extra argument (a "proof term") saying which one it is.
In fact you can use the proof term idea to "complete" bradm's solution, with:
class MyOpClass sh where
myOp :: Shape sh -> Int
shapeConstraint :: Either (sh :~: Circle') (sh :~: Square')
Now nobody can go adding any more instances (unless they use undefined
, which would be impolite).
You can accomplish something like this in (I think) a reasonably clean way using a type family together with ConstraintKinds
and PolyKinds
:
type family Union (a :: [k]) (r :: k) :: Constraint where
Union (x ': xs) x = ()
Union (x ': xs) y = Union xs y
test1 :: Union [Circle', Triangle'] s => Shape s -> Int
test1 = undefined
The ()
above is the empty constraint (it's like an empty "list" of type class constraints).
The first "equation" of the type family makes use of the nonlinear pattern matching available in type families (it uses x
twice on the left hand side). The type family also makes use of the fact that if none of the cases match, it will not give you a valid constraint.
You should also be able to use a type-level Boolean instead of ConstraintKinds
. That would be a bit more cumbersome and I think it would be best to avoid using a type-level Boolean here (if you can).
Side-note (I can never remember this and I had to look it up for this answer): You get Constraint
in-scope by importing it from GHC.Exts
.
Edit: Partially disallowing unreachable definitions
Here is a modification to get it to (partially) disallow unreachable definitions as well as invalid calls. It is slightly more roundabout, but it seems to work.
Modify Union
to give a *
instead of a constraint, like this:
type family Union (a :: [k]) (r :: k) :: * where
Union (x ': xs) x = ()
Union (x ': xs) y = Union xs y
It doesn't matter too much what the type is, as long as it has an inhabitant you can pattern match on, so I give back the ()
type (the unit type).
This is how you would use it:
test1 :: Shape s -> Union [Circle', Triangle'] s -> Int
test1 Circle {} () = undefined
test1 Triangle {} () = undefined
-- test1 Square {} () = undefined -- This line won't compile
If you forget to match on it (like, if you put a variable name like x
instead of matching on the ()
constructor), it is possible that an unreachable case can be defined. It will still give a type error at the call-site when you actually try to reach that case, though (so, even if you don't match on the Union
argument, the call test1 (Square undefined) ()
will not type check).
Note that it seems the Union
argument must come after the Shape
argument in order for this to work (fully as described, anyway).