# Permit levity polymorphism in kinds

```
{-# language TypeInType, TypeFamilies, MagicHash #-}
import GHC.Exts
type family MatchInt (f :: Int) :: () where
MatchInt ('I# x) = '()
```

produces

```
<interactive>:2:59: error:
• Couldn't match a lifted type with an unlifted type
When matching kinds
k0 :: *
Int# :: TYPE 'IntRep
Expected kind ‘Int#’, but ‘x’ has kind ‘k0’
• In the first argument of ‘ 'I#’, namely ‘x’
In the first argument of ‘MatchInt’, namely ‘( 'I# x)’
In the type family declaration for ‘MatchInt’
```

If, however, I replace `x`

in the pattern with `_`

, the type checker is satisfied. If I give it a pattern signature,

`MatchInt ('I# (x :: Int#)) = '()`

I get a different (and equally unhelpful) error message,

```
• Expecting a lifted type, but ‘Int#’ is unlifted
• In the kind ‘Int#’
In the first argument of ‘ 'I#’, namely ‘(x :: Int#)’
In the first argument of ‘MatchInt’, namely ‘( 'I# (x :: Int#))’
```

## Trac metadata

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

Version | 8.3 |

Type | Bug |

TypeOfFailure | OtherFailure |

Priority | normal |

Resolution | Unresolved |

Component | Compiler (Type checker) |

Test case | |

Differential revisions | |

BlockedBy | |

Related | |

Blocking | |

CC | |

Operating system | |

Architecture |