GHC.Core.Map.Type

TypeMap a is a map from Type to a. If you are a client, this is the type you want. The keys in this map may have different kinds.

A LooseTypeMap doesn't do a kind-check. Thus, when lookup up (t |> g), you'll find entries inserted under (t), even if (g) is non-reflexive.

TypeMapG a is a map from DeBruijn Type to a. The extended key makes it suitable for recursive traversal, since it can track binders, but it is strictly internal to this module. If you are including a TypeMap inside another TrieMap, this is the type you want. Note that this lookup does not do a kind-check. Thus, all keys in this map must have the same kind. Also note that this map respects the distinction between Type and Constraint, despite the fact that they are equivalent type synonyms in Core.

DeBruijn a represents a modulo alpha-renaming. This is achieved by equipping the value with a CmEnv, which tracks an on-the-fly deBruijn numbering. This allows us to define an Eq instance for DeBruijn a, even if this was not (easily) possible for a. Note: we purposely don't export the constructor. Make a helper function if you find yourself needing it.

Synthesizes a DeBruijn a from an a, by assuming that there are no bound binders (an empty CmEnv). This is usually what you want if there isn't already a CmEnv in scope.

A BndrMap is a TypeMapG which allows us to distinguish between binding forms whose binders have different types. For example, if we are doing a TrieMap lookup on (x :: Int) -> (), we should not pick up an entry in the TrieMap for (x :: Bool) -> (): we can disambiguate this by matching on the type (or kind, if this a binder in a type) of the binder.

We also need to do the same for multiplicity! Which, since multiplicities are encoded simply as a Type, amounts to have a Trie for a pair of types. Tries of pairs are composition.