Using tagged dictionaries to ensure coherency in Haskell

tagging.haskell

-- Demonstrates how to ensure coherence when representing typeclasses with first-class dictionaries

newtype Tag t a = Tag { untag :: a } -- constructor kept private
use :: a -> (forall t . Tag t a -> b) -> b -- tagged values introduced in a stack discipline

-- Example, a 'first-class' Ord

newtype Ord a = Ord { ordering :: a -> a -> Ordering }

-- Ensure coherence when using this with Set

empty :: Tag t (Set a)
fromList :: [a] -> Tag t (Order a) -> Tag t (Set a)

-- Common tag ensures both sets built with same `Order`, which is introduced in `use`
union :: Tag t (Set a) -> Tag t (Set a) -> Tag t (Set a)

-- Left as an exercise to make this general idea not horrible to use :)

By the way, I don't endorse actually doing this in Haskell. I just wanted to point out that it is in fact possible.