Meetings and locations model using simulated GADTs in F#

MeetingLocation.fs

module EmployeeLocation

open TypeEquality

type Name = string

/// Some employees are engineers.
type Engineer = Engineer of Name

/// Some employees are factory workers.
type FactoryWorker = FactoryWorker of Name

/// The company has offices. Each office room has a number.
type OfficeRoom = OfficeRoom of int

/// The company has a factory. A factory has different work areas at different floors.
type FactoryFloor =
    | Assembly
    | Electronics
    | QualityControl

/// A description of a (your) meeting with a single employee. Based on whom you want to talk to, the type of location
/// for the meeting is fixed. However the _actual_ location is not included in values of this type.
type MeetingRequest<'location> =
    | TalkToEngineer of Engineer * TEq<OfficeRoom,'location>
    | TaltToFactoryWorker of FactoryWorker * TEq<FactoryFloor,'location>

/// A helper for creating a meeting request with an engineer.
let meetingWithEngineer engineer = TalkToEngineer (engineer, TypeEquality.refl)

/// Similarly, a helper for creating a meeting request with a factory worker.
let meetingWithFactoryWorker factoryWorker = TaltToFactoryWorker (factoryWorker, TypeEquality.refl)

(* The most interesting function: given a meeting request, determine the location of the meeting. Each location is
consistent with the meeting request, namely whom the meeting is with. The function looks completely polymorphic in its
return type, which would mean that it can return nonsense location types like `bool`, but this is not the case and only
proper location types are possible. *)

/// Determine the location for a requested meeting.
let meetingLocation (meeting : MeetingRequest<'location>) : 'location =
    match meeting with
    | TalkToEngineer (Engineer name, forEngineer) ->
        // We could go to the database here, but here is a simple simulation
        let room = if name = "Peter" then OfficeRoom 1 else OfficeRoom 2
        room |> TypeEquality.coerce forEngineer
    | TaltToFactoryWorker (FactoryWorker _, forFactoryWorker) ->
        // All factory meetings should happen at the electronics floor because they have nice chairs
        let allFactoryMeetingsAtElectronics = Electronics
        allFactoryMeetingsAtElectronics |> TypeEquality.coerce forFactoryWorker

let example1 : OfficeRoom = meetingLocation (meetingWithEngineer (Engineer "Link"))

let example2 : FactoryFloor = meetingLocation (meetingWithFactoryWorker (FactoryWorker "Zelda"))