[GHC] #10075: Muddling Constraint and * means that Core is inconsistent
#10075: Muddling Constraint and * means that Core is inconsistent -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Blocked By: Test Case: | Related Tickets: Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- I can say this: {{{ type family F (a :: k) type instance F (a :: Constraint) = Int type instance F (a :: *) = Bool }}} This compiles to the following Core: {{{ F :: forall (k :: BOX). k -> * axF1 :: [a :: Constraint].F Constraint a ~ Int axF2 :: [a :: *]. F * a ~ Bool }}} I can then build the following: {{{ sym axF1[Any Constraint] ; axF2[Any *] :: Int ~ Bool }}} The transitivity is sound because, in Core, `Constraint` and `*` are indistinguishable. I don't think there's a way to actually cause a bug in a running program due to this problem, but we should probably patch it up. Possible resolution: Have `coreView` change `Constraint` to `*`. Possible resolution once we have `* :: *`: Make `Constraint` and `*` representationally equal. In other words, it would be as if `Constraint` were a newtype around `*`. I haven't thought out the ramifications of this decision, but there's something nice about it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10075 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10075: Muddling Constraint and * means that Core is inconsistent -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by simonpj): Ha! Good point! I like your newtype idea. I don't understand the `coreView` idea. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10075#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10075: Muddling Constraint and * means that Core is inconsistent -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by goldfire): If running `coreView` -- the function that unwraps type synonyms before inspecting a type -- also returned `Just *` when given `Constraint`, I think the problem would be solved. This essentially treats `Constraint` as a type synonym for `*` in `coreView`, but not in `tcView`. On the other hand, if we implemented this `coreView` idea, then my example code wouldn't compile, as the type instances would overlap. From a Haskell (as opposed to Core) point of view, the overlap here would be strange, as `Constraint` and `*` ''are'' distinct in Haskell. Perhaps we really do need kind equalities to sort this one out... :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10075#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#10075: Muddling Constraint and * means that Core is inconsistent -------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * status: new => closed * resolution: => duplicate Comment: This has been re-reported as #11715, but the discussion there is better than the discussion here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10075#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC