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