Core Lint error when building Agda-2.6.2.2 with HEAD (idArity 3 exceeds typeArity 1)

(Originally observed in a head.hackage CI job here.)

The Agda-2.6.2.2 library on Hackage fails to compile with HEAD (at commit 161a6f1f) when combined with -O and -dcore-lint. Here is a minimized example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Agda.TypeChecking.Serialise.Instances.Common (EmbPrj(..)) where

import Control.Monad.Except (ExceptT, throwError)
import Data.Array.IArray (Array, (!))
import Data.Int (Int32)
import Data.Kind (Constraint, Type)
import qualified Data.Map as M (Map, insert, lookup)
import Data.Proxy (Proxy(..))
import Data.Typeable (Typeable, TypeRep, typeRep, cast)
import Control.Monad.State.Strict (StateT, gets, modify)

class Typeable a => EmbPrj a where
  value :: Int32 -> R a

instance EmbPrj Bool where
  value = vcase valu where
    valu []  = valuN True
    valu [0] = valuN False
    valu _   = malformed

type family If (b :: Bool) (l :: k) (r :: k) :: k where
  If 'True  l r = l
  If 'False l r = r

type family All (p :: k -> Constraint) (as :: [k]) :: Constraint where
  All p '[]       = ()
  All p (a ': as) = (p a, All p as)

type family Foldr (c :: k -> l -> l) (n :: l) (as :: [k]) :: l where
  Foldr c n '[]       = n
  Foldr c n (a ': as) = c a (Foldr c n as)

type family Foldr' (c :: Function k (Function l l -> Type) -> Type)
                   (n :: l) (as :: [k]) :: l where
  Foldr' c n '[]       = n
  Foldr' c n (a ': as) = Apply (Apply c a) (Foldr' c n as)

type family Map (f :: Function k l -> Type) (as :: [k]) :: [l] where
  Map f as = Foldr' (ConsMap0 f) '[] as

data ConsMap0 :: (Function k l -> Type) -> Function k (Function [l] [l] -> Type) -> Type
data ConsMap1 :: (Function k l -> Type) -> k -> Function [l] [l] -> Type
type instance Apply (ConsMap0 f)    a = ConsMap1 f a
type instance Apply (ConsMap1 f a) tl = Apply f a ': tl

type family Constant (b :: l) (as :: [k]) :: [l] where
  Constant b as = Map (Constant1 b) as

type Arrows   (as :: [Type]) (r :: Type) = Foldr (->) r as
type Products (as :: [Type])             = Foldr (,) () as

type family IsBase (t :: Type) :: Bool where
  IsBase (a -> t) = 'False
  IsBase a        = 'True

type family Domains (t :: Type) :: [Type] where
  Domains t = If (IsBase t) '[] (Domains' t)
type family Domains' (t :: Type) :: [Type] where
  Domains' (a -> t) = a ': Domains t

type family CoDomain (t :: Type) :: Type where
  CoDomain t = If (IsBase t) t (CoDomain' t)
type family CoDomain' (t :: Type) :: Type where
  CoDomain' (a -> t) = CoDomain t

class Currying as b where
  uncurrys :: Proxy as -> Proxy b -> Arrows as b -> Products as -> b
  currys   :: Proxy as -> Proxy b -> (Products as -> b) -> Arrows as b

instance Currying '[] b where
  uncurrys _ _ f = \ () -> f
  currys   _ _ f = f ()

instance Currying as b => Currying (a ': as) b where
  uncurrys _ p f = uncurry $ uncurrys (Proxy :: Proxy as) p . f
  currys   _ p f = currys (Proxy :: Proxy as) p . curry f

data Function :: Type -> Type -> Type

data Constant0 :: Function a (Function b a -> Type) -> Type
data Constant1 :: Type -> Function b a -> Type

type family Apply (t :: Function k l -> Type) (u :: k) :: l

type instance Apply Constant0     a = Constant1 a
type instance Apply (Constant1 a) b = a

type Node = [Int32]

type Table k v = M.Map k v

data U = forall a . Typeable a => U !a

type Memo = Table (Int32, TypeRep) U

data St = St
  { nodeE     :: !(Array Int32 Node)
  , nodeMemo  :: !Memo
  }

data TypeError = GenericError String

type R a = ExceptT TypeError (StateT St IO) a

malformed :: R a
malformed = throwError $ GenericError "Malformed input."

{-# INLINE vcase #-}
vcase :: forall a . EmbPrj a => (Node -> R a) -> Int32 -> R a
vcase valu = \ix -> do
    memo <- gets nodeMemo
    let aTyp = typeRep (Proxy :: Proxy a)
    let maybeU = M.lookup (ix, aTyp) memo
    case maybeU of
      Just (U u) -> maybe malformed return (cast u)
      Nothing    -> do
          v <- valu . (! ix) =<< gets nodeE
          modify $ \s -> s { nodeMemo = M.insert (ix, aTyp) (U v) memo }
          return v

class VALU t b where
  valuN' :: b ~ IsBase t =>
            All EmbPrj (Domains t) =>
            t -> Products (Constant Int32 (Domains t)) -> R (CoDomain t)

instance VALU t 'True where
  valuN' c () = return c

{-# INLINE valuN #-}
valuN :: forall t. VALU t (IsBase t) =>
         Currying (Constant Int32 (Domains t)) (R (CoDomain t)) =>
         All EmbPrj (Domains t) =>
         t -> Arrows (Constant Int32 (Domains t)) (R (CoDomain t))
valuN f = currys (Proxy :: Proxy (Constant Int32 (Domains t)))
                 (Proxy :: Proxy (R (CoDomain t)))
                 (valuN' f)

With GHC 9.4 and earlier, this GHC invocation succeeds:

$ ghc-9.4 Bug.hs -fforce-recomp -dcore-lint -O
[1 of 1] Compiling Agda.TypeChecking.Serialise.Instances.Common ( Bug.hs, Bug.o )

With HEAD, however, this produces a Core Lint error:

$ ~/Software/ghc-9.5.20220827/bin/ghc Bug.hs -fforce-recomp -dcore-lint -O
[1 of 1] Compiling Agda.TypeChecking.Serialise.Instances.Common ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    idArity 3 exceeds typeArity 1: fail_d26u
    In the RHS of valu_s2B8 :: [Int32]
                               -> Foldr
                                    (->)
                                    (ExceptT TypeError (StateT St IO) (CoDomain Bool))
                                    (Constant Int32 (Domains Bool))
    In the body of lambda with binder ds_d26j :: [Int32]
    Substitution: <InScope = {}
                   IdSubst   = []
                   TvSubst   = []
                   CvSubst   = []>

The full Core Lint error is quite long, so I've attached it separately here: agda-core-lint-error.txt