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

14 Nov 2014

      #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