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.