Opened 5 years ago

Last modified 3 years ago

#9701 new bug

GADTs not specialized properly

Reported by: dfeuer Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.9
Keywords: GADTs, Inlining Cc: mpickering
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Runtime performance bug Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by dfeuer)

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

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.

Change History (15)

comment:1 Changed 5 years ago by dfeuer

Description: modified (diff)

comment:2 Changed 5 years ago by dfeuer

I think I've figured out what goes wrong here. As the comments in the source explain, there's a certain amount of redundancy between type arguments and dictionary arguments in general. The algorithm therefore ignores the type arguments and focuses on the dictionary arguments. For GADTs, this is not good enough. In particular, we can get something that looks (for a different isItSilly definition than the one above) like

GADTDict.isItSillyInt
  :: GADTDict.Silly GHC.Types.Int
     -> GADTDict.Silly GHC.Types.Int -> GADTDict.Silly GHC.Types.Int
GADTDict.isItSillyInt =
  \ (ds_dsS :: GADTDict.Silly GHC.Types.Int)
    (ds1_dsT :: GADTDict.Silly GHC.Types.Int) ->
    case ds_dsS of _ { GADTDict.Silly $dNum_apb a_ao9 ->
    case ds1_dsT of _ { GADTDict.Silly $dNum1_apc x_aoa ->
    GADTDict.Silly
      @ GHC.Types.Int
      $dNum1_apc
      (GHC.Num.+ @ GHC.Types.Int $dNum1_apc a_ao9 x_aoa)
    }
    }

Here, the compiler doesn't (currently) know what $dNum1_apc is; it's something it pulled out of a GADT constructor. But there's more information available: the GHC.Types.Int argument forces $dNum1_apc to be the Num dictionary for Int! The fix, presumably, is to recognize when a known (or collected) type argument corresponds to an unknown dictionary—when this happens, replace the dictionary with the right one. What I don't know is whether the necessary information about the correspondence is still readily available at this point.

comment:3 Changed 5 years ago 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).

comment:4 Changed 5 years ago by ekmett

Reid Barton mentioned a fairly simple scheme of skimming the core looking for terms of type C T where you have an instance C T declaration in scope with no context, and replacing those terms with the dictionary for the witness.

That could make cases like Set-carrying-a-dictionary-for-Ord optimizable for known instances.

It'd be the most specific match, should win for IncoherentInstances, doesn't collide with the (?x :: Int) case.

The trick then is selling an optimization for a style of code that currently doesn't get written.

comment:5 Changed 5 years ago 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.

comment:6 Changed 5 years ago by dfeuer

I apologize for the terribly undiplomatic tone of my last message. 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.

comment:7 in reply to:  6 Changed 5 years ago by goldfire

Replying to 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.

comment:8 in reply to:  2 Changed 5 years ago by dfeuer

Replying to dfeuer:

The algorithm therefore ignores the type arguments and focuses on the dictionary arguments.

I just re-read the comment, and I see that I read it wrong. It actually does look at the type arguments, but then it seems to miss the opportunity to grab a better dictionary. I'm not sure why that is yet.

comment:9 in reply to:  3 Changed 5 years ago by dfeuer

Replying to ekmett:

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).

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 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:

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.

comment:10 Changed 5 years ago by dfeuer

I just realized that you might not find that example as convincing as this one:

data Silly a where Silly :: Num a => a -> Silly a

double :: Int -> Int
double n = n + n

oops :: Silly Int -> Int
oops (Silly x) = double x

Now if double gets inlined, it will use the Num dictionary from Silly, but if it's not inlined, it will use the usual one.

comment:11 Changed 5 years ago 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

comment:12 in reply to:  11 Changed 5 years ago by dfeuer

Replying to simonpj:

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.

Edward Kmett raised two concerns about the sort of specialization I was trying to accomplish: that it would break implicit parameters in some fashion and that it would break incoherent instances, I was attempting to allay those concerns, the latter by showing that the incoherent ice is so thin it's just not worth worrying about—there's so little exploitable predictability about it that we shouldn't worry about making it less predictable.

comment:13 Changed 4 years ago by thomie

Keywords: GADTs added

comment:14 Changed 3 years ago by mpickering

Keywords: Inlining added

comment:15 Changed 3 years ago by mpickering

Cc: mpickering added

I agree with David here. It would be good to optimise cases like this.

Note: See TracTickets for help on using tickets.