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 |