Skip to content

SPECIALISE instance does not specialize as far as SPECIALISE for type signatures

type FreeM c = Reader (FreeEnv c) c

class Free' a c where
  freeVars' :: (Monoid c) => a -> FreeM c

instance (Free' a c, Free' b c) => Free' (a,b) c where
  {-# SPECIALIZE instance (Free' a All, Free' b All) => Free' (a,b) All #-}
  {-# SPECIALIZE freeVars' :: (Free' a Any, Free' b Any) => (a,b) -> FreeM Any #-}
  freeVars' (x,y) = freeVars' x `mappend` freeVars' y

I would expect these two specialize pragmas to work similarily. However, the interface file shows that the mappend for Any has been inlined, but not the one for All. If you look at the .hi file dump below, you see

Data.Monoid.mappend
                      @ Data.Monoid.All
                      $dMonoid

generated by the SPECIALIZE instance, and

     case (...) of wild1 {
                      GHC.Types.False
                      -> eta1
                           `cast`
                         (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                              <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any>_R
                              <Data.Functor.Identity.Identity>_R
                              <Data.Monoid.Any>_N)
                           eta2
                      GHC.Types.True
                      -> GHC.Types.True

generated by the SPECIALIZE for the type signature. For All, mappend is called from the dictionary dMonoid, which is still passed around, whereas for Any, the disjunction has been inlined.

  $fFree'(,)c_$s$cfreeVars' :: Agda.TypeChecking.Free.Lazy.Free'
                                   a Data.Monoid.All
                               -> Agda.TypeChecking.Free.Lazy.Free' b Data.Monoid.All
                               -> Data.Monoid.Monoid Data.Monoid.All
                               -> (a, b)
                               -> Agda.TypeChecking.Free.Lazy.FreeM Data.Monoid.All
    {- Arity: 4, HasNoCafRefs,
       Strictness: <L,1*C1(C1(U))><L,1*C1(C1(U))><L,U(U,U,U)><S,1*U(U,U)>,
       Unfolding: InlineRule (4, True, False)
                  (\ @ a
                     @ b
                     $dFree' :: Agda.TypeChecking.Free.Lazy.Free' a Data.Monoid.All
                     $dFree'1 :: Agda.TypeChecking.Free.Lazy.Free' b Data.Monoid.All
                     $dMonoid :: Data.Monoid.Monoid Data.Monoid.All
                     ds :: (a, b) ->
                   case ds of wild { (,) x y ->
                   let {
                     eta :: Control.Monad.Trans.Reader.ReaderT
                                (Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All)
                                Data.Functor.Identity.Identity
                                Data.Monoid.All
                     = $dFree'
                         `cast`
                       (Agda.TypeChecking.Free.Lazy.NTCo:Free'[0]
                            <a>_N <Data.Monoid.All>_N)
                         $dMonoid
                         x
                   } in
                   let {
                     eta1 :: Control.Monad.Trans.Reader.ReaderT
                                 (Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All)
                                 Data.Functor.Identity.Identity
                                 Data.Monoid.All
                     = $dFree'1
                         `cast`
                       (Agda.TypeChecking.Free.Lazy.NTCo:Free'[0]
                            <b>_N <Data.Monoid.All>_N)
                         $dMonoid
                         y
                   } in
                   (\ eta2 :: Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All ->
                    Data.Monoid.mappend
                      @ Data.Monoid.All
                      $dMonoid
                      (eta
                         `cast`
                       (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                            <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All>_R
                            <Data.Functor.Identity.Identity>_R
                            <Data.Monoid.All>_N)
                         eta2)
                        `cast`
                      (Data.Functor.Identity.NTCo:Identity[0] <Data.Monoid.All>_R)
                      (eta1
                         `cast`
                       (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                            <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All>_R
                            <Data.Functor.Identity.Identity>_R
                            <Data.Monoid.All>_N)
                         eta2)
                        `cast`
                      (Data.Functor.Identity.NTCo:Identity[0] <Data.Monoid.All>_R))
                     `cast`
                   (Trans
                        (<Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All>_R
                         ->_R Sym (Data.Functor.Identity.NTCo:Identity[0]
                                       <Data.Monoid.All>_R))
                        (Sym (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                                  <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.All>_R
                                  <Data.Functor.Identity.Identity>_R
                                  <Data.Monoid.All>_N))) }) -}
2292db791a93ca783c0315a38fa7d8f1
  $fFree'(,)c_$s$cfreeVars'1 :: Agda.TypeChecking.Free.Lazy.Free'
                                    a Data.Monoid.Any
                                -> Agda.TypeChecking.Free.Lazy.Free' b Data.Monoid.Any
                                -> (a, b)
                                -> Agda.TypeChecking.Free.Lazy.FreeM Data.Monoid.Any
    {- Arity: 3, HasNoCafRefs,
       Strictness: <L,1*C1(C1(U))><L,1*C1(C1(U))><S,1*U(U,U)>,
       Unfolding: InlineRule (3, True, False)
                  (\ $dFree' :: Agda.TypeChecking.Free.Lazy.Free' a Data.Monoid.Any
                     $dFree'1 :: Agda.TypeChecking.Free.Lazy.Free' b Data.Monoid.Any
                     ds :: (a, b) ->
                   case ds of wild { (,) x y ->
                   let {
                     eta :: Control.Monad.Trans.Reader.ReaderT
                                (Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any)
                                Data.Functor.Identity.Identity
                                Data.Monoid.Any
                     = $dFree'
                         `cast`
                       (Agda.TypeChecking.Free.Lazy.NTCo:Free'[0]
                            <a>_N <Data.Monoid.Any>_N)
                         Data.Monoid.$fMonoidAny
                         x
                   } in
                   let {
                     eta1 :: Control.Monad.Trans.Reader.ReaderT
                                 (Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any)
                                 Data.Functor.Identity.Identity
                                 Data.Monoid.Any
                     = $dFree'1
                         `cast`
                       (Agda.TypeChecking.Free.Lazy.NTCo:Free'[0]
                            <b>_N <Data.Monoid.Any>_N)
                         Data.Monoid.$fMonoidAny
                         y
                   } in
                   (\ eta2 :: Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any ->
                    case (eta
                            `cast`
                          (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                               <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any>_R
                               <Data.Functor.Identity.Identity>_R
                               <Data.Monoid.Any>_N)
                            eta2)
                           `cast`
                         (Data.Functor.Identity.NTCo:Identity[0]
                              (Data.Monoid.NTCo:Any[0])) of wild1 {
                      GHC.Types.False
                      -> eta1
                           `cast`
                         (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                              <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any>_R
                              <Data.Functor.Identity.Identity>_R
                              <Data.Monoid.Any>_N)
                           eta2
                      GHC.Types.True
                      -> GHC.Types.True
                           `cast`
                         (Sym (Data.Functor.Identity.NTCo:Identity[0]
                                   (Data.Monoid.NTCo:Any[0]))) })
                     `cast`
                   (Sym (Control.Monad.Trans.Reader.NTCo:ReaderT[0]
                             <Agda.TypeChecking.Free.Lazy.FreeEnv Data.Monoid.Any>_R
                             <Data.Functor.Identity.Identity>_R
                             <Data.Monoid.Any>_N)) }) -}
2292db791a93ca783c0315a38fa7d8f1
Trac metadata
Trac field Value
Version 7.8.3
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information