#8422: type nats solver is too weak! ----------------------------------------------+---------------------------- Reporter: carter | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.8.1 Component: Compiler (Type checker) | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects valid program | Unknown/Multiple Test Case: | Difficulty: Unknown Blocking: | Blocked By: | Related Tickets: ----------------------------------------------+---------------------------- Comment (by carter): the error in question is {{{ Fancy.hs:58:35: Could not deduce ((r2 + (1 + b)) ~ (a + b)) from the context (r ~ (1 + r1)) bound by a pattern with constructor :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r), in an equation for ‛reverseShape’ at Fancy.hs:54:19-30 or from (a ~ (1 + r2)) bound by a pattern with constructor :* :: forall (r :: Nat). Int -> Shape r -> Shape (1 + r), in an equation for ‛go’ at Fancy.hs:58:13-22 NB: ‛+’ is a type function, and may not be injective Expected type: Shape (a + b) Actual type: Shape (r2 + (1 + b)) Relevant bindings include res :: Shape b (bound at Fancy.hs:58:27) more :: Shape r2 (bound at Fancy.hs:58:19) go :: Shape a -> Shape b -> Shape (a + b) (bound at Fancy.hs:57:9) In the expression: go more (ix :* res) In an equation for ‛go’: go (ix :* more) res = go more (ix :* res) }}} in one case , the solver should be able to deduce that 0+b = b ===> b = r and in the other case that a = a_1+1 then (a+b =r ) implies a_1 + b +1=r or something like that -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8422#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler