A SuchThat c p is a p s, where s is such that it satisfies all of the constraints in c. Note that you must always wrap results from pattern-matching on the SuchThat constructor in a SuchThat, or GHC will complain about s escaping its scope.

Ideally, we would write:

type SuchThat (c :: [k -> Constraint]) (p :: k -> *) = forall s. Constrain c s => p s

But type synonyms don't work that way

Inject a value into a SuchThat. It becomes more ambiguous because it throws out the exact type of s.

Escape from a SuchThat by running a universally quantified continuation.

A ForAny f is an f containing some arbitrary values, meaning you can only apply operations that would work for any type of value it contains. This is useful if the type parameter is phantom because it allows you to ignore it. This is called "ghost busting" because it removes the phantom. It can also be used for reading only the structure of something rather than the actual values. For example, ForAny [] is isomorphic to both the natural numbers, and the fixed point of Maybe.

If the type constructor in question is a functor, we can scope out its structure by converting every element to (). Note that this is actually the most general way to do this, since the type signature would otherwise be Functor p => SuchThat c p -> (forall x. x -> a) -> p a. That means the output type must be isomorphic to () because that is the terminal object in Hask.

>>> discoverStructure (ambiguate ['a','b','c'] :: ForAny [])
[(),(),()]

>>> discoverStructure (ambiguate (Just "hi") :: ForAny Maybe)
Just ()

>>> discoverStructure (ambiguate Nothing :: ForAny Maybe)
Nothing

A function between SuchThat c's between different type constructors is isomorphic to a natural transformation between those type constructors. This is especially useful if c ~ '[], meaning you have a ForAny.

The other half of the aforementioned isomorphism. This specialises c to '[Constains x] under the hood.

A Some c is some value that satisfies all the constraints in c.

Build a Some c from some thing that satisfies c.

A Satisfies x is a value that satisfies the single constraint x.

A Contains x f is isomorphic to an f x:

containsToRaw :: Contains x f -> f x
containsToRaw = ambiguously id

rawToContains :: f x -> Contains x f
rawToContains = ambiguate

A type level fold for applying many constraints to the same thing