Core Lint error when compiling singletons (HEAD only), possibly due to nested foralls
I originally observed this bug in head.hackage
when compiling the singletons-2.6
library with GHC HEAD. Minimizing the issue is tricky, and the smallest reproducer I've managed to create is still pretty long. Here it is:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
module Bug where
import Data.Kind
import qualified Data.Text as T
import Data.Text (Text)
import Data.Proxy
import GHC.TypeLits
import Unsafe.Coerce
type SingFunction1 f = forall t. Sing t -> Sing (f `Apply` t)
singFun1 :: forall f. SingFunction1 f -> Sing f
singFun1 f = SLambda f
-- type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
singFun2 :: forall f. SingFunction2 f -> Sing f
singFun2 f = SLambda (\x -> singFun1 (f x))
-- type SingFunction3 f = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
type SingFunction3 f = forall t1. Sing t1 -> forall t2. Sing t2 -> forall t3. Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
singFun3 :: forall f. SingFunction3 f -> Sing f
singFun3 f = SLambda (\x -> singFun2 (f x))
type family Sing :: k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type SameKind (a :: k) (b :: k) = (() :: Constraint)
class SingKind k where
type Demote k = (r :: Type) | r -> k
fromSing :: Sing (a :: k) -> Demote k
toSing :: Demote k -> SomeSing k
class SingI a where
sing :: Sing a
data SList :: forall a. [a] -> Type where
SNil :: SList '[]
SCons :: Sing x -> Sing xs -> SList (x:xs)
type instance Sing = SList
data SSymbol (n :: Symbol) = KnownSymbol n => SSym
type instance Sing = SSymbol
instance KnownSymbol n => SingI n where
sing = SSym
instance SingKind Symbol where
type Demote Symbol = Text
fromSing (SSym :: Sing n) = T.pack (symbolVal (Proxy :: Proxy n))
toSing s = case someSymbolVal (T.unpack s) of
SomeSymbol (_ :: Proxy n) -> SomeSing (SSym :: Sing n)
newtype SLambda (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
type instance Sing = SLambda
type family ((f :: b ~> c) . (g :: a ~> b)) (x :: a) :: c where
(f . g) x = f `Apply` (g `Apply` x)
data (.@#@$) :: (b ~> c) ~> (a ~> b) ~> a ~> c
data (.@#@$$) :: (b ~> c) -> (a ~> b) ~> a ~> c
data (.@#@$$$) :: (b ~> c) -> (a ~> b) -> a ~> c
type instance Apply (.@#@$) f = (.@#@$$) f
type instance Apply ((.@#@$$) f) g = f .@#@$$$ g
type instance Apply (f .@#@$$$ g) x = (f . g) x
(%.) :: Sing f -> Sing g -> Sing x -> Sing ((f . g) x)
(sF %. sG) sX = sF `applySing` (sG `applySing` sX)
class PSemigroup a where
type (x :: a) <> (y :: a) :: a
data (<>@#@$) :: a ~> a ~> a
data (<>@#@$$) :: a -> a ~> a
type instance Apply (<>@#@$) x = (<>@#@$$) x
type instance Apply ((<>@#@$$) x) y = x <> y
class SSemigroup a where
(%<>) :: forall (x :: a) (y :: a). Sing x -> Sing y -> Sing (x <> y)
instance PSemigroup Symbol where
type a <> b = AppendSymbol a b
instance SSemigroup Symbol where
sa %<> sb =
let a = fromSing sa
b = fromSing sb
ex = someSymbolVal $ T.unpack $ a <> b
in case ex of
SomeSymbol (_ :: Proxy ab) -> unsafeCoerce (SSym :: Sing ab)
type family Foldr1 (f :: a ~> a ~> a) (l :: [a]) :: a where
Foldr1 _ '[x] = x
Foldr1 f (x:y:ys) = f `Apply` x `Apply` (Foldr1 f (y:ys))
data Foldr1Sym0 :: (a ~> a ~> a) ~> [a] ~> a
data Foldr1Sym1 :: (a ~> a ~> a) -> [a] ~> a
type instance Apply Foldr1Sym0 f = Foldr1Sym1 f
type instance Apply (Foldr1Sym1 f) l = Foldr1 f l
sFoldr1 :: Sing f -> Sing l -> Sing (Foldr1 f l)
sFoldr1 _ (sX `SCons` SNil) = sX
sFoldr1 sF (sX `SCons` sXs@(_ `SCons` _)) = sF `applySing` sX `applySing` (sFoldr1 sF sXs)
sFoldr1 _ _ = error "empty list"
type family Lambda_6989586621679111672_aqvf ss_aqvc a_6989586621679111668_aqvd t_aqvi t_aqvj where
Lambda_6989586621679111672_aqvf ss_aqvc a_6989586621679111668_aqvd s_aqvg r_aqvh = Apply (Apply (.@#@$) s_aqvg) (Apply (Apply (.@#@$) (Apply ShowCharSym0 ",")) r_aqvh)
type Lambda_6989586621679111672Sym4 ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676 t6989586621679111677 =
Lambda_6989586621679111672_aqvf ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676 t6989586621679111677
data Lambda_6989586621679111672Sym3 ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676 t6989586621679111677
type instance Apply (Lambda_6989586621679111672Sym3 t6989586621679111676 a_69895866216791116686989586621679111671 ss6989586621679111670) t6989586621679111677 = Lambda_6989586621679111672_aqvf t6989586621679111676 a_69895866216791116686989586621679111671 ss6989586621679111670 t6989586621679111677
data Lambda_6989586621679111672Sym2 ss6989586621679111670 a_69895866216791116686989586621679111671 t6989586621679111676
type instance Apply (Lambda_6989586621679111672Sym2 a_69895866216791116686989586621679111671 ss6989586621679111670) t6989586621679111676 = Lambda_6989586621679111672Sym3 a_69895866216791116686989586621679111671 ss6989586621679111670 t6989586621679111676
data Lambda_6989586621679111672Sym1 ss6989586621679111670 a_69895866216791116686989586621679111671
type instance Apply (Lambda_6989586621679111672Sym1 ss6989586621679111670) a_69895866216791116686989586621679111671 = Lambda_6989586621679111672Sym2 ss6989586621679111670 a_69895866216791116686989586621679111671
data Lambda_6989586621679111672Sym0 ss6989586621679111670
type instance Apply Lambda_6989586621679111672Sym0 ss6989586621679111670 = Lambda_6989586621679111672Sym1 ss6989586621679111670
type Show_tupleSym2 (a6989586621679111664 :: [(~>) Symbol Symbol]) (a6989586621679111665 :: Symbol) =
Show_tuple a6989586621679111664 a6989586621679111665
data Show_tupleSym1 (a6989586621679111664 :: [(~>) Symbol Symbol]) :: (~>) Symbol Symbol
type instance Apply (Show_tupleSym1 a6989586621679111664) a6989586621679111665 = Show_tuple a6989586621679111664 a6989586621679111665
data Show_tupleSym0 :: (~>) [(~>) Symbol Symbol] ((~>) Symbol Symbol)
type instance Apply Show_tupleSym0 a6989586621679111664 = Show_tupleSym1 a6989586621679111664
type ShowStringSym2 (a6989586621679111686 :: Symbol) (a6989586621679111687 :: Symbol) =
ShowString a6989586621679111686 a6989586621679111687
data ShowStringSym1 (a6989586621679111686 :: Symbol) :: (~>) Symbol Symbol
type instance Apply (ShowStringSym1 a6989586621679111686) a6989586621679111687 = ShowString a6989586621679111686 a6989586621679111687
data ShowStringSym0 :: (~>) Symbol ((~>) Symbol Symbol)
type instance Apply ShowStringSym0 a6989586621679111686 = ShowStringSym1 a6989586621679111686
type ShowCharSym2 (a6989586621679111696 :: Symbol) (a6989586621679111697 :: Symbol) =
ShowChar a6989586621679111696 a6989586621679111697
data ShowCharSym1 (a6989586621679111696 :: Symbol) :: (~>) Symbol Symbol
type instance Apply (ShowCharSym1 a6989586621679111696) a6989586621679111697 = ShowChar a6989586621679111696 a6989586621679111697
data ShowCharSym0 :: (~>) Symbol ((~>) Symbol Symbol)
type instance Apply ShowCharSym0 a6989586621679111696 = ShowCharSym1 a6989586621679111696
type family Show_tuple (a_aqv6 :: [(~>) Symbol Symbol]) (a_aqv7 :: Symbol) :: Symbol where
Show_tuple ss_aqvc a_6989586621679111668_aqvd = Apply (Apply (Apply (.@#@$) (Apply ShowCharSym0 "(")) (Apply (Apply (.@#@$) (Apply (Apply Foldr1Sym0 (Apply (Apply Lambda_6989586621679111672Sym0 ss_aqvc) a_6989586621679111668_aqvd)) ss_aqvc)) (Apply ShowCharSym0 ")"))) a_6989586621679111668_aqvd
type family ShowString (a_aqvs :: Symbol) (a_aqvt :: Symbol) :: Symbol where
ShowString a_6989586621679111682_aqvw a_6989586621679111684_aqvx = Apply (Apply (<>@#@$) a_6989586621679111682_aqvw) a_6989586621679111684_aqvx
type family ShowChar (a_aqvC :: Symbol) (a_aqvD :: Symbol) :: Symbol where
ShowChar a_6989586621679111692_aqvG a_6989586621679111694_aqvH = Apply (Apply (<>@#@$) a_6989586621679111692_aqvG) a_6989586621679111694_aqvH
sShow_tuple ::
forall (t_aqvI :: [(~>) Symbol Symbol]) (t_aqvJ :: Symbol).
Sing t_aqvI
-> Sing t_aqvJ
-> Sing (Show_tuple t_aqvI t_aqvJ)
sShowString ::
forall (t_aqvM :: Symbol) (t_aqvN :: Symbol).
Sing t_aqvM
-> Sing t_aqvN
-> Sing (ShowString t_aqvM t_aqvN)
sShowChar ::
forall (t_aqvQ :: Symbol) (t_aqvR :: Symbol).
Sing t_aqvQ
-> Sing t_aqvR
-> Sing (ShowChar t_aqvQ t_aqvR)
sShow_tuple
(sSs :: Sing ss_aqvc)
(sA_6989586621679111668 :: Sing a_6989586621679111668_aqvd)
= (applySing
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing ((singFun2 @ShowCharSym0) sShowChar))
(sing :: Sing "("))))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing
((applySing ((singFun2 @Foldr1Sym0) sFoldr1))
((singFun2
@(Apply (Apply Lambda_6989586621679111672Sym0 ss_aqvc) a_6989586621679111668_aqvd))
(\ sS sR
-> case ((,) sS) sR of {
(,) (_ :: Sing s_aqvg) (_ :: Sing r_aqvh)
-> (applySing ((applySing ((singFun3 @(.@#@$)) (%.))) sS))
((applySing
((applySing ((singFun3 @(.@#@$)) (%.)))
((applySing
((singFun2 @ShowCharSym0) sShowChar))
(sing :: Sing ","))))
sR) }))))
sSs)))
((applySing ((singFun2 @ShowCharSym0) sShowChar))
(sing :: Sing ")")))))
sA_6989586621679111668
sShowString
(sA_6989586621679111682 :: Sing a_6989586621679111682_aqvw)
(sA_6989586621679111684 :: Sing a_6989586621679111684_aqvx)
= (applySing
((applySing ((singFun2 @(<>@#@$)) (%<>))) sA_6989586621679111682))
sA_6989586621679111684
sShowChar
(sA_6989586621679111692 :: Sing a_6989586621679111692_aqvG)
(sA_6989586621679111694 :: Sing a_6989586621679111694_aqvH)
= (applySing
((applySing ((singFun2 @(<>@#@$)) (%<>))) sA_6989586621679111692))
sA_6989586621679111694
instance SingI (ShowStringSym0 :: (~>) Symbol ((~>) Symbol Symbol)) where
sing = (singFun2 @ShowStringSym0) sShowString
This passes Core Lint on GHC 8.8.3 and 8.10.1-rc1, but not on HEAD:
$ ~/Software/ghc5/inplace/bin/ghc-stage2 -dcore-lint Bug.hs -fprint-explicit-kinds
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:174:34: warning:
Kind application error in type ‘Sing @Symbol t_X5’
Function kind = forall k. k -> *
Arg kinds = [(Symbol, *), (t_X5, Symbol ~> Symbol)]
Fun: Symbol
(t_X5, Symbol ~> Symbol)
In the RHS of sShow_tuple :: forall (t_aqvI :: [Symbol ~> Symbol])
(t_aqvJ :: Symbol).
Sing @[Symbol ~> Symbol] t_aqvI
-> Sing @Symbol t_aqvJ -> Sing @Symbol (Show_tuple t_aqvI t_aqvJ)
In the body of lambda with binder t_aqvI_a29K :: [Symbol ~> Symbol]
In the body of lambda with binder t_aqvJ_a29L :: Symbol
In the body of lambda with binder ds_X1 :: Sing
@[Symbol ~> Symbol] t_aqvI_a29K
In the body of lambda with binder ds_X2 :: Sing @Symbol t_aqvJ_a29L
In the body of letrec with binders x_s2zK :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "(" t)
In the RHS of x_s2zL :: Sing
@(Symbol ~> Symbol)
((.@#@$$$)
@Symbol
@Symbol
@Symbol
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
(ShowCharSym1 ")"))
In the RHS of x_s2zI :: Sing
@(TyFun Symbol Symbol -> *)
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
In the RHS of x_s2zH :: forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> Sing
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
(Apply
@Symbol
@(TyFun
(Symbol ~> Symbol)
(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
-> *)
(Apply
@[Symbol ~> Symbol]
@(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol) ~> (Symbol ~> Symbol)))
-> *)
(Lambda_6989586621679111672Sym0
@{TyFun
[Symbol ~> Symbol]
(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol)
~> (Symbol ~> Symbol)))
-> *)})
t_aqvI_a29K)
t_aqvJ_a29L)
t)
t)
In the body of lambda with binder t_X3 :: Symbol ~> Symbol
In the body of lambda with binder x_X4 :: Sing
@(Symbol ~> Symbol) t_X3
In the body of lambda with binder t_X5 :: Symbol ~> Symbol
In the body of letrec with binders $dKnownSymbol_s2zD :: [Char]
In the body of letrec with binders $dSingI_s2zE :: SSymbol ","
In the body of lambda with binder sR_aMu :: Sing
@(Symbol ~> Symbol) t_X5
In the RHS of x_s2zG :: Sing
@(Symbol ~> Symbol)
((.@#@$$$) @Symbol @Symbol @Symbol (ShowCharSym1 ",") t_X5)
In the body of letrec with binders x_s2zF :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)
In the type of a binder: x_s2zF
In the type ‘forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)’
Substitution: [TCvSubst
In scope: InScope {t_X3 t_X5 t_X6 t_aqvI_a29K t_aqvJ_a29L}
Type env: [X5 :-> t_X6]
Co env: []]
Bug.hs:174:34: warning:
Kind application error in type ‘(<>) @Symbol "," t_X5’
Function kind = forall a. a -> a -> a
Arg kinds = [(Symbol, *), (",", Symbol), (t_X5, Symbol ~> Symbol)]
Fun: Symbol
(t_X5, Symbol ~> Symbol)
In the RHS of sShow_tuple :: forall (t_aqvI :: [Symbol ~> Symbol])
(t_aqvJ :: Symbol).
Sing @[Symbol ~> Symbol] t_aqvI
-> Sing @Symbol t_aqvJ -> Sing @Symbol (Show_tuple t_aqvI t_aqvJ)
In the body of lambda with binder t_aqvI_a29K :: [Symbol ~> Symbol]
In the body of lambda with binder t_aqvJ_a29L :: Symbol
In the body of lambda with binder ds_X1 :: Sing
@[Symbol ~> Symbol] t_aqvI_a29K
In the body of lambda with binder ds_X2 :: Sing @Symbol t_aqvJ_a29L
In the body of letrec with binders x_s2zK :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "(" t)
In the RHS of x_s2zL :: Sing
@(Symbol ~> Symbol)
((.@#@$$$)
@Symbol
@Symbol
@Symbol
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
(ShowCharSym1 ")"))
In the RHS of x_s2zI :: Sing
@(TyFun Symbol Symbol -> *)
(Foldr1
@(TyFun Symbol Symbol -> *)
(Lambda_6989586621679111672Sym2
@{[Symbol ~> Symbol]}
@{Symbol}
@{TyFun
(Symbol ~> Symbol)
((Symbol ~> Symbol) ~> (Symbol ~> Symbol))}
t_aqvI_a29K
t_aqvJ_a29L)
t_aqvI_a29K)
In the RHS of x_s2zH :: forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> forall {t :: Symbol ~> Symbol}.
Sing @(Symbol ~> Symbol) t
-> Sing
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(Symbol ~> Symbol)
(Apply
@(Symbol ~> Symbol)
@(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
(Apply
@Symbol
@(TyFun
(Symbol ~> Symbol)
(TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> *)
-> *)
(Apply
@[Symbol ~> Symbol]
@(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol) ~> (Symbol ~> Symbol)))
-> *)
(Lambda_6989586621679111672Sym0
@{TyFun
[Symbol ~> Symbol]
(TyFun
Symbol
((Symbol ~> Symbol)
~> ((Symbol ~> Symbol)
~> (Symbol ~> Symbol)))
-> *)})
t_aqvI_a29K)
t_aqvJ_a29L)
t)
t)
In the body of lambda with binder t_X3 :: Symbol ~> Symbol
In the body of lambda with binder x_X4 :: Sing
@(Symbol ~> Symbol) t_X3
In the body of lambda with binder t_X5 :: Symbol ~> Symbol
In the body of letrec with binders $dKnownSymbol_s2zD :: [Char]
In the body of letrec with binders $dSingI_s2zE :: SSymbol ","
In the body of lambda with binder sR_aMu :: Sing
@(Symbol ~> Symbol) t_X5
In the RHS of x_s2zG :: Sing
@(Symbol ~> Symbol)
((.@#@$$$) @Symbol @Symbol @Symbol (ShowCharSym1 ",") t_X5)
In the body of letrec with binders x_s2zF :: forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)
In the type of a binder: x_s2zF
In the type ‘forall {t :: Symbol}.
Sing @Symbol t -> Sing @Symbol ((<>) @Symbol "," t)’
Substitution: [TCvSubst
In scope: InScope {t_X3 t_X5 t_X6 t_aqvI_a29K t_aqvJ_a29L}
Type env: [X5 :-> t_X6]
Co env: []]
*** Offending Program ***
<elided>
(The full Core Lint error has been elided due to its sheer length.)
One interesting observation about this program is that the Core Lint error only occurs if SingFunction2
and SingFunction3
are defined like so:
type SingFunction2 f = forall t1. Sing t1 -> forall t2. Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction3 f = forall t1. Sing t1 -> forall t2. Sing t2 -> forall t3. Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
If they are instead defined without nested forall
s, like so:
type SingFunction2 f = forall t1 t2. Sing t1 -> Sing t2 -> Sing (f `Apply` t1 `Apply` t2)
type SingFunction3 f = forall t1 t2 t3. Sing t1 -> Sing t2 -> Sing t3 -> Sing (f `Apply` t1 `Apply` t2 `Apply` t3)
Then the Core Lint error does not occur.