[GHC] #4385: Type-level natural numbers

[GHC]

#4385: Type-level natural numbers
----------------------------------------+-----------------------------------
    Reporter:  diatchki                 |       Owner:  diatchki        
        Type:  feature request          |      Status:  new             
    Priority:  normal                   |   Milestone:  7.6.2           
   Component:  Compiler (Type checker)  |     Version:                  
    Keywords:                           |          Os:  Unknown/Multiple
Architecture:  Unknown/Multiple         |     Failure:  None/Unknown    
  Difficulty:                           |    Testcase:                  
   Blockedby:                           |    Blocking:                  
     Related:                           |  
----------------------------------------+-----------------------------------

Comment(by guest):

 Is there a way to make the following work?

 Couldn't match type `1 + 0' with `1'

 Here is a test to reproduce this.

  (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/4385#comment:62>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler