[GHC] #10177: Typeable solver regression
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler | Version: 7.10.1-rc3 (Type checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: | valid program Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- This bug is known and fixed in master. Simon and Austin and Iavor are all aware of it. This ticket exists to ensure that the fix doesn't get lost. This code breaks under the Typeable solver in 7.10.1-rc3 and is fixed in master. The relevant commit in master is 3a0019e3672097761e7ce09c811018f774febfd2 : Improve `Typeable` solver. {{{ {-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleContexts #-} module Bug where import Data.Typeable newtype V n a = V [a] class Typeable a => C a instance (Typeable (V n), Typeable a) => C (V n a) -- Bug.hs:13:10: -- Could not deduce (Typeable (V n a)) -- arising from the superclasses of an instance declaration -- from the context (Typeable (V n), Typeable a) -- bound by the instance declaration at Bug.hs:13:10-50 -- In the instance declaration for ‘C (V n a)’ }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: closed Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Changes (by glguy): * status: new => closed * resolution: => fixed Comment: I just saw this was merged -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: closed Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | Blocking: Blocked By: | Differential Revisions: Related Tickets: | -------------------------------------+------------------------------------- Comment (by hvr): merged to ghc-7.10 via 32a5d959ea47f0ebd3231d41d77c4dd13c138658 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression
-------------------------------------+-------------------------------------
Reporter: glguy | Owner:
Type: bug | Status: closed
Priority: highest | Milestone: 7.10.1
Component: Compiler (Type | Version: 7.10.1-rc3
checker) | Keywords:
Resolution: fixed | Architecture:
Operating System: Unknown/Multiple | Unknown/Multiple
Type of failure: GHC rejects | Test Case:
valid program | Blocking:
Blocked By: | Differential Revisions:
Related Tickets: |
-------------------------------------+-------------------------------------
Comment (by Austin Seipp
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: closed Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thoughtpolice): * testcase: => testsuite/tests/typecheck/should_compile/T10177 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: closed => new * resolution: fixed => Comment: Actually I really don't think this code should work. It should be {{{ instance (Typeable n, Typeable a) => C (V n a) }}} Otherwise there is an overlap between the given `(Typeable (V n))` and the built-in instance for `Typeable (V n a)`. Making the code given here work is very fragile, and might depend on solve order. I vote that should fail. Any dissenters? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): What about this? {{{ instance (Typeable a, Typeable b) => C (a b) }}} That looks good to me. But what you have above is just a simple substitution on my instance, so I think it should be good. Can the `Typeable` solver just immediately decompose `Typeable (V n)` to `Typeable n`? Is there a threat that the overlapping instances are semantically different? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by diatchki): I don't think that there is anything wrong here, so I think that we should accept the program. The (new, now merged) `Typeable` solver does exactly what Richard says. The instance for `Typeable (f a)` has to be computed from the evidence for the types `f` and `a`. If that was not the case, we'd get some very odd behavior depending on how type variables get instantiated. Now, if `f` happened to be a concrete type (e.g., like `V n`), then we can reduce further, but if we happen to already have a solution for `V n`, we don't have to reduce any further---after all, ''that'' solution must have been built by the internal typeable solver in the first place. Note that the actual `TypeRep`s are built by always applying the constructor to all arguments: see the comment on `mkAppTy` in `Data.Typeable.Internal`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by hvr): * milestone: 7.10.1 => 7.10.2 Comment: GHC 7.10.1 was just released, so any change can occur in milestone:7.10.2 earliest (if it turns out there's nothing to change, please revert back to the 7.10.1 milestone) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.10.2 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Austin: check that this works on the 7.10 branch; assuming that it does, re-milestone for 7.12. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: new Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by thoughtpolice): * milestone: 7.10.2 => 7.12.1 Comment: Confirmed working on 7.10.1, so we can punt this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10177: Typeable solver regression -------------------------------------+------------------------------------- Reporter: glguy | Owner: Type: bug | Status: closed Priority: highest | Milestone: 7.12.1 Component: Compiler (Type | Version: 7.10.1-rc3 checker) | Keywords: Resolution: fixed | Architecture: Operating System: Unknown/Multiple | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | testsuite/tests/typecheck/should_compile/T10177 Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * resolution: => fixed Comment: Actually it's fine in HEAD and should stay that way, i.e. NOT as I said in comment:5. See `Note [Instance and Given overlap]` in `TcInteract`. I'll close as fixed. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10177#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC