[GHC] #10321: GHC.TypeLits.Nat types no longer fully simplified.

18 Apr 2015

      #10321: GHC.TypeLits.Nat types no longer fully simplified.
-------------------------------------+-------------------------------------
              Reporter:  darchon     |             Owner:
                  Type:  bug         |            Status:  new
              Priority:  normal      |         Milestone:  7.10.2
             Component:  Compiler    |           Version:  7.10.1
  (Type checker)                     |  Operating System:  Unknown/Multiple
              Keywords:  TypeLits    |   Type of failure:  Other
          Architecture:              |        Blocked By:
  Unknown/Multiple                   |   Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10321
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler