Currently, I generate eliminators with predicates of two different kinds, <Datatype> -> Type and <Datatype> ~> Type, and I also have a story for eliminators that are polymorphic over the arrow kind used. However, I'm questioning whether all of this is worth it, since:
99% of the type, I use the (~>) variants anyway
Predicates of kind <Datatype> -> Type can be turned into ones of kind <Datatype> ~> Type without too much trouble (using the genDefunSymbols function from singletons)
The arrow-polymorphic approach doesn't even work for all datatypes (e.g., GADTs)
Perhaps we should only generate eliminators of kind <Datatype> ~> Type.
Currently, I generate eliminators with predicates of two different kinds,
<Datatype> -> Type
and<Datatype> ~> Type
, and I also have a story for eliminators that are polymorphic over the arrow kind used. However, I'm questioning whether all of this is worth it, since:(~>)
variants anyway<Datatype> -> Type
can be turned into ones of kind<Datatype> ~> Type
without too much trouble (using thegenDefunSymbols
function fromsingletons
)Perhaps we should only generate eliminators of kind
<Datatype> ~> Type
.