#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 maltem): I'm trying out the type-nats branch and the wiki says to complain when the solver cannot solve something, so here we go: {{{ Bug.hs:22:29: Could not deduce ((2 * n) ~ ((2 * n1) + 2)) from the context (n ~ (n1 + 1)) }}} The code is attached. I'd welcome a hint how I can work around the error (the wiki mentions that this should typically be possible, but I don't understand how). -- Ticket URL: http://hackage.haskell.org/trac/ghc/ticket/4385#comment:58 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler