GitLab

{-# Language KindSignatures #-}
{-# Language PolyKinds      #-}
{-# Language RankNTypes     #-}

{-# Options_GHC -O2 -fobject-code -fstatic-argument-transformation -dcore-lint #-}

import Control.Category
import Data.Kind

apply :: Int -> (forall (ob :: Type) (cat :: ob -> ob -> Type) (a :: ob). Category cat => cat a a -> cat a a)
apply n = apply n

Gets a core lint error, I'm using GHC 9.1.0.20201202 and it seems all these flags play together. If I remove any of them it compiles fine.

$ ./ghc -ignore-dot-ghci --interactive ./4091_bug.hs
GHCi, version 9.1.0.20201202: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /home/.., /home/.. )
*** Core Lint errors : in result of Static argument ***
/home/..:11:1: warning:
    Mismatch in type between binder and occurrence
    Binder: apply_rzf :: Int
                         -> forall {ob} {cat :: ob_aF9 -> ob_aF9 -> *} {a :: ob_aF9}.
                            Category cat_aFa =>
                            cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
    Occurrence: apply :: Int
                         -> forall ob (cat :: ob -> ob -> *) (a :: ob).
                            Category cat =>
                            cat a a -> cat a a
      Before subst: Int
                    -> forall ob (cat :: ob -> ob -> *) (a :: ob).
                       Category cat =>
                       cat a a -> cat a a
    In the RHS of apply :: Int
                           -> forall ob (cat :: ob -> ob -> *) (a :: ob).
                              Category cat =>
                              cat a a -> cat a a
    In the body of lambda with binder ds_dFA :: Int
    In the body of lambda with binder ob_aF9 :: *
    In the body of lambda with binder cat_aFa :: ob_aF9 -> ob_aF9 -> *
    In the body of lambda with binder a_aFb :: ob_aF9
    In the body of lambda with binder $dCategory_aFc :: Category
                                                          cat_aFa
    In the RHS of sat_worker_sFM :: cat_aFa a_aFb a_aFb
                                    -> cat_aFa a_aFb a_aFb
    In the body of letrec with binders apply_rzf :: Int
                                                    -> forall {ob} {cat :: ob_aF9 -> ob_aF9 -> *}
                                                              {a :: ob_aF9}.
                                                       Category cat_aFa =>
                                                       cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
    In an occurrence of apply :: Int
                                 -> forall ob (cat :: ob -> ob -> *) (a :: ob).
                                    Category cat =>
                                    cat a a -> cat a a
    Substitution: [TCvSubst
                     In scope: InScope {ob_aF9 cat_aFa a_aFb}
                     Type env: [aF9 :-> ob_aF9, aFa :-> cat_aFa, aFb :-> a_aFb]
                     Co env: []]
*** Offending Program ***
apply [Occ=LoopBreaker]
  :: Int
     -> forall ob (cat :: ob -> ob -> *) (a :: ob).
        Category cat =>
        cat a a -> cat a a
[LclIdX,
 Arity=2,
 Str=<U><U>b,
 Cpr=b,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True,
         Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=True)}]
apply
  = \ (ds_dFA :: Int)
      (@ob_aF9)
      (@(cat_aFa :: ob_aF9 -> ob_aF9 -> *))
      (@(a_aFb :: ob_aF9))
      ($dCategory_aFc :: Category cat_aFa) ->
      letrec {
        sat_worker_sFM :: cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
        [LclId]
        sat_worker_sFM
          = let {
              apply_rzf
                :: Int
                   -> forall {ob} {cat :: ob_aF9 -> ob_aF9 -> *} {a :: ob_aF9}.
                      Category cat_aFa =>
                      cat_aFa a_aFb a_aFb -> cat_aFa a_aFb a_aFb
              [LclId]
              apply_rzf
                = \ (ds_sFH :: Int)
                    (@ob_sFI)
                    (@(cat_sFJ :: ob_aF9 -> ob_aF9 -> *))
                    (@(a_sFK :: ob_aF9))
                    ($dCategory_sFL :: Category cat_aFa) ->
                    sat_worker_sFM } in
            apply ds_dFA @ob_aF9 @cat_aFa @a_aFb $dCategory_aFc; } in
      sat_worker_sFM

$trModule_sFC :: Addr#
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_sFC = "main"#

$trModule_sFD :: TrName
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
$trModule_sFD = TrNameS $trModule_sFC

$trModule_sFE :: Addr#
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
$trModule_sFE = "Main"#

$trModule_sFF :: TrName
[LclId,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
$trModule_sFF = TrNameS $trModule_sFE

$trModule :: Module
[LclIdX,
 Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
         WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
$trModule = Module $trModule_sFD $trModule_sFF

*** End of Offense ***


<no location info>: error:
Compilation had errors


*** Exception: ExitFailure 1
ghci>