Unnecessary error using GHC.TypeLits

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
%

changed weight to 3

added Tbug Trac import labels

Forgot to add the actual failing case:

test :: Fin 1
test = Fsucc Fzero

The first error you report is certainly a bug. But, the second one is legitimate -- the type Fin 1 has only 1 inhabitant, Fzero.

Confirmed reproducible in HEAD.

Yes the second error is expected, the bug seems to occur for any finite set that is too small except the smallest example:

Fzero :: Fin 0

assigned to @yav

Iavor, might you look at this, as Mr type-lits? Thanks!

Simon

changed the description

changed milestone to %7.10.1

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.

Trac metadata

Trac field	Value
Operating system	Linux → Unknown/Multiple

removed milestone

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

mentioned in commit 58b5f044

closed

I don't know which commit fixed it, but this is looking good now. I added a test.

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed
Test case	- → typecheck/should_fail/T9260

changed milestone to %8.0.1

Milestone renamed

added error messages label

added Plow label