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