#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