I'm trying to restrict the return type of a function to a subset of (kind) constructors. I can use typeclasses to restrict the input types, but when I try the same technique on return types as shown below, I get a Couldn't match type ‘s’ with ‘'A’ error.
Is there a way to restrict the bar function below to return either SomeA or SomeB?
It seems that Liquid Haskell is an alternative, but it seems that this should be possible using only things like DataKinds, GADTs and/or TypeInType.
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
module Test where
data State = A | B | C
class AorB (s :: State)
instance AorB 'A
instance AorB 'B
data Some (s :: State) where
SomeA :: Some 'A
SomeB :: Some 'B
SomeC :: Some 'C
-- This works
foo :: AorB s => Some s -> Bool
foo aorb = case aorb of
SomeA -> True
SomeB -> False
-- This fails to compile with ""Couldn't match type ‘s’ with ‘'A’""
bar :: AorB s => Some s
bar = SomeA
A few things here. If you compile with -Wall (which you should!) you would find that your definition of foo gives an inexhaustive patterns warning. And it should, because the way you have defined AorB is "open". That is, somebody in another module is free to declare
instance AorB 'C
and then your definition of foo will suddenly become invalid as it fails to handle the SomeC case. To get what you are looking for, you should use a closed type family:
type family IsAorB s where
IsAorB 'A = 'True
IsAorB 'B = 'True
IsAorB _ = 'False
This family is totally defined on States. We would then define your previous AorB constraint like so:
type AorB s = IsAorB s ~ 'True
However, in a moment we will need to use AorB in curried form, which is not allowed for type synonyms. There is an idiom for declaring curriable synonyms which is a bit clunky, but is the best we have at the moment:
class (IsAorB s ~ 'True) => AorB s
instance (IsAorB s ~ 'True) => AorB s
Anyway, with this new definition, you will find that the inexhaustive pattern warning goes away for foo. Good.
Now on to your question. The trouble with your definition (with an explicit forall added for clarity)
bar :: forall s. AorB s => Some s
bar = SomeA
is that we are allowed to instantiate bar @B, giving us
bar @B :: AorB B => Some B
bar = SomeA
AorB B is satisfiable, so we should be able to get a Some B, right? But not according to your implementation. So something is logically wrong here. You are probably looking to return an existentially quantified s, in other words, you want the bar function to choose which s it is, not the caller. Informally
bar :: exists s. AorB s <AND> Some s
That is, bar chooses an s, and returns a Some s, together with some evidence that AorB s holds. This is no longer an implication, we would not put the responsibility on the caller to prove that the type bar chose was either A or B -- the caller has no idea what was chosen.
Haskell does not directly support existential types, but we can model them with a GADT (make sure to use PolyKinds and ConstraintKinds)
data Ex c f where
Ex :: c a => f a -> Ex c f
Ex c f can be read as "there exists a such that c a holds and there is a value f a". This is existential becuase the variable a does not appear in Ex c f, it's hidden by the constructor. And now we can implement bar
bar :: Ex AorB Some
bar = Ex SomeA
We can test that the constraints are correctly propagated by passing this to your foo:
test :: Bool
test = case bar of Ex s -> foo s
There you go.
That said, design-wise I would just say
bar :: Some A
instead. Type signatures should be as informative as possible. Don't hide information that you know -- let abstraction do the hiding. When you hide information about your assumptions/arguments, you are making your signature stronger; when you hide about your results, you are making it weaker. Make it strong.