To be super-clear about at least one aspect: I don't want Tidy Core to ever contain something that looks like this: GADTTest.potato :: GHC.Types.Int -> GADTTest.Silly GHC.Types.Int -> GHC.Types.Int GADTTest.potato = \ (x_asZ :: GHC.Types.Int) (ds_dPR :: GADTTest.Silly GHC.Types.Int) -> case ds_dPR of _ { GADTTest.Silly $dNum_aLV ds1_dPS -> GHC.Num.+ @ GHC.Types.Int $dNum_aLV x_asZ x_asZ } Here we see GHC.Num.+ applied to GHC.Types.Int and $dNum_aLV. We therefore know that $dNum_aLV must be GHC.Num.$fNumInt, so GHC.Num.+ can eat these arguments and produce GHC.Num.$fNumInt_$c+. But for some reason, GHC fails to recognize and exploit this fact! I would like help understanding why that is, and what I can do to fix it. On Mon, Oct 20, 2014 at 7:53 AM, David Feuer wrote:

On Oct 20, 2014 5:05 AM, "Simon Peyton Jones" wrote:

...

I’m unclear what you are trying to achieve with #9701. I urge you to write a clear specification that we all agree about before burning cycles hacking code.

What I'm trying to achieve is to make specialization work in a situation where it currently does not. It appears that when the type checker determines that a GADT carries a certain dictionary, the specializer happily uses it *even once the concrete type is completely known*. What we would want to do in that case is to replace the use of the GADT-carried dictionary with a use of the known dictionary for that type.

...

There are a lot of comments at the top of Specialise.lhs. But it is, I’m afraid, a tricky pass. I could skype.

I would appreciate that. What day/time are you available?

I'll let you know as soon as I can what times I'm available Thursday/Friday. I don't know that the pattern I describe is common (now), but it's a straightforward application of constraints on GADT constructors. Whether people *like* such constraints is another question—there seem to be good reasons to use them and good reasons not to use them. At the moment, the lack of specialization is a good reason not to. You'll see the same thing if you look at the Core for the code down below the line. By the way, I tried experimentally adding {-# SPECIALIZE eval :: Expr Int -> Int #-} and got a warning about the pragma being used on a non-overloaded function. In theory, the function is not overloaded, but in practice it effectively is; I would hope to be able to do that and get a specialized version like this: evalInt :: Expr Int -> Int evalInt (N n) = n -- No B case, because Int is not Bool evalInt (Add a b) = evalNum a `+.Int` evalNum b -- Specialized addition evalInt (Mul a b) = evalNum a `*.Int` evalNum b -- Specialized multiplication -- No EqNum case, because Int is not Bool -- ---------------------------------------------- module Calc (checkInt, eval) where data Expr a where N :: Num n => n -> Expr n B :: Bool -> Expr Bool Add :: Num n => Expr n -> Expr n -> Expr n Mul :: Num n => Expr n -> Expr n -> Expr n EqNum :: (Num e, Eq e) => Expr e -> Expr e -> Expr Bool infixl 6 `Add` infixl 7 `Mul` infix 4 `EqNum` eval :: Expr a -> a eval (N n) = n eval (B b) = b eval (Add a b) = evalNum a + evalNum b eval (Mul a b) = evalNum a * evalNum b eval (EqNum a b) = evalNum a == evalNum b {-# SPECIALIZE evalNum :: Expr Int -> Int #-} evalNum :: Num a => Expr a -> a evalNum (N n) = n evalNum (Add a b) = evalNum a + evalNum b evalNum (Mul a b) = evalNum a * evalNum b {-# SPECIALIZE check :: Int -> Int -> Int -> Bool #-} check :: (Eq n, Num n) => n -> n -> n -> Bool check x y z = eval $ N x `Add` N y `Mul` N z `EqNum` N z `Mul` N y `Add` N x checkInt :: Int -> Int -> Int -> Bool checkInt x y z = check x y z On Mon, Oct 20, 2014 at 12:11 PM, Simon Peyton Jones wrote:

David

If you want to suggest a couple of possible alternative 20-min slots in work time (London time zone), not Mon-Weds this week, then maybe we can find a mutually convenient time.

Do you have reason to suppose that the pattern you describe below is common? That is, if implemented, would it make a big difference to programs we care about?

Simon

*From:* David Feuer [mailto:david.feuer@gmail.com] *Sent:* 20 October 2014 13:58 *To:* Simon Peyton Jones *Cc:* ghc-devs *Subject:* Re: Help understanding Specialise.lhs

To be super-clear about at least one aspect: I don't want Tidy Core to ever contain something that looks like this:

GADTTest.potato :: GHC.Types.Int -> GADTTest.Silly GHC.Types.Int -> GHC.Types.Int GADTTest.potato = \ (x_asZ :: GHC.Types.Int) (ds_dPR :: GADTTest.Silly GHC.Types.Int) -> case ds_dPR of _ { GADTTest.Silly $dNum_aLV ds1_dPS -> GHC.Num.+ @ GHC.Types.Int $dNum_aLV x_asZ x_asZ }

Here we see GHC.Num.+ applied to GHC.Types.Int and $dNum_aLV. We therefore know that $dNum_aLV must be GHC.Num.$fNumInt, so GHC.Num.+ can eat these arguments and produce GHC.Num.$fNumInt_$c+. But for some reason, GHC fails to recognize and exploit this fact! I would like help understanding why that is, and what I can do to fix it.

On Mon, Oct 20, 2014 at 7:53 AM, David Feuer wrote:

On Oct 20, 2014 5:05 AM, "Simon Peyton Jones" wrote:

...

I’m unclear what you are trying to achieve with #9701. I urge you to write a clear specification that we all agree about before burning cycles hacking code.

What I'm trying to achieve is to make specialization work in a situation where it currently does not. It appears that when the type checker determines that a GADT carries a certain dictionary, the specializer happily uses it *even once the concrete type is completely known*. What we would want to do in that case is to replace the use of the GADT-carried dictionary with a use of the known dictionary for that type.

...

There are a lot of comments at the top of Specialise.lhs. But it is, I’m afraid, a tricky pass. I could skype.

I would appreciate that. What day/time are you available?