GHC.TypeLits.Nat types no longer fully simplified.
The following code:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n + 1) a
infixr 5 :>
when loaded in GHCi 7.8.3, and asking for the type of (1 :> 2 :> 3 :> Nil)
, gives:
$ ghci example/vec.hs
GHCi, version 7.8.3: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec 3 a
while in GHCi 7.10.1 it gives:
$ ghci example/vec.hs
GHCi, version 7.10.1: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
That is, the type-level computation, ((0 + 1) + 1) + 1
is only simplified to 2 + 1
in GHC 7.10.1, whereas in 7.8.3 2+1
was further simplified to 3
.
The same still happens in HEAD (20150417)
$ ghci example/vec.hs
GHCi, version 7.11.20150417: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( example/vec.hs, interpreted )
Ok, modules loaded: Main.
*Main> :t (3:>4:>5:>Nil)
(3:>4:>5:>Nil) :: Num a => Vec (2 + 1) a
I strongly feel that the behaviour in ghc 7.8.3 is the desired behaviour.
Trac metadata
Trac field | Value |
---|---|
Version | 7.10.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |