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 ScopedTypeVariables            #-}
  {-# LANGUAGE StandaloneDeriving             #-}
  {-# LANGUAGE TemplateHaskell                #-}
  {-# LANGUAGE TypeApplications               #-}
  {-# LANGUAGE TypeFamilies                   #-}
  {-# LANGUAGE TypeOperators                  #-}
  {-# LANGUAGE UndecidableInstances           #-}
  {-# OPTIONS_GHC -Wall                       #-}
  {-# OPTIONS_GHC -Werror=incomplete-patterns #-}
  
  import           Data.Kind
  import           Data.Singletons
  import           Data.Singletons.Prelude hiding (And, Or)
  import           Data.Singletons.TH
  
  $(singletons [d|
    data DoorState = Opened | Closed | Locked
      deriving (Show, Eq, Ord)
    |])
  
  data Door :: DoorState -> Type where
      UnsafeMkDoor :: { doorMaterial :: String } -> Door s
  
  mkDoor :: Sing s -> String -> Door s
  mkDoor _ = UnsafeMkDoor
  
  data SomeDoor :: Type where
      MkSomeDoor :: Sing s -> Door s -> SomeDoor
  
  $(singletons [d|
    mergeState :: DoorState -> DoorState -> DoorState
    mergeState = max
    |])
  
  mergeDoor
      :: Door s
      -> Door t
      -> Door (MergeState s t)
  mergeDoor d e = UnsafeMkDoor $ doorMaterial d ++ " and " ++ doorMaterial e
  
  mergeSomeDoor :: SomeDoor -> SomeDoor -> SomeDoor
  mergeSomeDoor (MkSomeDoor s d) (MkSomeDoor t e) =
      MkSomeDoor (sMergeState s t) (mergeDoor d e)
  
  data Hallway :: [DoorState] -> Type where
      HEnd  :: Hallway '[]        -- ^ end of the hallway, a stretch with no
                                  --   doors
      (:<#) :: Door s
            -> Hallway ss
            -> Hallway (s ': ss)  -- ^ A door connected to a hallway is a new
                                  --   hallway, and we track the door's state
                                  --   in the list of hallway door states
  infixr 5 :<#
  
  $(singletons [d|
    mergeStateList :: [DoorState] -> DoorState
    mergeStateList []     = Opened               -- ^ the identity of mergeState
    mergeStateList (s:ss) = s `mergeState` mergeStateList ss
    |])
  
  collapseHallway :: Hallway ss -> Door (MergeStateList ss)
  collapseHallway HEnd       = mkDoor SOpened "End of Hallway"
  collapseHallway (d :<# ds) = d `mergeDoor` collapseHallway ds
  