"rules/prof.mk" did not exist on "master"
GHC panic (Prelude.!!: index too large) and Core Lint error (Trans coercion mis-match)
GHC 9.0 and HEAD are very unhappy with this program:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Bug where
import Data.Kind
import Data.Type.Equality
type family Sing :: k -> Type
data SomeSing :: Type -> Type where
SomeSing :: Sing (a :: k) -> SomeSing k
data SList :: forall a. [a] -> Type where
SNil :: SList '[]
SCons :: Sing x -> Sing xs -> SList (x:xs)
type instance Sing = SList
data Univ = U1 | K1 Type | Sum Univ Univ | Product Univ Univ
data SUniv :: Univ -> Type where
SU1 :: SUniv U1
SK1 :: Sing c -> SUniv (K1 c)
SSum :: Sing a -> Sing b -> SUniv (Sum a b)
SProduct :: Sing a -> Sing b -> SUniv (Product a b)
type instance Sing = SUniv
data In :: Univ -> Type where
MkU1 :: In U1
MkK1 :: c -> In (K1 c)
L1 :: In a -> In (Sum a b)
R1 :: In b -> In (Sum a b)
MkProduct :: In a -> In b -> In (Product a b)
data SIn :: forall u. In u -> Type where
SMkU1 :: SIn MkU1
SMkK1 :: Sing c -> SIn (MkK1 c)
SL1 :: Sing a -> SIn (L1 a)
SR1 :: Sing b -> SIn (R1 b)
SMkProduct :: Sing a -> Sing b -> SIn (MkProduct a b)
type instance Sing = SIn
class Generic (a :: Type) where
type Rep a :: Univ
from :: a -> In (Rep a)
to :: In (Rep a) -> a
class PGeneric (a :: Type) where
type PFrom (x :: a) :: In (Rep a)
type PTo (x :: In (Rep a)) :: a
class SGeneric k where
sFrom :: forall (a :: k). Sing a -> Sing (PFrom a)
sTo :: forall (a :: In (Rep k)). Sing a -> Sing (PTo a :: k)
sTof :: forall (a :: k). Sing a -> PTo (PFrom a) :~: a
sFot :: forall (a :: In (Rep k)). Sing a -> PFrom (PTo a :: k) :~: a
instance Generic [a] where
type Rep [a] = Sum U1 (Product (K1 a) (K1 [a]))
from [] = L1 MkU1
from (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
to (L1 MkU1) = []
to (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
instance PGeneric [a] where
type PFrom '[] = L1 MkU1
type PFrom (x:xs) = R1 (MkProduct (MkK1 x) (MkK1 xs))
type PTo (L1 MkU1) = '[]
type PTo (R1 (MkProduct (MkK1 x) (MkK1 xs))) = x:xs
instance SGeneric [a] where
sFrom SNil = SL1 SMkU1
sFrom (SCons x xs) = SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))
sTo (SL1 SMkU1) = SNil
sTo (SR1 (SMkProduct (SMkK1 x) (SMkK1 xs))) = SCons x xs
sTof SNil = Refl
sTof SCons{} = Refl
sFot (SL1 SMkU1) = Refl
sFot (SR1 (SMkProduct SMkK1{} SMkK1{})) = ReflCompiling it without -dcore-lint will cause a panic:
$ ~/Software/ghc-9.0/bin/ghc -fforce-recomp Bug.hs
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20200920:
Prelude.!!: index too largeCompiling it with -dcore-lint will result in a Core Lint error that prematurely ends in a panic:
$ ~/Software/ghc-9.0/bin/ghc -fforce-recomp Bug.hs -dcore-lint
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Desugar (after optimization) ***
Bug.hs:81:3: warning:
Trans coercion mis-match: Nth:0
(Nth:3
(Inst (Inst <forall (a :: Univ) (b :: Univ).
In a -> In ('Sum a b)>_N (Nth:0 co_aRl)) (Nth:1
co_aRl))) ; (Nth:0
(Sym (Kind
co_aRm)) ; Sym (D:R:Rep[][0]
<a_aOX>_N))
'U1 ~ a_aRi
'Sum a_aRi b_aRj ~ Rep [a_aOX]
In the RHS of $csFot_aRb :: forall a (a :: In (Rep [a])).
Sing a -> PFrom (PTo a) :~: a
In the body of lambda with binder a_aOX :: *
In the body of lambda with binder a_aRe :: In (Rep [a_aOX])
In the body of lambda with binder ds_d1rk :: Sing a_aRe
In the body of letrec with binders fail_d1RM :: Void#
-> PFrom (PTo a_aRe) :~: a_aRe
In a case alternative: (SL1 a_aRi :: Univ,
b_aRj :: Univ,
a_aRk :: In a_aRi,
co_aRl :: 'Sum 'U1 ('Product ('K1 a_aOX) ('K1 [a_aOX]))
~# 'Sum a_aRi b_aRj,
co_aRm :: (a_aRe |> Sym (In (Sym (D:R:Rep[][0] <a_aOX>_N)))_N)
~# 'L1 a_aRk,
ds_d1RC :: Sing a_aRk)
In a case alternative: (SMkU1 co_aRq :: 'U1 ~# 'U1,
co_aRr :: (a_aRk |> Sym (In (Sym (Nth:0 (Sym co_aRl))))_N)
~# 'MkU1)
Substitution: [TCvSubst
In scope: InScope {a_aOX a_aRe a_aRi b_aRj a_aRk co_aRl co_aRm
co_aRq co_aRr}
Type env: [aOX :-> a_aOX, aRe :-> a_aRe, aRi :-> a_aRi,
aRj :-> b_aRj, aRk :-> a_aRk]
Co env: [aRl :-> co_aRl, aRm :-> co_aRm, aRq :-> co_aRq,
aRr :-> co_aRr]]
*** Offending Program ***
$cto_aSH :: forall a. In (Rep [a]) -> [a]
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [68] 260 20}]
$cto_aSH
= \ (@a_aSl) (ds_d1RZ :: In (Rep [a_aSl])) ->
join {
fail_d217 :: Void# -> [a_aSl]
[LclId[JoinId(1)],
Str=<L,U>,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [0] 120 0}]
fail_d217 _ [Occ=Dead, OS=OneShot]
= patError
@'LiftedRep @[a_aSl] "Bug.hs:(65,3)-(66,47)|function to"# } in
case ds_d1RZ of {
__DEFAULT -> jump fail_d217 void#;
L1 @a_aSK @b_aSL co_aSM ds_d213 ->
case ds_d213 of {
__DEFAULT -> jump fail_d217 void#;
MkU1 co_aSN -> [] @a_aSl
};
R1 @b_aSR @a_aSS co_aST ds_d214 ->
case ds_d214 of {
__DEFAULT -> jump fail_d217 void#;
MkProduct @a_aSU @b_aSV co_aSW ds_d215 ds_d216 ->
case ds_d215 of {
__DEFAULT -> jump fail_d217 void#;
MkK1 @c_aSX co_aSY x_axD ->
case ds_d216 of {
__DEFAULT -> jump fail_d217 void#;
MkK1 @c_aSZ co_aT0 xs_axE ->
(: @c_aSX
x_axD
(xs_axE
`cast` (Sub (Nth:0
(Sym co_aT0 ; Nth:1
(Sym co_aSW ; Nth:1
(Sym co_aST ; D:R:Rep[][0]
<a_aSl>_N)))) ; ([Sub (Nth:0
(Nth:0
(Nth:1
(Sym (D:R:Rep[][0]
<a_aSl>_N) ; co_aST) ; co_aSW) ; co_aSY))])_R
:: c_aSZ ~R# [c_aSX])))
`cast` (([Sub (Nth:0
(Sym co_aSY ; Nth:0
(Sym co_aSW ; Nth:1
(Sym co_aST ; D:R:Rep[][0]
<a_aSl>_N))))])_R
:: [c_aSX] ~R# [a_aSl])
}
}
}
}
$cfrom_aSn :: forall a. [a] -> In (Rep [a])
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [50] 130 0}]
$cfrom_aSn
= \ (@a_aSl) (ds_d1RO :: [a_aSl]) ->
case ds_d1RO of {
[] ->
($WL1 @'U1 @('Product ('K1 a_aSl) ('K1 [a_aSl])) $WMkU1)
`cast` ((In (Sym (D:R:Rep[][0] <a_aSl>_N)))_R
:: In ('Sum 'U1 ('Product ('K1 a_aSl) ('K1 [a_aSl])))
~R# In (Rep [a_aSl]));
: x_axB xs_axC ->
($WR1
@('Product ('K1 a_aSl) ('K1 [a_aSl]))
@'U1
($WMkProduct
@('K1 a_aSl)
@('K1 [a_aSl])
($WMkK1 @a_aSl x_axB)
($WMkK1 @[a_aSl] xs_axC)))
`cast` ((In (Sym (D:R:Rep[][0] <a_aSl>_N)))_R
:: In ('Sum 'U1 ('Product ('K1 a_aSl) ('K1 [a_aSl])))
~R# In (Rep [a_aSl]))
}
$fGeneric[] [InlPrag=NOUSERINLINE CONLIKE] :: forall a. Generic [a]
[LclIdX[DFunId],
Unf=DFun: \ (@a_axA) ->
C:Generic TYPE: [a_axA] $cfrom_aSn @a_axA $cto_aSH @a_axA]
$fGeneric[]
= \ (@a_aSl) ->
C:Generic @[a_aSl] ($cfrom_aSn @a_aSl) ($cto_aSH @a_aSl)
$fPGeneric[] [InlPrag=NOUSERINLINE CONLIKE]
:: forall a. PGeneric [a]
[LclIdX[DFunId], Unf=DFun: \ (@a_axv) -> C:PGeneric TYPE: [a_axv]]
$fPGeneric[] = \ (@a_aSi) -> C:PGeneric @[a_aSi]
$csFot_aRb
:: forall a (a :: In (Rep [a])). Sing a -> PFrom (PTo a) :~: a
[LclId,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [68] 250 0}]
$csFot_aRb
= \ (@a_aOX)
(@(a_aRe :: In (Rep [a_aOX])))
(ds_d1rk :: Sing a_aRe) ->
join {
fail_d1RM :: Void# -> PFrom (PTo a_aRe) :~: a_aRe
[LclId[JoinId(1)],
Str=<L,U>,
Unf=Unf{Src=<vanilla>, TopLvl=False, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [0] 120 0}]
fail_d1RM _ [Occ=Dead, OS=OneShot]
= patError
@'LiftedRep
@(PFrom (PTo a_aRe) :~: a_aRe)
"Bug.hs:(81,3)-(82,48)|function sFot"# } in
case ds_d1rk
`cast` ((Sub (D:R:SingIn[0] <Rep [a_aOX]>_N) ; ((SIn
(D:R:Rep[][0]
<a_aOX>_N))_R ; GRefl representational SIn
((In
(Sym (D:R:Rep[][0]
<a_aOX>_N)))_N
# <'Many>_N ->_N <*>_N))) <a_aRe>_N
:: Sing a_aRe
~R# SIn (a_aRe |> Sym (In (Sym (D:R:Rep[][0] <a_aOX>_N)))_N))
of {
__DEFAULT -> jump fail_d1RM void#;
SL1 @a_aRi @b_aRj @a_aRk co_aRl co_aRm ds_d1RC ->
case ds_d1RC
`cast` ((Sub (D:R:SingIn[0] <a_aRi>_N) ; ((SIn
(Nth:0
(Sym co_aRl)))_R ; GRefl representational SIn
((In
(Nth:0
co_aRl))_N
# <'Many>_N ->_N <*>_N))) <a_aRk>_N
:: Sing a_aRk ~R# SIn (a_aRk |> Sym (In (Nth:0 co_aRl))_N))
of {
__DEFAULT -> jump fail_d1RM void#;
SMkU1 co_aRq co_aRr ->
($WRefl
@(In ('Sum 'U1 ('Product ('K1 a_aOX) ('K1 [a_aOX])))) @('L1 'MkU1))
`cast` (((:~:)
(In (Sym (D:R:Rep[][0] <a_aOX>_N)))_N
(Sym (GRefl nominal ('L1 'MkU1 |> (In
(Sym (D:R:Rep[][0] <a_aOX>_N)))_N)
(In (D:R:Rep[][0] <a_aOX>_N))_N) ; (Sym (D:R:PFrom[][][0]
<a_aOX>_N) ; (PFrom
<[a_aOX]>_N
(Sym (D:R:PTo[]L1[0]
<a_aOX>_N) ; (PTo
<[a_aOX]>_N
(Sym (GRefl nominal ('L1
'MkU1)
(In
(Nth:0
(Nth:3
(Inst (Inst <forall (a :: Univ)
(b :: Univ).
In
a
-> In
('Sum
a
b)>_N (Nth:0
co_aRl)) (Nth:1
co_aRl))) ; (Nth:0
(Sym (Kind
co_aRm)) ; Sym (D:R:Rep[][0]
<a_aOX>_N))))_N) ; (('L1
(Nth:0
co_aRl)
(Nth:1
co_aRl)
(Sym co_aRr ; Sym (GRefl nominal a_aRk
(In
(Nth:0
(Sym co_aRl)))_N)))_N ; (Sym co_aRm ; Sym (GRefl nominal a_aRe
(In
(D:R:Rep[][0]
<a_aOX>_N))_N)))))_N))_N))
(('L1
(Nth:0 co_aRl)
(Nth:1 co_aRl)
(Sym co_aRr ; Sym (GRefl nominal a_aRk
(In
(Nth:0
(Sym co_aRl)))_N)))_N ; (Sym co_aRm ; Sym (GRefl nominal a_aRe
(In
(D:R:Rep[][0]
<a_aOX>_N))_N))))_R
:: ('L1 'MkU1 :~: 'L1 'MkU1) ~R# (PFrom (PTo a_aRe) :~: a_aRe))
};
SR1 @b_aRD @a_aRE @b_aRF co_aRG co_aRH ds_d1RE ->
case ds_d1RE
`cast` ((Sub (D:R:SingIn[0] <b_aRD>_N) ; ((SIn
(Nth:1
(Sym co_aRG)))_R ; GRefl representational SIn
((In
(Nth:1
co_aRG))_N
# <'Many>_N ->_N <*>_N))) <b_aRF>_N
:: Sing b_aRF ~R# SIn (b_aRF |> Sym (In (Nth:1 co_aRG))_N))
of {
__DEFAULT -> jump fail_d1RM void#;
SMkProduct @a_aRL @b_aRM @a_aRN @b_aRO co_aRP co_aRQ ds_d1RG
ds_d1RH ->
case ds_d1RG
`cast` ((Sub (D:R:SingIn[0] <a_aRL>_N) ; ((SIn
(Nth:0
(Sym co_aRP)))_R ; GRefl representational SIn
((In
(Nth:0
co_aRP))_N
# <'Many>_N ->_N <*>_N))) <a_aRN>_N
:: Sing a_aRN ~R# SIn (a_aRN |> Sym (In (Nth:0 co_aRP))_N))
of {
__DEFAULT -> jump fail_d1RM void#;
SMkK1 @k_aRU @c_aRV co_aRW co_aRX _ [Occ=Dead] ->
case ds_d1RH
`cast` ((Sub (D:R:SingIn[0] <b_aRM>_N) ; ((SIn
(Nth:1
(Sym co_aRP)))_R ; GRefl representational SIn
((In
(Nth:1
co_aRP))_N
# <'Many>_N ->_N <*>_N))) <b_aRO>_N
:: Sing b_aRO ~R# SIn (b_aRO |> Sym (In (Nth:1 co_aRP))_N))
of {
__DEFAULT -> jump fail_d1RM void#;
SMkK1 @k_aS1 @c_aS2 co_aS3 co_aS4 _ [Occ=Dead] ->
($WRefl
@(In ('Sum 'U1 ('Product ('K1 a_aOX) ('K1 [a_aOX]))))
@('R1
('MkProduct
('MkK1 (c_aRV |> Nth:0 (Sym co_aRW)))
('MkK1ghc: panic! (the 'impossible' happened)
(GHC version 9.0.0.20200920:
Prelude.!!: index too largeNote that GHC 8.10.2 can compile this program (even with -dcore-lint) without any issues, so this is a regression.