A value can carry proof

Every codebase past a certain age has this move somewhere: a string-keyed bag of settings, and a read function that lets you name whatever type you would like back. TypeScript spells it config.get("retries") as number. The Haskell below spells it with unsafeCoerce, which at least has the decency to look dangerous.

UnsafeRegistry.hs

import Data.Map.Strict (Map)import qualified Data.Map.Strict as Mapimport Data.Text (Text)import GHC.Exts (Any)import Unsafe.Coerce (unsafeCoerce)type Registry = Map Text AnyinsertValue :: Text -> a -> Registry -> RegistryinsertValue name value = Map.insert name (unsafeCoerce value)readValue :: Text -> Registry -> areadValue name registry = unsafeCoerce (registry Map.! name)

Look at what readValue promises: any a the caller feels like. The map stores every value as Any, the key picks the slot, and you pick the type, and no part of the program marries the two. Ask for the retries slot at Text and the registry hands you an integer's bits wearing a text label. That compiles today, passes every test that only asks correct questions, and detonates next month inside some innocent function that tried to use the value.

Put the type inside the key#

The repair is one of my favorite tricks in typed programming: stop letting the question and the type of its answer travel separately. A generalized algebraic data type lets each constructor pick its own index, so Retries does not have type Key — it has type Key Int, and asking with it is already a typed act.

Settings.hs

{-# LANGUAGE GADTs #-}data Config = Config { host :: Text, retries :: Int, debug :: Bool }data Key a where  Host    :: Key Text  Retries :: Key Int  Debug   :: Key BoolreadKey :: Key a -> Config -> areadKey Host    = hostreadKey Retries = retriesreadKey Debug   = debug

Here is the part worth slowing down for. When readKey matches on Retries, GHC learns something inside that branch: the abstract a from Key a is now provably Int, which is why returning the retries field type-checks. GHC's guide calls this refinement, and none of it exists at runtime — no cast, no tag check beyond the match you already wrote. People call the constructor a witness because holding it testifies to a fact the checker could not otherwise see.

Make equality a value too#

A real registry is harder than readKey, because a registry hides types. Each Entry boxes a key with its value and forgets the index — that is the existential — so lookup has to recover a type it can no longer see. The move is the same one again, pushed further: comparing two keys can produce the missing proof as an ordinary value.

Registry.hs

import Data.Type.Equality ((:~:)(Refl))sameKey :: Key a -> Key b -> Maybe (a :~: b)sameKey Host Host = Just ReflsameKey Retries Retries = Just ReflsameKey Debug Debug = Just ReflsameKey _ _ = Nothingdata Entry where  Entry :: Key a -> a -> EntrylookupEntry :: Key a -> [Entry] -> Maybe alookupEntry _ [] = NothinglookupEntry wanted (Entry actual value : rest) =  case sameKey wanted actual of    Just Refl -> Just value    Nothing -> lookupEntry wanted rest

The type a :~: b has exactly one constructor, Refl :: a :~: a. So if sameKey hands you a Refl, the hidden type and the requested type were equal all along, and matching on it lets value walk out of its box at the type you asked for. Misses stay boring: different constructors mean Nothing, the search moves on, and no Any ever leaks past the door.

You could build something similar on TypeRep, which is how GHC's own Dynamic compares types at runtime. What Dynamic cannot tell you is why retries should be an Int in the first place. Untrusted configuration text still needs a parser at the boundary, one that returns an existential SomeKey and rejects unknown names, but that check runs once instead of at every use site.

	Any + unsafeCoerce	Dynamic + TypeRep	GADT Key
Who names the result type	the caller, with nothing checking the choice	the caller, checked against the stored type	the key itself — `Retries` is a `Key Int`
When a mismatch surfaces	at runtime, later, inside whatever code uses the mislabeled value	at lookup, when the runtime comparison fails	the compiler rejects a mistyped ask before the program runs
The key vocabulary	any string at all	every type in the program	`Host`, `Retries`, `Debug` — the registry's actual domain

Three designs for the same settings registry, from unchecked cast to carried proof.

The snag in my toy version is the wildcard at the bottom of sameKey. Add a Timeout constructor and forget its equal case, and everything still compiles — the new key is simply unfindable, every lookup a polite Nothing. Deleting the wildcard and enumerating the unequal pairs makes the compiler name the missing case, at the price of a quadratic pile of Nothing clauses. Whether that trade is worth it might be taste, but key vocabularies tend to grow exactly when nobody is thinking about this file anymore.