#9260: Unnecessary error using GHC.TypeLits -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | 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: -------------------------------------+------------------------------------- Comment (by Iceland_jack): Forgot to add the actual failing case: {{{ test :: Fin 1 test = Fsucc Fzero }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9260#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9260: Unnecessary error using GHC.TypeLits -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: bug | Status: new Priority: low | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | 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: -------------------------------------+------------------------------------- Comment (by Iceland_jack): 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9260#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#9260: Unnecessary error using GHC.TypeLits -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: diatchki Type: bug | Status: closed Priority: low | Milestone: 7.12.1 Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: type lits, | data kinds, error message Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: Incorrect | Test Case: warning at compile-time | typecheck/should_fail/T9260 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thomie): * status: new => closed * testcase: => typecheck/should_fail/T9260 * resolution: => fixed Comment: I don't know which commit fixed it, but this is looking good now. I added a test. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9260#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler