[GHC] #8019: Can't match type `1+0` with `1`. (TypeNats addition doesn't reduce)

28 Jun 2013


      #8019: Can't match type `1+0` with `1`. (TypeNats addition doesn't reduce)
--------------------------------------+-------------------------------------
Reporter:  guest                      |          Owner:                    
    Type:  bug                        |         Status:  new               
Priority:  normal                     |      Component:  libraries/base    
 Version:  7.6.3                      |       Keywords:  TypeNats, addition
      Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple  
 Failure:  GHC rejects valid program  |      Blockedby:                    
Blocking:                             |        Related:                    
--------------------------------------+-------------------------------------
 Here are two examples illustrating my problem:

 (test2 and test3 produce the errors when the line that don't work are
 uncommented)
 This is a file:

 --file: Scratch.hs
 {-# Language DataKinds, KindSignatures, TypeOperators #-}

 import GHC.TypeLits

 test1 = sing :: Sing (1) --works

 --test2 = sing :: Sing (1+0) --doesn't

 data F (n::Nat) = F ()

 f :: F n -> F n -> ()
 f _ _ = ()

 x = F () :: F (1) --works

 --x = F () :: F (1+0) --doesn't

 y = F () :: F (1)

 test3 = f x y

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