Skip to content

built in type lit type families that could be injective *should* be injective

Motivation

make type lits useful sans solvers

Proposal

https://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-TypeLits.html

AppendSymbol + * - and ^

all of these have clear "unique answer" or "should be error" semantics when any 2 of the pair of inputs and the output are specified

adding that extra knowledge to the type checker/inference machinery would also make it possible to write a "S :: Nat -> Nat" type family in user space that works as an injective type family too i think? (and thats a long running pain point that kills using them)

might also be good to think about other type level literals that should be in base. Eg type level integers?

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information