#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