GHC states the same kind mismatched
|Reported by:||konn||Owned by:|
|Operating System:||MacOS X||Architecture:||x86_64 (amd64)|
|Type of failure:||Incorrect warning at compile-time||Test Case:||T7230|
|Related Tickets:||Differential Revisions:|
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.
Change History (5)
Changed 3 years ago by konn
comment:3 Changed 3 years ago by simonpj
- difficulty set to Unknown
- Status changed from new to merge
- Test Case set to T7230