ghc-exactprint-0.5.7.0: tests/examples/ghc86/determ004.hs
{-# LANGUAGE TypeOperators
, DataKinds
, PolyKinds
, TypeFamilies
, GADTs
, UndecidableInstances
, RankNTypes
, ScopedTypeVariables
#-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Werror #-}
{-# OPTIONS_GHC -O1 -fspec-constr #-}
{-
With reversed order of allocated uniques the type variables would be in
wrong order:
*** Core Lint errors : in result of SpecConstr ***
determ004.hs:88:12: warning:
[in body of lambda with binder m_azbFg :: a_afdP_azbON]
@ (a_afdP_azbON :: BOX) is out of scope
*** Offending Program ***
...
Rec {
$s$wsFoldr1_szbtK
:: forall (m_azbFg :: a_afdP_azbON)
(x_azbOM :: TyFun
a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> Type)
-> Type)
(a_afdP_azbON :: BOX)
(ipv_szbwN :: a_afdP_azbON)
(ipv_szbwO :: [a_afdP_azbON]).
R:Sing[]z (ipv_szbwN : ipv_szbwO)
~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO)
-> Sing ipv_szbwO
-> Sing ipv_szbwN
-> (forall (t_azbNM :: a_afdP_azbON).
Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM))
-> Sing
(Apply
(Apply Foldr1Sym0 x_azbOM)
(Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
[LclId,
Arity=4,
Str=DmdType <L,U><L,U><L,U><C(S(C(S))),C(U(1*C1(U)))>]
$s$wsFoldr1_szbtK =
\ (@ (m_azbFg :: a_afdP_azbON))
(@ (x_azbOM :: TyFun
a_afdP_azbON (TyFun a_afdP_azbON a_afdP_azbON -> Type)
-> Type))
(@ (a_afdP_azbON :: BOX))
(@ (ipv_szbwN :: a_afdP_azbON))
(@ (ipv_szbwO :: [a_afdP_azbON]))
(sg_szbtL
:: R:Sing[]z (ipv_szbwN : ipv_szbwO)
~R# Sing (Apply (Apply (:$) ipv_szbwN) ipv_szbwO))
(sc_szbtM :: Sing ipv_szbwO)
(sc_szbtN :: Sing ipv_szbwN)
(sc_szbtP
:: forall (t_azbNM :: a_afdP_azbON).
Sing t_azbNM -> Sing (Apply x_azbOM t_azbNM)) ->
case (SCons
@ a_afdP_azbON
@ (ipv_szbwN : ipv_szbwO)
@ ipv_szbwO
@ ipv_szbwN
@~ (<ipv_szbwN : ipv_szbwO>_N
:: (ipv_szbwN : ipv_szbwO) ~# (ipv_szbwN : ipv_szbwO))
sc_szbtN
sc_szbtM)
`cast` (sg_szbtL
; TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <Let1627448493XsSym4
x_azbOM m_azbFg ipv_szbwN ipv_szbwO>_N
:: R:Sing[]z (ipv_szbwN : ipv_szbwO)
~R# R:Sing[]z
(Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO))
of wild_XD {
SNil dt_dzbxX ->
(lvl_szbwi @ a_afdP_azbON)
`cast` ((Sing
(Sym (TFCo:R:Foldr1[2] <a_afdP_azbON>_N <x_azbOM>_N)
; Sym
(TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
<a_afdP_azbON>_N <'[]>_N <x_azbOM>_N)
; (Apply
(Sym
(TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
(Sym dt_dzbxX))_N))_R
:: Sing (Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list")
~R# Sing
(Apply
(Apply Foldr1Sym0 x_azbOM)
(Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
SCons @ n_azbFh @ m_XzbGe dt_dzbxK _sX_azbOH
ds_dzbyu [Dmd=<S,1*U>] ->
case ds_dzbyu
`cast` (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N <n_azbFh>_N
:: Sing n_azbFh ~R# R:Sing[]z n_azbFh)
of wild_Xo {
SNil dt_dzbxk ->
(lvl_szbw1 @ a_afdP_azbON @ m_XzbGe)
`cast` ((Sing
(Sym (TFCo:R:Foldr1[0] <a_afdP_azbON>_N <m_XzbGe>_N <x_azbOM>_N)
; Sym
(TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
<a_afdP_azbON>_N <'[m_XzbGe]>_N <x_azbOM>_N)
; (Apply
(Sym
(TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
((<m_XzbGe>_N ': Sym dt_dzbxk)_N ; Sym dt_dzbxK))_N))_R
:: Sing m_XzbGe
~R# Sing
(Apply
(Apply Foldr1Sym0 x_azbOM)
(Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)));
SCons @ ipv_XzbxR @ ipv_XzbyV ipv_szbwM ipv_szbwL ipv_szbwK ->
case (sc_szbtP @ m_XzbGe _sX_azbOH)
`cast` (TFCo:R:Sing(->)f[0]
<a_afdP_azbON>_N <a_afdP_azbON>_N <Apply x_azbOM m_XzbGe>_N
:: Sing (Apply x_azbOM m_XzbGe)
~R# R:Sing(->)f (Apply x_azbOM m_XzbGe))
of wild_X3X { SLambda ds_XzbBr [Dmd=<C(S),1*C1(U)>] ->
(ds_XzbBr
@ (Foldr1 x_azbOM (ipv_XzbyV : ipv_XzbxR))
(($wsFoldr1_szbuc
@ a_afdP_azbON
@ x_azbOM
@ (Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR)
sc_szbtP
((SCons
@ a_afdP_azbON
@ (ipv_XzbyV : ipv_XzbxR)
@ ipv_XzbxR
@ ipv_XzbyV
@~ (<ipv_XzbyV : ipv_XzbxR>_N
:: (ipv_XzbyV : ipv_XzbxR) ~# (ipv_XzbyV : ipv_XzbxR))
ipv_szbwL
ipv_szbwK)
`cast` (Sym (TFCo:R:Sing[]z[0] <a_afdP_azbON>_N) (Sym
(TFCo:R:Apply[][]:$$i[0]
<a_afdP_azbON>_N
<ipv_XzbxR>_N
<ipv_XzbyV>_N)
; (Apply
(Sym
(TFCo:R:Applyk(->):$l[0]
<a_afdP_azbON>_N
<ipv_XzbyV>_N))
<ipv_XzbxR>_N)_N)
:: R:Sing[]z (ipv_XzbyV : ipv_XzbxR)
~R# Sing (Apply (Apply (:$) ipv_XzbyV) ipv_XzbxR))))
`cast` ((Sing
((Apply
(TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N)
<Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR>_N)_N
; TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
<a_afdP_azbON>_N
((Apply
(TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N)
<ipv_XzbxR>_N)_N
; TFCo:R:Apply[][]:$$i[0]
<a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
<x_azbOM>_N))_R
:: Sing
(Apply
(Apply Foldr1Sym0 x_azbOM)
(Let1627448493XsSym4 x_azbOM m_XzbGe ipv_XzbyV ipv_XzbxR))
~R# Sing (Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))))
`cast` ((Sing
((Apply
<Apply x_azbOM m_XzbGe>_N
(Sym
(TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
<a_afdP_azbON>_N <ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
; (Apply
(Sym
(TFCo:R:Apply(->)(->)Foldr1Sym0l[0]
<a_afdP_azbON>_N <x_azbOM>_N))
(Sym
(TFCo:R:Apply[][]:$$i[0]
<a_afdP_azbON>_N <ipv_XzbxR>_N <ipv_XzbyV>_N)
; (Apply
(Sym
(TFCo:R:Applyk(->):$l[0] <a_afdP_azbON>_N <ipv_XzbyV>_N))
<ipv_XzbxR>_N)_N))_N))_N
; Sym
(TFCo:R:Foldr1[1]
<a_afdP_azbON>_N
<ipv_XzbxR>_N
<ipv_XzbyV>_N
<m_XzbGe>_N
<x_azbOM>_N)
; Sym
(TFCo:R:Apply[]kFoldr1Sym1l_afe2[0]
<a_afdP_azbON>_N <m_XzbGe : ipv_XzbyV : ipv_XzbxR>_N <x_azbOM>_N)
; (Apply
(Sym
(TFCo:R:Apply(->)(->)Foldr1Sym0l[0] <a_afdP_azbON>_N <x_azbOM>_N))
((<m_XzbGe>_N ': Sym ipv_szbwM)_N ; Sym dt_dzbxK))_N))_R
:: Sing
(Apply
(Apply x_azbOM m_XzbGe)
(Foldr1Sym2 x_azbOM (ipv_XzbyV : ipv_XzbxR)))
~R# Sing
(Apply
(Apply Foldr1Sym0 x_azbOM)
(Let1627448493XsSym4 x_azbOM m_azbFg ipv_szbwN ipv_szbwO)))
}
}
}
...
-}
module List (sFoldr1) where
data Proxy t
data family Sing (a :: k)
data TyFun (a :: Type) (b :: Type)
type family Apply (f :: TyFun k1 k2 -> Type) (x :: k1) :: k2
data instance Sing (f :: TyFun k1 k2 -> Type) =
SLambda { applySing :: forall t. Sing t -> Sing (Apply f t) }
type SingFunction1 f = forall t. Sing t -> Sing (Apply f t)
type SingFunction2 f = forall t. Sing t -> SingFunction1 (Apply f t)
singFun2 :: Proxy f -> SingFunction2 f -> Sing f
singFun2 _ f = SLambda (\x -> SLambda (f x))
data (:$$) (j :: a) (i :: TyFun [a] [a])
type instance Apply ((:$$) j) i = (:) j i
data (:$) (l :: TyFun a (TyFun [a] [a] -> Type))
type instance Apply (:$) l = (:$$) l
data instance Sing (z :: [a])
= z ~ '[] =>
SNil
| forall (m :: a)
(n :: [a]). z ~ (:) m n =>
SCons (Sing m) (Sing n)
data ErrorSym0 (t1 :: TyFun k1 k2)
type Let1627448493XsSym4 t_afee t_afef t_afeg t_afeh = Let1627448493Xs t_afee t_afef t_afeg t_afeh
type Let1627448493Xs f_afe9
x_afea
wild_1627448474_afeb
wild_1627448476_afec =
Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec
type Foldr1Sym2 (t_afdY :: TyFun a_afdP (TyFun a_afdP a_afdP -> Type)
-> Type)
(t_afdZ :: [a_afdP]) =
Foldr1 t_afdY t_afdZ
data Foldr1Sym1 (l_afe3 :: TyFun a_afdP (TyFun a_afdP a_afdP -> Type)
-> Type)
(l_afe2 :: TyFun [a_afdP] a_afdP)
type instance Apply (Foldr1Sym1 l_afe3) l_afe2 = Foldr1Sym2 l_afe3 l_afe2
data Foldr1Sym0 (l_afe0 :: TyFun (TyFun a_afdP (TyFun a_afdP a_afdP
-> Type)
-> Type) (TyFun [a_afdP] a_afdP -> Type))
type instance Apply Foldr1Sym0 l = Foldr1Sym1 l
type family Foldr1 (a_afe5 :: TyFun a_afdP (TyFun a_afdP a_afdP
-> Type)
-> Type)
(a_afe6 :: [a_afdP]) :: a_afdP where
Foldr1 z_afe7 '[x_afe8] = x_afe8
Foldr1 f_afe9 ((:) x_afea ((:) wild_1627448474_afeb wild_1627448476_afec)) = Apply (Apply f_afe9 x_afea) (Apply (Apply Foldr1Sym0 f_afe9) (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec))
Foldr1 z_afew '[] = Apply ErrorSym0 "Data.Singletons.List.foldr1: empty list"
sFoldr1 ::
forall (x :: TyFun a_afdP (TyFun a_afdP a_afdP -> Type) -> Type)
(y :: [a_afdP]).
Sing x
-> Sing y -> Sing (Apply (Apply Foldr1Sym0 x) y)
sFoldr1 _ (SCons _sX SNil) = undefined
sFoldr1 sF (SCons sX (SCons sWild_1627448474 sWild_1627448476))
= let
lambda_afeC ::
forall f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec.
Sing f_afe9
-> Sing x_afea
-> Sing wild_1627448474_afeb
-> Sing wild_1627448476_afec
-> Sing (Apply (Apply Foldr1Sym0 f_afe9) (Apply (Apply (:$) x_afea) (Apply (Apply (:$) wild_1627448474_afeb) wild_1627448476_afec)))
lambda_afeC f_afeD x_afeE wild_1627448474_afeF wild_1627448476_afeG
= let
sXs ::
Sing (Let1627448493XsSym4 f_afe9 x_afea wild_1627448474_afeb wild_1627448476_afec)
sXs
= applySing
(applySing
(singFun2 (undefined :: Proxy (:$)) SCons) wild_1627448474_afeF)
wild_1627448476_afeG
in
applySing
(applySing f_afeD x_afeE)
(applySing
(applySing (singFun2 (undefined :: Proxy Foldr1Sym0) sFoldr1) f_afeD)
sXs)
in lambda_afeC sF sX sWild_1627448474 sWild_1627448476
sFoldr1 _ SNil = undefined