GHC states the same kind mismatched
The attached code fails to compile with following rather strange kind error:
/Users/hiromi/haskell/lab/typelevel/kind-mismatch-error.hs:52:17:
Couldn't match kind `Nat' with `Nat'
Expected type: (':) Nat x1 xs2
Actual type: xs1
Kind incompatibility when matching types:
xs1 :: [Nat]
(':) Nat x1 xs2 :: [Nat]
In the pattern: SCons y xs
In the pattern: SCons x (SCons y xs)
Failed, modules loaded: none.
The code, on the other hand, is expected not to compile because current GHC can't infer that Increasing (x ': y ': xs)
implies x :<<= y
, and the code attached compiles successfully if we rewrite the function crash
as follows:
crash :: (Increasing xs) ~ True => SList xs -> SBool (Increasing xs)
crash (SCons x (SCons y xs)) =
case x %:<<= y of
STrue -> x %:<<= y
_ -> error "impossible"
crash _ = STrue
I think it is strange and rather confusing that GHC says "Nat
kind doesn't match with Nat
!" and GHC should throws more appropriate compile error.
(Furthermore, it would be more convenient if GHC could infer x :<<= y
from Increasing (x ': y ': xs)
, but it should be argued in another place, not here.)
I confirmed that this strange error message is genrated in 7.7.20120906.
Trac metadata
Trac field | Value |
---|---|
Version | 7.7 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |