[GHC] #16343: Changing an irrelevant constraint leads to inlining failure

[GHC]

#16343: Changing an irrelevant constraint leads to inlining failure
-------------------------------------+-------------------------------------
           Reporter:  mpickering     |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This is an example Andres sent me but I can't work out precisely what is
 going on.

 {{{
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE QuantifiedConstraints #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeOperators #-}
 module Tests where

 import Data.Kind
 import Data.Maybe (maybeToList)

 data Product (f :: a -> Type) (xs :: [a]) :: Type where
   Nil  :: Product f '[]
   (:*) :: f x -> !(Product f xs) -> Product f (x : xs)

 infixr 5 :*

 class Top a
 instance Top a

 class (forall d . (forall x . c x => d x) => All d xs) => All (c :: a ->
 Constraint) (xs :: [a]) where
   ccataList ::
        f '[]
     -> (forall y ys . (c y, All c ys) => f ys -> f (y : ys))
     -> f xs

 instance All c '[] where
   ccataList nil _cons = nil
   {-# INLINE ccataList #-}

 instance (c x, All c xs) => All c (x : xs) where
   ccataList nil  cons = cons (ccataList @_ @c nil cons)
   {-# INLINE ccataList #-}

 newtype (f ~> g) x = Lambda { apply :: f x -> g x }

 cpureProduct :: forall c xs f . All c xs => (forall x . c x => f x) ->
 Product f xs
 cpureProduct p =
   ccataList @_ @c
     Nil
     (p :*)
 {-# INLINE cpureProduct #-}

 newtype Apply f g x = MkApply { unApply :: Product (f ~> g) x -> Product f
 x -> Product g x }

 capplyProduct :: forall c xs f g . All c xs => Product (f ~> g) xs ->
 Product f xs -> Product g xs
 capplyProduct =
   unApply $
   ccataList @_ @c
     (MkApply (\ Nil Nil -> Nil))
     (\ rec -> MkApply (\ (f :* fs) (x :* xs) -> apply f x :* unApply rec
 fs xs))
 {-# INLINE capplyProduct #-}

 -- The addition of the constraint makes the test pass.
 mapProduct :: forall c xs f g . ({- All Top xs, -} All c xs) => (forall x
 . c x => f x -> g x) -> Product f xs -> Product g xs
 mapProduct p q =
   capplyProduct @Top (cpureProduct @c (Lambda p)) q
 {-# INLINE mapProduct #-}

 test :: Product [] [ (), (), () ]
 test =
   mapProduct @Top maybeToList (cpureProduct @Top Nothing)

 reference :: Product [] [ (), (), () ]
 reference =
   [] :* [] :* [] :* Nil
 }}}

 `test` should simplify to something close to `reference.

 There are a few ways to make it do so.

 1. Uncomment the constraint in `mapProduct`
 2. Change `Top` to `c` in `capplyProduct @Top`.

 From looking at `-ddump-inlinings`, it seems that things start to go wrong
 when `$cccataList` is inlined.

 In the good case, it looks like this.

 {{{

 Considering inlining: $cccataList_a1Bi
    arg infos [ValueArg, ValueArg, ValueArg, ValueArg, NonTrivArg,
               NonTrivArg]
    interesting continuation RhsCtxt
    some_benefit True
    is exp: True
    is work-free: True
    guidance ALWAYS_IF(arity=4,unsat_ok=False,boring_ok=False)
    ANSWER = YES
 }}}

 In the bad case it looks like

 {{{
  Considering inlining: $cccataList_a1Bv
   arg infos [ValueArg, ValueArg, ValueArg, ValueArg]
   interesting continuation RuleArgCtxt
   some_benefit True
   is exp: True
   is work-free: True
   guidance ALWAYS_IF(arity=4,unsat_ok=False,boring_ok=False)
   ANSWER = YES
 }}}

 Notice the continuation and arg infos are different for the two cases. The
 first case seems to be eta expanded?

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16343>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler