[GHC] #7230: GHC states the same kind mismatched

[GHC]

#7230: GHC states the same kind mismatched
-----------------------------------------------+----------------------------
 Reporter:  konn                               |          Owner:                
     Type:  bug                                |         Status:  new           
 Priority:  normal                             |      Component:  Compiler      
  Version:  7.7                                |       Keywords:                
       Os:  MacOS X                            |   Architecture:  x86_64 (amd64)
  Failure:  Incorrect warning at compile-time  |       Testcase:                
Blockedby:                                     |       Blocking:                
  Related:                                     |  
-----------------------------------------------+----------------------------
 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.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7230>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler