Core Lint error (Data alternative when scrutinee is not a tycon application) on GHC 8.10.4+
The following program will produce a Core Lint error when compiled with GHC 8.10.4 or later:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug (decCongS) where
import Data.Kind
import Data.Type.Equality
import Data.Void
decCongS :: forall n j (d :: PDecision (n :~: j)). Sing n -> SDecision d -> Decision (S n :~: S j)
decCongS sn sDNJ = case sDNJ of
SPProved SRefl -> Proved Refl
SPDisproved no -> Disproved $ \r -> case sInjective @n @j sn r of
Refl -> case no @@ SRefl of {}
-----
type Sing :: k -> Type
type family Sing
type SVoid :: Void -> Type
data SVoid z
type instance Sing @Void = SVoid
type Nat :: Type
data Nat = Z | S Nat
type SNat :: Nat -> Type
data SNat z where
SZ :: SNat Z
SS :: Sing n -> SNat (S n)
type instance Sing @Nat = SNat
type (:%~:) :: a :~: b -> Type
data (:%~:) z where
SRefl :: (:%~:) Refl
type instance Sing @(a :~: b) = (:%~:)
type TyFun :: Type -> Type -> Type
data TyFun a b
type (~>) :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type Apply :: (a ~> b) -> a -> b
type family Apply f x
type (@@) :: (a ~> b) -> a -> b
type f @@ x = Apply f x
type SLambda :: (k1 ~> k2) -> Type
newtype SLambda (f :: k1 ~> k2) =
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
type instance Sing = SLambda
(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
(@@) f = applySing f
type Decision :: Type -> Type
data Decision a
= Proved a
| Disproved (a -> Void)
type PDecision :: Type -> Type
data PDecision a
= PProved a
| PDisproved (a ~> Void)
type SDecision :: PDecision a -> Type
data SDecision d where
SPProved :: forall a (x :: a). Sing x -> SDecision (PProved x)
SPDisproved :: forall a (r :: a ~> Void). Sing r -> SDecision (PDisproved r)
type instance Sing @(PDecision a) = SDecision
type ElimNat :: forall (p :: Nat ~> Type) (n :: Nat)
-> p @@ Z
-> (forall (m :: Nat) -> p @@ m ~> p @@ (S m))
-> p @@ n
type family ElimNat p n pZ pS where
forall (p :: Nat ~> Type)
(pZ :: p @@ Z)
(pS :: forall (m :: Nat) -> p @@ m ~> p @@ (S m)).
ElimNat p Z pZ pS = pZ
forall (p :: Nat ~> Type)
(pZ :: p @@ Z)
(pS :: forall (m :: Nat) -> p @@ m ~> p @@ (S m))
(m :: Nat).
ElimNat p (S m) pZ pS = pS m @@ ElimNat p m pZ pS
type Const :: a -> b -> a
type family Const x y where
Const x _ = x
type ConstSym1 :: a -> b ~> a
data ConstSym1 x f
type instance Apply (ConstSym1 x) y = Const x y
type EqSameNat :: Nat -> forall (m :: Nat) -> Const Type m -> Const Type (S m)
type EqSameNat n m r = n :~: m
data EqSameNatSym2 (n :: Nat) (m :: Nat) :: Const Type m ~> Const Type (S m)
type instance Apply (EqSameNatSym2 n m) r = EqSameNat n m r
type NatEqConsequencesBase :: Nat -> Type
type family NatEqConsequencesBase m where
NatEqConsequencesBase Z = ()
NatEqConsequencesBase (S _) = Void
type NatEqConsequencesBaseSym0 :: Nat ~> Type
data NatEqConsequencesBaseSym0 f
type instance Apply NatEqConsequencesBaseSym0 m = NatEqConsequencesBase m
type NatEqConsequencesStep :: forall (m :: Nat) -> Const (Nat ~> Type) m
-> Nat -> Const Type (S m)
type NatEqConsequencesStep m r n = ElimNat (ConstSym1 Type) n Void (EqSameNatSym2 m)
data NatEqConsequencesStepSym1 (m :: Nat) :: Const (Nat ~> Type) m ~> Nat ~> Const Type (S m)
type instance Apply (NatEqConsequencesStepSym1 m) r = NatEqConsequencesStepSym2 m r
data NatEqConsequencesStepSym2 (m :: Nat) (r :: Const (Nat ~> Type) m) :: Nat ~> Const Type (S m)
type instance Apply (NatEqConsequencesStepSym2 m r) n = NatEqConsequencesStep m r n
type NatEqConsequences :: Nat -> Nat -> Type
type NatEqConsequences n m =
ElimNat (ConstSym1 (Nat ~> Type)) n
NatEqConsequencesBaseSym0
NatEqConsequencesStepSym1 @@ m
useNatEq :: forall n j. Sing n -> n :~: j -> NatEqConsequences n j
useNatEq sn Refl = case sn of
SZ -> ()
SS{} -> Refl
sInjective :: forall n j. Sing n -> S n :~: S j -> n :~: j
sInjective sn = useNatEq @(S n) @(S j) (SS sn)$ /opt/ghc/9.0.1/bin/ghc Bug.hs -dcore-lint -ddump-simpl -dno-typeable-binds -dsuppress-coercions
[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
*** Core Lint errors : in result of Simplifier ***
Bug.hs:22:34: warning:
Data alternative when scrutinee is not a tycon application
Scrutinee type: (EqSameNat
n_aWm
j_aWn
(ElimNat
(ConstSym1 (*))
j_aWn
(Void |> Sym (D:R:ApplybaConstSym1y[0]
<*>_N <Nat>_N <*>_N <'Z>_N ; D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<'Z>_N))
(EqSameNatSym2 n_aWm |> forall (m :: <Nat>_N).
(TyFun
(D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<m>_N ; Sym (D:R:ApplybaConstSym1y[0]
<*>_N
<Nat>_N
<*>_N
<m>_N ; D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<m>_N))
(D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<'S m>_N ; Sym (D:R:ApplybaConstSym1y[0]
<*>_N
<Nat>_N
<*>_N
<'S
m>_N ; D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<'S
m>_N)))_N
%<'Many>_N ->_N <*>_N) |> (D:R:ApplybaConstSym1y[0]
<*>_N
<Nat>_N
<*>_N
<j_aWn>_N ; D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<j_aWn>_N) ; Sym (D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<j_aWn>_N)) |> D:R:Const[0]
<*>_N
<Nat>_N
<*>_N
<'S
j_aWn>_N)
Alternative: Refl co_aWO ->
case ((no_aAp `cast` <Co:90>)
@'Refl (($WSRefl @Nat @n_aWm) `cast` <Co:9>))
`cast` <Co:66>
of nt_s10P {
}
In the RHS of decCongS :: forall (n :: Nat) (j :: Nat)
(d :: PDecision (n :~: j)).
Sing n -> SDecision d -> Decision ('S n :~: 'S j)
In the body of lambda with binder n_aWm :: Nat
In the body of lambda with binder j_aWn :: Nat
In the body of lambda with binder d_aWo :: PDecision
(n_aWm :~: j_aWn)
In the body of lambda with binder sn_aAn :: Sing n_aWm
In the body of lambda with binder sDNJ_aAo :: SDecision d_aWo
In a case alternative: (SPDisproved r_aWG :: (n_aWm :~: j_aWn)
~> Void,
co_aWH :: d_aWo ~# 'PDisproved r_aWG,
no_aAp :: Sing r_aWG)
In the body of lambda with binder r_aAq :: 'S n_aWm :~: 'S j_aWn
In a case alternative: (Refl co_aVG :: 'S j_aWn ~# 'S n_aWm)
Substitution: [TCvSubst
In scope: InScope {co_aVG n_aWm j_aWn d_aWo r_aWG co_aWH}
Type env: [aWm :-> n_aWm, aWn :-> j_aWn, aWo :-> d_aWo,
aWG :-> r_aWG]
Co env: [aVG :-> co_aVG, aWH :-> co_aWH]]
*** Offending Program ***
applySing
:: forall k1 k2 (f :: k1 ~> k2).
SLambda f -> forall (t :: k1). Sing t -> Sing (f @@ t)
[LclIdX[[RecSel]],
Arity=1,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}]
applySing
= \ (@k1_aDS)
(@k2_aDT)
(@(f_aDU :: k1_aDS ~> k2_aDT))
(ds_d10J :: SLambda f_aDU)
(@(t_aDV :: k1_aDS)) ->
(ds_d10J `cast` <Co:4>) @t_aDV
decCongS
:: forall (n :: Nat) (j :: Nat) (d :: PDecision (n :~: j)).
Sing n -> SDecision d -> Decision ('S n :~: 'S j)
[LclIdX,
Arity=2,
Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True, Guidance=IF_ARGS [0 50] 140 10}]
decCongS
= \ (@(n_aWm :: Nat))
(@(j_aWn :: Nat))
(@(d_aWo :: PDecision (n_aWm :~: j_aWn)))
(sn_aAn :: Sing n_aWm)
(sDNJ_aAo :: SDecision d_aWo) ->
case sDNJ_aAo of {
SPProved @x_aWq co_aWr ds_d10F ->
case ds_d10F `cast` <Co:6> of { SRefl co_aWx co_aWy ->
(Proved @('S n_aWm :~: 'S n_aWm) ($WRefl @Nat @('S n_aWm)))
`cast` <Co:8>
};
SPDisproved @r_aWG co_aWH no_aAp ->
$ @'LiftedRep
@(('S n_aWm :~: 'S j_aWn) -> Void)
@(Decision ('S n_aWm :~: 'S j_aWn))
(\ (ds_d105 :: ('S n_aWm :~: 'S j_aWn) -> Void) ->
Disproved @('S n_aWm :~: 'S j_aWn) ds_d105)
(\ (r_aAq :: 'S n_aWm :~: 'S j_aWn) ->
case r_aAq of { Refl co_aVG ->
case (Refl @Nat @n_aWm @n_aWm @~<Co:1>) `cast` <Co:3597> of
{ Refl co_aWO ->
case ((no_aAp `cast` <Co:90>)
@'Refl (($WSRefl @Nat @n_aWm) `cast` <Co:9>))
`cast` <Co:66>
of nt_s10P {
}
}
})
}
*** End of Offense ***