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