# Inferring non-tau kinds

While up to my usual type-level shenanigans, I found that I want this definition:

```
data TypeRep (a :: k) -- abstract
data TypeRepX :: (forall k. k -> Constraint) -> Type where
TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
c a => TypeRep a -> TypeRepX c
```

Note `TypeRepX`

's higher-rank kind. The idea is that I want to optionally constrain `TypeRepX`

's payload. Without using a higher-rank kind, the constraint would necessary fix the kind of the payload, and I don't want that. For example, I sometimes use `TypeRepX ConstTrue`

, where

```
class ConstTrue (a :: k)
instance ConstTrue a
```

This actually works just fine, and I've been using the above definition to good effect.

But then I wanted a `Show`

instance:

```
instance Show (TypeRep a) -- elsewhere
instance Show (TypeRepX c) where
show (TypeRepX tr) = show t
```

Looks sensible. But GHC complains. This is because it tries to infer `c`

's kind, by inventing a unification variable and then unifying. But this doesn't work, of course, because `c`

's kind is not a tau-type, so unification fails, lest we let impredicativity sneak in. What's particularly vexing is that, even if I annotate `c`

with the correct kind, unification *still* fails. This is because that `c`

is a *usage* of `c`

, not a *binding* of `c`

. Indeed, there is no place in an instance declaration to bind a type variable explicitly, so I have no recourse.

I'm not sure what the solution is here. Somehow, it feels that inferring a non-tau kind for `c`

is perfectly safe, because the kind is known from the use of `TypeRepX`

. This would allow me to drop the kind annotation in the definition of `TypeRepX`

, which looks redundant to me. But I'm not fully sure about this assumption.

At the least, we could introduce a spot for explicit binding of type variables in instance declarations.

I think, actually, I just figured it out. Use `ExpType`

s when kind-checking types. Then I think the normal bidirectional thing (actually already implemented) will do the Right Thing.

## Trac metadata

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

Version | 8.1 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |