[GHC] #9260: Unnecessary error using GHC.TypeLits

[GHC]

#9260: Unnecessary error using GHC.TypeLits
-------------------------------------+-------------------------------------
       Reporter:  Iceland_jack       |             Owner:
           Type:  bug                |            Status:  new
       Priority:  low                |         Milestone:
      Component:  Compiler           |           Version:  7.8.2
       Keywords:  type lits, data    |  Operating System:  Linux
  kinds, error message               |   Type of failure:  Incorrect
   Architecture:  Unknown/Multiple   |  warning at compile-time
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 Compiling:

 {{{
 {-# LANGUAGE DataKinds, TypeOperators, GADTs #-}

 module Error where

 import GHC.TypeLits

 data Fin n where
   Fzero :: Fin (n + 1)
   Fsucc :: Fin n -> Fin (n + 1)
 }}}

 gives a strange (unnecessary) error message claiming that `Fin 1` doesn't
 match the expected type `Fin (0 + 1)`:

 {{{
 % ghc --version
 The Glorious Glasgow Haskell Compilation System, version 7.8.2
 % ghc -ignore-dot-ghci /tmp/Error.hs
 [1 of 1] Compiling Error            ( /tmp/Error.hs, /tmp/Error.o )

 /tmp/Error.hs:12:8:
     Couldn't match type ‘0’ with ‘1’
     Expected type: Fin 1
       Actual type: Fin (0 + 1)
     In the expression: Fsucc Fzero
     In an equation for ‘test’: test = Fsucc Fzero

 /tmp/Error.hs:12:14:
     Couldn't match type ‘1’ with ‘0’
     Expected type: Fin 0
       Actual type: Fin (0 + 1)
     In the first argument of ‘Fsucc’, namely ‘Fzero’
     In the expression: Fsucc Fzero
 %
 }}}

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