content: #!/usr/bin/env stack
  -- stack --install-ghc ghci --resolver lts-16 --package singletons
  
  {-# LANGUAGE DataKinds            #-}
  {-# LANGUAGE EmptyCase            #-}
  {-# LANGUAGE GADTs                #-}
  {-# LANGUAGE InstanceSigs         #-}
  {-# LANGUAGE KindSignatures       #-}
  {-# LANGUAGE LambdaCase           #-}
  {-# LANGUAGE RankNTypes           #-}
  {-# LANGUAGE ScopedTypeVariables  #-}
  {-# LANGUAGE StandaloneDeriving   #-}
  {-# LANGUAGE TemplateHaskell      #-}
  {-# LANGUAGE TypeApplications     #-}
  {-# LANGUAGE TypeFamilies         #-}
  {-# LANGUAGE UndecidableInstances #-}
  
  import           Data.Kind
  import           Data.Singletons
  import           Data.Singletons.TH
  
  $(singletons [d|
    data DoorState = Opened | Closed | Locked
      deriving (Show, Eq)
    |])
  
  data Door :: DoorState -> Type where
      UnsafeMkDoor :: { doorMaterial :: String } -> Door s
  
  closeDoor :: Door 'Opened -> Door 'Closed
  closeDoor (UnsafeMkDoor m) = UnsafeMkDoor m
  
  lockDoor :: Door 'Closed -> Door 'Locked
  lockDoor (UnsafeMkDoor m) = UnsafeMkDoor m
  
  openDoor :: Door 'Closed -> Door 'Opened
  openDoor (UnsafeMkDoor m) = UnsafeMkDoor m
  
  doorStatus :: Sing s -> Door s -> DoorState
  doorStatus SOpened _ = Opened
  doorStatus SClosed _ = Closed
  doorStatus SLocked _ = Locked
  
  lockAnyDoor :: Sing s -> (Door s -> Door 'Locked)
  lockAnyDoor = \case
      SOpened -> lockDoor . closeDoor
      SClosed -> lockDoor
      SLocked -> id
  
  doorStatus_ :: SingI s => Door s -> DoorState
  doorStatus_ = doorStatus sing
  
  lockAnyDoor_ :: SingI s => Door s -> Door 'Locked
  lockAnyDoor_ = lockAnyDoor sing
  
  mkDoor :: Sing s -> String -> Door s
  mkDoor _ = UnsafeMkDoor
  
  main :: IO ()
  main = return ()
  
  
  -- Exercises
  
  unlockDoor :: Int -> Door 'Locked -> Maybe (Door 'Closed)
  unlockDoor n (UnsafeMkDoor m)
      | n `mod` 2 == 1 = Just (UnsafeMkDoor m)
      | otherwise      = Nothing
  
  openAnyDoor :: SingI s => Int -> Door s -> Maybe (Door 'Opened)
  openAnyDoor n = openAnyDoor_ sing
    where
      openAnyDoor_ :: Sing s -> Door s -> Maybe (Door 'Opened)
      openAnyDoor_ = \case
        SOpened -> Just
        SClosed -> Just . openDoor
        SLocked -> fmap openDoor . unlockDoor n
  