Open phantom types with proof

PhantomProof.fs

namespace PhantomTypes

module Phantom =

    // Private, so must use function 'prove'.
    type ProofOf<'a> = private | ProofOfA

    // A module proves that it can construct values of type 'a' by providing a value to this function.
    let prove (_ : 'a) : ProofOf<'a> = ProofOfA

module Names =
    
    open Phantom

    /// A type of names for entities represented by 'e'. Intention: modules which own entities do not expose constructors
    /// of "their" 'e'.
    type Name<'e> = private | Name of (string * ProofOf<'e>)

    /// Access the name (only).
    let (|Name|) (Name (name, _)) = name

    /// Make a name 'n' for entity represented by 'e'.
    let name e n = Name (n, prove e)

module Database =

    open Names

    type DB = private | DB

    // Only this module, namely this function, can provide values of type Name<DB>.
    let databaseName dbname = name DB dbname // Name<DB>

module User =

    open Names
    
    type User = private | User

    // Only this module, namely this function, can provide values of type Name<User>.
    let userName uname = name User uname // Name<User>

module Program =

    open Names
    open Database
    open User

    // Not allowed in this module, must use 'userName'.
    //let fakeUser = name User "root"
    // Like this
    let trustedUser = userName "root" // Name<User>

    let giveAccess (database : Name<DB>) (user : Name<User>) =
        let (Name database), (Name user) = database, user
        (failwith "Do something here") database user