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