[GHC] #8422: type nats solver is too weak!
#8422: type nats solver is too weak! -------------------------------------+------------------------------------- Reporter: carter | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.8.1 Component: Compiler (Type | Version: 7.7 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- I just built ghc HEAD today, and the type nat solver can't handle the attached program, which *should* be simple to check! (and while I could use unsafeCoerce to "prove" it correct, that defeats the purpose of having the type nat solver!) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8422 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#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
#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): i tried getting solver example in the status report to work, and it doesn't :( http://ghc.haskell.org/trac/ghc/wiki/Status/Oct13 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8422#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#8422: type nats solver is too weak! -------------------------------------+------------------------------------- Reporter: carter | Owner: Type: bug | Status: new Priority: normal | Milestone: 8.0.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: TypeLits Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by thomie): * keywords: => TypeLits @@ -5,0 +5,24 @@ + + {{{#!hs + {-# LANGUAGE DataKinds #-} + {-# LANGUAGE GADTs #-} + {-# LANGUAGE KindSignatures #-} + {-# LANGUAGE TypeOperators #-} + module Fancy where + + import GHC.TypeLits + + infixr 3 :* + + data Shape (rank :: Nat) where + Nil :: Shape 0 + (:*) :: {-# UNPACK #-} !(Int :: *) -> !(Shape r) -> Shape (1 + r) + + reverseShape :: Shape r -> Shape r + reverseShape Nil = Nil + reverseShape shs = go shs Nil + where + go :: Shape a -> Shape b -> Shape (a+b) + go Nil res = res + go (ix :* more ) res = go more (ix :* res) + }}} New description: I just built ghc HEAD today, and the type nat solver can't handle the attached program, which *should* be simple to check! (and while I could use unsafeCoerce to "prove" it correct, that defeats the purpose of having the type nat solver!) {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} module Fancy where import GHC.TypeLits infixr 3 :* data Shape (rank :: Nat) where Nil :: Shape 0 (:*) :: {-# UNPACK #-} !(Int :: *) -> !(Shape r) -> Shape (1 + r) reverseShape :: Shape r -> Shape r reverseShape Nil = Nil reverseShape shs = go shs Nil where go :: Shape a -> Shape b -> Shape (a+b) go Nil res = res go (ix :* more ) res = go more (ix :* res) }}} -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8422#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC