How To Add a Constraint to a Type Constructor

Question

Consider the following data type:

data Get (statusCode :: Nat)

Actually, it's a simplified type constructor from servant which is then used in a type-level API like this:

type API = "users" :> Verb 'GET 200 '[JSON] [User]

For our purposes we can cut down the API to

type API = Get 200

Now, having a restriction of the status code being of kind Nat is too loose, allowing to define a non-existing HTTP status code:

type API = Get 999

Hence, the question: Is there a way to restrict the set of naturals that can be applied to the Get type constructor?

What was Tried

I'll omit all the pragmas and imports in the code samples for clarity.

A different kind for statusCode

One obvious way to fix it would be to define a separate ADT for status codes and use it in place of Nat utilizing data type promotion.

data StatusCode = HTTP200 | HTTP201 | HTTP202
data Get (statusCode :: StatusCode)

However, this is a breaking change, which'd require to bump a major version and rewrite all the users' definitions. I doubt the benefit of restricted codes is worth it.

DatatypeContexts

This extension allows to have a straightforward constraint on our type variable

data IsStatusCode statusCode => Get (statusCode :: Nat)

but it requires users to add the constraint to all their declaration. Again, a breaking change. Besides, DatatypeContexts is deprecated.

Type Families

We could conditionally create Get' from the example below using type families, but for some reason declaring a type alias happily compiles. In order to get an error we need to construct a value of this type, which is also a breaking change.

data Get' (statusCode :: Nat) = Get

type family Get x where
  Get x = If (x <=? 600) (Get' x) (TypeError (Text "Invalid Code"))

type API1 = Get 200
type API2 = Get 999 -- compiles.

api :: Get 999 -- doesn't compile.
api = Get

Answer 1

I'll start with a solution, then discuss the other possibilities (which appear to not have panned out):

{-# LANGUAGE TypeOperators, TypeInType, GADTs #-}

import GHC.TypeLits (Nat, type (<=))
import Data.Proxy (Proxy(..))
import Data.Kind (type (*))

data Get (statusCode :: Nat) :: (statusCode <= 600) => *

type API1 = Get 900 -- compiles
type API2 = Get 200 -- compiles

api1 :: Proxy (Get 900) -- doesn't compile
api1 = Proxy

api2 :: Proxy (Get 200) -- compiles
api2 = Proxy

No type families needed, no need to ever drop down to the value level. The type synonyms, however, will compile just fine. Using a type synonym of an invalid Get will lead to a compile time crash at the usage site. I reckon this is as good a solution as you can hope for. Please let me know if anything is unclear.

---

Next, just some thoughts on the other approaches:

DatatypeContexts

This one will never work: besides being deprecated, all this does is add the constraint to constructors. You specifically indicated you don't want to have to construct anything of the type, so this is pointless. The new GADT syntax fixes this ambiguity - the constraints are now clearly bound to the data or type constructors.

Type Families and TypeError

I believe this should work, and without having to construct a value of the type. (So the following should be fine:)

data Get' (statusCode :: Nat)

type family Get x where
  Get x = If (x <=? 600) (Get' x) (TypeError (Text "Invalid Code"))

api2 :: Proxy (Get 200) -- should compile.
api2 = Proxy

api1 :: Proxy (Get 999) -- shouldn't compile, but currently does
api1 = Proxy

I am motivated to believe this should work based on the example in this trac ticker. Something here is clearly not behaving as it should: even if I replace the call to the type function If with the TypeError itself, still nothing gets triggered - it appears that TypeErrors that aren't top-level still cause some problems.

On the other hand, I am really unsure what the behaviour of TypeError in type synonyms should be, although I'm inclined to say that type API1 = Get 999 should not compile, since type API1 = TypeError (Text "error") doesn't.