A Haskell implementation of Gasche's unique inhabitation thesis work.
In slightly more detail, we try to decide whether there are 0, 1, or more possible implementations of a given type. If there is one, we synthesize it.
- Which types have a unique inhabitant, Focusing on pure program equivalence -- Gabriel Scherer's thesis
- djinn - "generate Haskell code from a type". This does a similar trick, but in a different way.