How can I create a function that only accepts a subset of constructors of a type?

Question

Let's say I have a type like this:

data Foo = Bar String | Baz | Qux String

I want to have a function like this:

get : Foo -> String
get (Bar s) = s
get (Qux s) = s

As written, this compiles, but it's not total, as there are missing cases; in other words, get Baz is treated like a hole rather than as an expression that doesn't typecheck.

I want to replace that Foo in the type signature of get with something that specifies that the value must be either a Bar or a Qux. How can I express this subset of the Foo type?

Answer 1

You could also mix the two approaches (by Kim Stiebel and Anton Trunov) and construct a helper data type. The type OnlyBarAndQux can only be constructed with values of Bar and Qux. For idris it is then possible to automatically infer a proof if this is the case when invoking get:

module FooMe

data Foo = Bar String | Baz | Qux String

data OnlyBarAndQux: Foo -> Type where
    BarEy: OnlyBarAndQux (Bar s)
    QuxEx: OnlyBarAndQux (Qux s)

||| get a string from a Bar or Qux
total
get: (f: Foo) -> {auto prf : OnlyBarAndQux f} -> String
get (Bar s) {prf = BarEy} = s
get (Qux s) {prf = QuxEx} = s

-- Tests

test1: get $ Bar "hello" = "hello"
test1 = Refl

test2: get $ Qux "hello" = "hello"
test2 = Refl

-- does not compile
-- test3: get $ Baz = "hello"