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

[GHC]

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

 * os:  Linux => Unknown/Multiple
 * milestone:   => 7.10.1


Old description:

> 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
> %
> }}}

New description:

 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)

 test :: Fin 1
 test = Fsucc Fzero
 }}}

 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
 %
 }}}

--

Comment:

 GHC HEAD now gives the following error message for the program from the
 description:
 {{{
 $ ghc-7.9.20141113 test.hs
 [1 of 1] Compiling Test             ( test.hs, test.o )

 test.hs:12:14:
     Couldn't match type ‘n0 + 1’ with ‘0’
     The type variable ‘n0’ is ambiguous
     Expected type: Fin 0
       Actual type: Fin (n0 + 1)
     In the first argument of ‘Fsucc’, namely ‘Fzero’
     In the expression: Fsucc Fzero
 }}}

 It looks like this bug got fixed, but I'm not 100% sure. A regression test
 is still missing.

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