Changing an irrelevant constraint leads to inlining failure

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?

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture