testing for singletons

singletons.hs

#! /usr/bin/env nix-shell --
#! nix-shell -p ghcid -p "haskellPackages.ghcWithPackages (pkgs: with pkgs; [singletons])" -i "ghcid -c 'ghci -Wall' -T main"

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Singletons
import Data.Singletons.TH

newtype Named n a = Named {forgetName :: a}

withNamed :: a -> (forall name. Named name a -> r) -> r
withNamed x f = f (Named x)

$( singletons
     [d|
       data People = Michael | Alex | Koray
       |]
 )

deriving instance Show People

deriving instance Eq People

data CanHaveSoup a s where
  CanHaveSoup :: SingI (s :: People) => Named a People -> Sing s -> CanHaveSoup a s

canHaveSoup ::
  SingI s =>
  Named a People ->
  Maybe (CanHaveSoup a s)
canHaveSoup a = case singThat (== forgetName a) of
  Nothing -> Nothing
  Just x -> Just (CanHaveSoup a x)

withCanHaveSoup ::
  SingI lbl =>
  People ->
  ( forall a.
    Named a People ->
    CanHaveSoup a lbl ->
    IO ()
  ) ->
  IO ()
withCanHaveSoup person f =
  withNamed person $ \namedPerson ->
    case canHaveSoup namedPerson of
      Nothing -> putStrLn "No soup for you!!!"
      Just canHaveSoupProof -> f namedPerson canHaveSoupProof

onlyForMichael ::
  Named a People ->
  CanHaveSoup a 'Michael ->
  IO ()
onlyForMichael _ _ = putStrLn "Soup For Michael!"

onlyForKoray ::
  Named a People ->
  CanHaveSoup a 'Koray ->
  IO ()
onlyForKoray _ _ = putStrLn "You get a soup too Koray!"

main :: IO ()
main = do
  withCanHaveSoup Michael onlyForMichael
  withCanHaveSoup Koray onlyForMichael
  withCanHaveSoup Koray onlyForKoray