Example on how to create constrained functions for particular ADT constructors in Haskell using GADTs, DataKinds and KindSignatures extension

Example.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
module Main where

data UserType
  = VirtualUser
  | RealUser

data User (userType :: UserType) where
  MkVirtualUser :: String -> User 'VirtualUser
  MkRealUser    :: String -> User 'RealUser

deliverPackage :: User 'RealUser -> String -> IO ()
deliverPackage (MkRealUser name) package =
  putStrLn $ "Delivering package " ++ package ++ " for user " ++ name

sendEmail :: User 'VirtualUser -> String -> IO ()
sendEmail (MkVirtualUser email) body =
  putStrLn $ "Sending email to " ++ email ++ " with body: \n" ++ body

userData :: User userType -> IO ()
userData (MkRealUser name) = putStrLn $ "User with name: " ++ name
userData (MkVirtualUser email) = putStrLn $ "User with email: " ++ email

main :: IO ()
main = do
  let vuser = MkVirtualUser "[email protected]"
      ruser = MkRealUser "Roman Gonzalez"


  -- Compiles with all types of users
  userData vuser
  userData ruser

  --------------------------------------------------------------------------------
  -- Compiles only with types of user @'RealUser@

  deliverPackage ruser "foobar"

  {-
  deliverPackage vuser "barfoo" -- <- Compile Error
  --  Couldn't match type ‘'VirtualUser’ with ‘'RealUser’
  --  Expected type: User 'RealUser
  --    Actual type: User 'VirtualUser
  --  In the first argument of ‘deliverPackage’, namely ‘vuser’
  --  In a stmt of a 'do' block: deliverPackage vuser "barfoo"
  -}

  --------------------------------------------------------------------------------
  -- Compiles only with types of user @'VirtualUser@

  sendEmail vuser "[email protected]"

  {-
  sendEmail ruser "[email protected]" -- <- Compile Error

  --  Couldn't match type ‘'RealUser’ with ‘'VirtualUser’
  --  Expected type: User 'VirtualUser
  --    Actual type: User 'RealUser
  --  In the first argument of ‘sendEmail’, namely ‘ruser’
  --  In a stmt of a 'do' block: sendEmail ruser "[email protected]"
  -}

No need for DataKinds and plain GADTs are enough

data VirtualUser 
data RealUser

data User a where
  MkVirtualUser :: String -> User VirtualUser
  MkRealUser    :: String -> User RealUser


deliverPackage :: User RealUser -> String -> IO ()
deliverPackage = …

sendEmail :: User VirtualUser -> String -> IO ()
sendEmail = …

I see, we could do it too with EmptyDataDecls LANGUAGE pragma, we can constraint together the Phantom Type values with a DataKind extensions though, which would drive me more to that approach.

e.g. User FooBar is something I don't want to be defined if it is not a constructor on the UserType ADT.

Thanks for your feedback 👍

I used EmptyDataDecl because there no need for that in your example. But as you noticed, nothing prevents you from doing otherwise.

@YoEight @roman using only GADTs means you cannot constrain the types of User, as anything of kind * may be a valid user, thus losing some semantics.

But it is nice not to have to use so many extensions, so perhaps it's worth it ;)