#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Description changed by dfeuer: Old description:

This has probably been raised before, but I can't find a ticket. If I write

{{{#!hs data Silly a where Silly :: Ord a => a -> Silly a

isItSilly :: a -> Silly a -> Bool isItSilly a (Silly x) = a < x

isItSillyInt :: Int -> Silly Int -> Bool isItSillyInt = isItSilly }}}

then I get

{{{ isItSilly isItSilly = \ @ a_aBq eta_B2 eta1_B1 -> case eta1_B1 of _ { Silly $dOrd_aBs x_aAy -> < $dOrd_aBs eta_B2 x_aAy }

isItSillyInt isItSillyInt = isItSilly }}}

Although GHC knows that `eta_B2` is an `Int`, and `x_aAy` therefore must be one as well, it looks up the `<` method in the `eta1_B1` dictionary instead of just using `ltInt`.

New description: This has probably been raised before, but I can't find a ticket. If I write {{{#!hs data Silly a where Silly :: Ord a => a -> Silly a isItSilly :: a -> Silly a -> Bool isItSilly a (Silly x) = a < x isItSillyInt :: Int -> Silly Int -> Bool isItSillyInt = isItSilly }}} then I get {{{ isItSilly isItSilly = \ @ a_aBq eta_B2 eta1_B1 -> case eta1_B1 of _ { Silly $dOrd_aBs x_aAy -> < $dOrd_aBs eta_B2 x_aAy } isItSillyInt isItSillyInt = isItSilly }}} Although GHC knows that `eta_B2` and `x_aAy` are `Int`, it looks up the `<` method in the `eta1_B1` dictionary instead of just using `ltInt`. Note: it does not help to `INLINE` `isItSilly`. -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by ekmett): What you want here has a number of problems. 1.) It conflicts with `IncoherentInstances` by randomly changing answers based on inlining. 2.) It doesn't really interact well with the notion of typechecking producing a witness that holds the elaborated code and just using the witness. 3.) We actually '''have''' to take the "nearest" instance when you bind instances in local scope. Why? `ImplicitParams` unfortunately exist. If you have `(?x :: Int)` in scope and you come across `let ?x = 12 :: Int in ...` you need to switch to the new witness of `(?x :: Int)`. The same should work if you open a `Dict (?x :: Int)`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dfeuer): The reason I set about this whole line of thinking was the fact that `Set` cannot implement an efficient `Data.Foldable.elem` method. Wrapping a `Set` in an `Ord`-carrying GADT would enable such a thing. Unfortunately, if the GADT blocks `Ord` specialization, everything will be rather slow: comparison operators will always be looked up in the dictionary the wrapper points to, and there will be no opportunity for inlining, etc. My position regarding Incoherent Instances (and DysFunctional Dependencies) is that if your program breaks when the compiler hands you a different dictionary than you expected, you get to keep both pieces—humans invented nasal demons for a reason. I'm much more open to arguments against this idea based on implementation complexity. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:6 dfeuer]:

Thinking over the matter some more, I believe that incoherent instances already interact about as badly as they can with GADTs. Specifically, consider what will happen when GADT values coming from two different modules and carrying incoherent instances come together—if I'm not mistaken, there's no way to predict which dictionary will be chosen for any given operation combining them.

And you don't even need `-XIncoherentInstances` to cause this problem -- orphan instances are enough. Yes, you're right in that you can unpack two different instances from GADTs, and it's a tossup as to which one gets used. See #8338. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

3.) We actually '''have''' to take the "nearest" instance when you bind instances in local scope. Why? `ImplicitParams` unfortunately exist.

If you have `(?x :: Int)` in scope

and you come across `let ?x = 12 :: Int in ...` you need to switch to

#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:3 ekmett]: the new witness of `(?x :: Int)`.

The same should work if you open a `Dict (?x :: Int)`.

What am I missing here? Core distinguishes dictionaries that came from type classes from implicit parameters, doesn't it? If someone decides to implement some sort of local instance extension, as suggested by [http://okmij.org/ftp/Haskell/tr-15-04.pdf Oleg Kiselyov and Chung-chieh Shan], some restrictions are required to make anything work (as discussed in the paper). I believe the restrictions they describe would probably skirt the problem you consider, because (if my vague understanding is sufficiently correct) the types won't match where the dictionary replacement would be problematic. Also, I realized today that things can be simplified some more, and perhaps in a way you might find more convincing: {{{#!hs data Silly a where Silly :: Num a => a -> Silly a potato :: Int -> Silly Int -> Int potato x (Silly _) = x + x }}} Even here, `potato` uses the dictionary it takes from `Silly`. If there were incoherent instances in the air, this would not really be a result to be proud of. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: Runtime | Blocked By: performance bug | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Implicit parameters. They are indeed treated specially. In particular, the example in comment:10 for implicit parameters would look like this: {{{ data SillyIP a where Silly :: ?plus::(a->a->a) => a -> Silly a -- Inferred type -- double :: (?plus :: Int -> Int -> Int) => Int -> Int double n = ?plus n (n::Int) oops :: Silly Int oops (Silly x) = double x }}} There are no top-level implicit parameters, so `double`'s inferred type is as shown, and it'll pick up `plus` from the `Silly` pattern match. Reverting to the main thread, I'm not sure where this discussion is going. The base assumption is if multiple type-class instances match (e.g. from two enclosing pattern matches, comment:2, or from an enclosing patten- match and the top level) then you are on terribly thin ice is you want to predict which one will be chosen. They are all supposed to have the same value, and if they don't then, well, the ice is thin. One could try to thicken up the ice here, but it's all tangled up with the scoping of instances, overlapping instances, incoherent instances etc... My take on this: brain cycles are more productively invested elsewhere. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#9701: GADTs not specialized properly -------------------------------------+------------------------------------- Reporter: dfeuer | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.9 Resolution: | Keywords: GADTs, | Inlining Operating System: Unknown/Multiple | Architecture: Type of failure: Runtime | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by mpickering): * keywords: GADTs => GADTs, Inlining -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9701#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler