Haskell GADT with Existential

gadt.hs

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

-- Run this with
-- $ chmod +x ./file.hs
-- $ ./file.hs
--
-- See this thread https://discourse.haskell.org/t/how-to-restrict-function-to-certain-constructors/2785/7
-- for a discussion of the problem

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

main :: IO ()
main =
  -- Change "admin" to "user" for the user session or any other string for the
  -- NoAuthentication session
  let session = login "koo"
   in do
        handleAnyAuthenticationLevel session
        case session of
          (HelperType adminSession@(Admin _)) -> handleOnlyAdmins adminSession
          _ -> print "403"

data AuthenticationLevel
  = NoAuthentication
  | UserLevel
  | AdminLevel

data Session authStatus sessionValue where
  None :: Session 'NoAuthentication sessionValue
  User :: String -> Session 'UserLevel String
  Admin :: String -> Session 'AdminLevel String

data HelperType c where
  HelperType :: Session a c -> HelperType c

-- This works
handleAnyAuthenticationLevel :: HelperType c -> IO ()
handleAnyAuthenticationLevel (HelperType None) =
  print $ "handleAnyAuthenticationLevel: " ++ ":("
handleAnyAuthenticationLevel (HelperType (User value)) =
  print $ "handleAnyAuthenticationLevel: " ++ value
handleAnyAuthenticationLevel (HelperType (Admin value)) =
  print $ "handleAnyAuthenticationLevel: " ++ value

handleOnlyAdmins :: Session 'AdminLevel String -> IO ()
handleOnlyAdmins (Admin value) = print $ "handleOnlyAdmins: " ++ value

-- This compiles, thanks to the existential
login :: String -> HelperType String
login "admin" = HelperType $ Admin "I am an admin"
login "user" = HelperType $ User "I am a user"
login _ = HelperType None

-- This does not compile, since the return type is restricted to one of the
-- GADT branches
-- loginDoesNotCompile =
--   if False
--     then None
--     else User "I am Joe"