Skip to content

Teach Template Haskell about specificity

Consider

data P1 a = MkP1
data P2 (a :: k) = MkP2

We have

P1 :: forall {k}. k -> Type
MkP1 :: forall {k} (a :: k). P1 a

P2 :: forall k. k -> Type
MkP2 :: forall k (a :: k). P2 a

Note the different specificities.

Yet if we reify these two types, we get the exact same output. This makes downstream processing more challenging. For example, it causes trouble for singletons.

We should fix. I propose adding specifities to TyVarBndr, but there may be other solutions.

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