# Typeable imposes seemingly redundant constraints on polykinded instances

**See also #21822 (closed), #16627.**

To derive `Data`

for `Const`

, we need

`deriving instance (Typeable k, Data a, Typeable (b :: k)) => Data (Const a b)`

Where's that `Typeable k`

constraint come from? It turns out that for reasons I haven't looked into, we can only obtain `Typeable (Const a (b :: k))`

if we have `Typeable k`

; `(Typeable a, Typeable b)`

is insufficient. Is there a reason for that?

Annoyingly, we can actually *get* that:

```
weGotThat :: forall k (a :: k). Typeable a :- Typeable k
weGotThat = Sub $ withTypeable (typeRepKind (typeRep :: TypeRep a)) Dict
```

But of course that doesn't help us.

Could we use `UndecidableSuperClasses`

to work around this problem? I think we likely can, although I'm concerned about the performance implications:

```
class (Typeable a, Typeable' k) => Typeable' (a :: k)
instance (Typeable a, Typeable' k) => Typeable' (a :: k)
withTypeable' :: forall k (a :: k) r. TypeRep a -> (Typeable' a => r) -> r
withTypeable' tr f = withTypeable tr $ withTypeable (typeRepKind (typeRep @a)) f
```

## Trac metadata

Trac field | Value |
---|---|

Version | 8.2.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | bgamari |

Operating system | |

Architecture |