ghc
ghc copied to clipboard
goldfirere
Not in scope while type-checking
{-# LANGUAGE DeriveDataTypeable, TypeFamilies, TemplateHaskell, DataKinds,
PolyKinds, GADTs, RankNTypes, MultiParamTypeClasses,
FlexibleInstances, UndecidableInstances, UnicodeSyntax,
FunctionalDependencies, StandaloneDeriving,
TypeOperators, ScopedTypeVariables, NoMonomorphismRestriction,
MonadComprehensions, DeriveGeneric, FlexibleContexts,
GeneralizedNewtypeDeriving, ConstraintKinds,
LambdaCase, ViewPatterns, -- AllowAmbiguousTypes,
DefaultSignatures, RecursiveDo, -- ImpredicativeTypes,
ImplicitParams, MagicHash, UnboxedTuples, RoleAnnotations,
ExtendedDefaultRules, PatternSynonyms, EmptyCase,
BangPatterns, InstanceSigs, DeriveFunctor, Arrows
, NamedWildCards, PartialTypeSignatures
, TypeInType, TypeApplications, TypeFamilyDependencies
-- , OverloadedLists
#-}
module Scratch where
import Data.Singletons
import Data.Singletons.Prelude.Base
import Data.Singletons.Prelude.Instances
import Data.Singletons.Prelude.Eq
import Data.Proxy
import GHC.Types
type CompareSym2 t_aRSH t_aRSI =
Compare t_aRSH t_aRSI
data CompareSym1 (l_aRSM :: a1627597068)
(l_aRSL :: Data.Singletons.TyFun a1627597068 Ordering)
type instance Data.Singletons.Apply (CompareSym1 l_aRSM) l_aRSL = CompareSym2 l_aRSM l_aRSL
data CompareSym0 (l_aRSJ :: Data.Singletons.TyFun a1627597068 (Data.Singletons.TyFun a1627597068 Ordering
-> GHC.Types.Type))
= forall arg_aRSK. Data.Singletons.KindOf (Data.Singletons.Apply CompareSym0 arg_aRSK) ~ Data.Singletons.KindOf (CompareSym1 arg_aRSK) =>
CompareSym0KindInference
type instance Data.Singletons.Apply CompareSym0 l_aRSJ = CompareSym1 l_aRSJ
type (:<$$$) (t_aRSQ :: a1627597068) (t_aRSR :: a1627597068) =
(:<) t_aRSQ t_aRSR
data (:<$$) (l_aRSV :: a1627597068)
(l_aRSU :: Data.Singletons.TyFun a1627597068 Bool)
= forall arg_aRSW. Data.Singletons.KindOf (Data.Singletons.Apply ((:<$$) l_aRSV) arg_aRSW) ~ Data.Singletons.KindOf ((:<$$$) l_aRSV arg_aRSW) =>
(:<$$###)
type instance Data.Singletons.Apply ((:<$$) l_aRSV) l_aRSU = (:<$$$) l_aRSV l_aRSU
data (:<$) (l_aRSS :: Data.Singletons.TyFun a1627597068 (Data.Singletons.TyFun a1627597068 Bool
-> GHC.Types.Type))
= forall arg_aRST. Data.Singletons.KindOf (Data.Singletons.Apply (:<$) arg_aRST) ~ Data.Singletons.KindOf ((:<$$) arg_aRST) =>
(:<$###)
type instance Data.Singletons.Apply (:<$) l_aRSS = (:<$$) l_aRSS
type (:<=$$$) (t_aRSZ :: a1627597068) (t_aRT0 :: a1627597068) =
(:<=) t_aRSZ t_aRT0
data (:<=$$) (l_aRT4 :: a1627597068)
(l_aRT3 :: Data.Singletons.TyFun a1627597068 Bool)
= forall arg_aRT5. Data.Singletons.KindOf (Data.Singletons.Apply ((:<=$$) l_aRT4) arg_aRT5) ~ Data.Singletons.KindOf ((:<=$$$) l_aRT4 arg_aRT5) =>
(:<=$$###)
type instance Data.Singletons.Apply ((:<=$$) l_aRT4) l_aRT3 = (:<=$$$) l_aRT4 l_aRT3
data (:<=$) (l_aRT1 :: Data.Singletons.TyFun a1627597068 (Data.Singletons.TyFun a1627597068 Bool
-> GHC.Types.Type))
= forall arg_aRT2. Data.Singletons.KindOf (Data.Singletons.Apply (:<=$) arg_aRT2) ~ Data.Singletons.KindOf ((:<=$$) arg_aRT2) =>
(:<=$###)
type instance Data.Singletons.Apply (:<=$) l_aRT1 = (:<=$$) l_aRT1
type (:>$$$) (t_aRT8 :: a1627597068) (t_aRT9 :: a1627597068) =
(:>) t_aRT8 t_aRT9
data (:>$$) (l_aRTd :: a1627597068)
(l_aRTc :: Data.Singletons.TyFun a1627597068 Bool)
= forall arg_aRTe. Data.Singletons.KindOf (Data.Singletons.Apply ((:>$$) l_aRTd) arg_aRTe) ~ Data.Singletons.KindOf ((:>$$$) l_aRTd arg_aRTe) =>
(:>$$###)
type instance Data.Singletons.Apply ((:>$$) l_aRTd) l_aRTc = (:>$$$) l_aRTd l_aRTc
data (:>$) (l_aRTa :: Data.Singletons.TyFun a1627597068 (Data.Singletons.TyFun a1627597068 Bool
-> GHC.Types.Type))
= forall arg_aRTb. Data.Singletons.KindOf (Data.Singletons.Apply (:>$) arg_aRTb) ~ Data.Singletons.KindOf ((:>$$) arg_aRTb) =>
(:>$###)
type instance Data.Singletons.Apply (:>$) l_aRTa = (:>$$) l_aRTa
type (:>=$$$) (t_aRTh :: a1627597068) (t_aRTi :: a1627597068) =
(:>=) t_aRTh t_aRTi
data (:>=$$) (l_aRTm :: a1627597068)
(l_aRTl :: Data.Singletons.TyFun a1627597068 Bool)
= forall arg_aRTn. Data.Singletons.KindOf (Data.Singletons.Apply ((:>=$$) l_aRTm) arg_aRTn) ~ Data.Singletons.KindOf ((:>=$$$) l_aRTm arg_aRTn) =>
(:>=$$###)
type instance Data.Singletons.Apply ((:>=$$) l_aRTm) l_aRTl = (:>=$$$) l_aRTm l_aRTl
data (:>=$) (l_aRTj :: Data.Singletons.TyFun a1627597068 (Data.Singletons.TyFun a1627597068 Bool
-> GHC.Types.Type))
= forall arg_aRTk. Data.Singletons.KindOf (Data.Singletons.Apply (:>=$) arg_aRTk) ~ Data.Singletons.KindOf ((:>=$$) arg_aRTk) =>
(:>=$###)
type instance Data.Singletons.Apply (:>=$) l_aRTj = (:>=$$) l_aRTj
type Let1627597129Scrutinee_1627597071Sym2 t_aRTA t_aRTB =
Let1627597129Scrutinee_1627597071 t_aRTA t_aRTB
data Let1627597129Scrutinee_1627597071Sym1 l_aRTF l_aRTE
= forall arg_aRTG. Data.Singletons.KindOf (Data.Singletons.Apply (Let1627597129Scrutinee_1627597071Sym1 l_aRTF) arg_aRTG) ~ Data.Singletons.KindOf (Let1627597129Scrutinee_1627597071Sym2 l_aRTF arg_aRTG) =>
Let1627597129Scrutinee_1627597071Sym1KindInference
type instance Data.Singletons.Apply (Let1627597129Scrutinee_1627597071Sym1 l_aRTF) l_aRTE = Let1627597129Scrutinee_1627597071Sym2 l_aRTF l_aRTE
data Let1627597129Scrutinee_1627597071Sym0 l_aRTC
= forall arg_aRTD. Data.Singletons.KindOf (Data.Singletons.Apply Let1627597129Scrutinee_1627597071Sym0 arg_aRTD) ~ Data.Singletons.KindOf (Let1627597129Scrutinee_1627597071Sym1 arg_aRTD) =>
Let1627597129Scrutinee_1627597071Sym0KindInference
type instance Data.Singletons.Apply Let1627597129Scrutinee_1627597071Sym0 l_aRTC = Let1627597129Scrutinee_1627597071Sym1 l_aRTC
type family Let1627597129Scrutinee_1627597071 x_aRTx y_aRTy where
Let1627597129Scrutinee_1627597071 x_aRTx y_aRTy = Data.Singletons.Apply (Data.Singletons.Apply CompareSym0 x_aRTx) y_aRTy
type family Case_1627597137_aRTI x_aRTx y_aRTy t_aRTJ where
Case_1627597137_aRTI x_aRTx y_aRTy LT = TrueSym0
Case_1627597137_aRTI x_aRTx y_aRTy EQ = TrueSym0
Case_1627597137_aRTI x_aRTx y_aRTy GT = FalseSym0
type family TFHelper_1627597142_aRTN (a_aRTK :: a_aRSA)
(a_aRTL :: a_aRSA) :: Bool where
TFHelper_1627597142_aRTN x_aRTx y_aRTy = Case_1627597137_aRTI x_aRTx y_aRTy (Let1627597129Scrutinee_1627597071Sym2 x_aRTx y_aRTy)
type TFHelper_1627597142Sym2 (t_aRTO :: a1627597068)
(t_aRTP :: a1627597068) =
TFHelper_1627597142_aRTN t_aRTO t_aRTP
data TFHelper_1627597142Sym1 (l_aRTT :: a1627597068)
(l_aRTS :: Data.Singletons.TyFun a1627597068 Bool)
= forall arg_aRTU. Data.Singletons.KindOf (Data.Singletons.Apply (TFHelper_1627597142Sym1 l_aRTT) arg_aRTU) ~ Data.Singletons.KindOf (TFHelper_1627597142Sym2 l_aRTT arg_aRTU) =>
TFHelper_1627597142Sym1KindInference
type instance Data.Singletons.Apply (TFHelper_1627597142Sym1 l_aRTT) l_aRTS = TFHelper_1627597142Sym2 l_aRTT l_aRTS
data TFHelper_1627597142Sym0 (l_aRTQ :: Data.Singletons.TyFun a1627597068 (Data.Singletons.TyFun a1627597068 Bool
-> GHC.Types.Type))
= forall arg_aRTR. Data.Singletons.KindOf (Data.Singletons.Apply TFHelper_1627597142Sym0 arg_aRTR) ~ Data.Singletons.KindOf (TFHelper_1627597142Sym1 arg_aRTR) =>
TFHelper_1627597142Sym0KindInference
type instance Data.Singletons.Apply TFHelper_1627597142Sym0 l_aRTQ = TFHelper_1627597142Sym1 l_aRTQ
class PEq a_aRSA => POrd a_aRSA where
type Compare (arg_aRSF :: a_aRSA) (arg_aRSG :: a_aRSA) :: Ordering
type (:<) (arg_aRSO :: a_aRSA) (arg_aRSP :: a_aRSA) :: Bool
type (:<=) (arg_aRSX :: a_aRSA) (arg_aRSY :: a_aRSA) :: Bool
type (:>) (arg_aRT6 :: a_aRSA) (arg_aRT7 :: a_aRSA) :: Bool
type (:>=) (arg_aRTf :: a_aRSA) (arg_aRTg :: a_aRSA) :: Bool
type (:<=) a_aRTK
a_aRTL = Data.Singletons.Apply (Data.Singletons.Apply TFHelper_1627597142Sym0 a_aRTK) a_aRTL
class SEq a_aRSA => SOrd a_aRSA where
sCompare ::
forall (t_aRTV :: a_aRSA) (t_aRTW :: a_aRSA).
Sing t_aRTV
-> Sing t_aRTW
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply CompareSym0 t_aRTV) t_aRTW :: Ordering)
(%:<) ::
forall (t_aRTX :: a_aRSA) (t_aRTY :: a_aRSA).
Sing t_aRTX
-> Sing t_aRTY
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply (:<$) t_aRTX) t_aRTY :: Bool)
(%:<=) ::
forall (t_aRTZ :: a_aRSA) (t_aRU0 :: a_aRSA).
Sing t_aRTZ
-> Sing t_aRU0
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply (:<=$) t_aRTZ) t_aRU0 :: Bool)
(%:>) ::
forall (t_aRU1 :: a_aRSA) (t_aRU2 :: a_aRSA).
Sing t_aRU1
-> Sing t_aRU2
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply (:>$) t_aRU1) t_aRU2 :: Bool)
(%:>=) ::
forall (t_aRU3 :: a_aRSA) (t_aRU4 :: a_aRSA).
Sing t_aRU3
-> Sing t_aRU4
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply (:>=$) t_aRU3) t_aRU4 :: Bool)
default (%:<=) ::
forall (t_aRTZ :: a_aRSA) (t_aRU0 :: a_aRSA).
Data.Singletons.Apply (Data.Singletons.Apply (:<=$) t_aRTZ) t_aRU0 ~ Data.Singletons.Apply (Data.Singletons.Apply TFHelper_1627597142Sym0 t_aRTZ) t_aRU0 =>
Sing t_aRTZ
-> Sing t_aRU0
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply (:<=$) t_aRTZ) t_aRU0 :: Bool)
(%:<=) sX sY
= let
lambda_aRU5 ::
forall x_aRTx y_aRTy.
(t_aRTZ ~ x_aRTx, t_aRU0 ~ y_aRTy) =>
Sing x_aRTx
-> Sing y_aRTy
-> Sing (Data.Singletons.Apply (Data.Singletons.Apply (:<=$) t_aRTZ) t_aRU0 :: Bool)
lambda_aRU5 x_aRU6 y_aRU7
= let
sScrutinee_1627597071 ::
Sing (Let1627597129Scrutinee_1627597071Sym2 x_aRTx y_aRTy)
sScrutinee_1627597071
= Data.Singletons.applySing
(Data.Singletons.applySing
(Data.Singletons.singFun2
(Data.Proxy.Proxy :: Data.Proxy.Proxy CompareSym0) sCompare)
x_aRU6)
y_aRU7
in case sScrutinee_1627597071 of {
SLT
-> let
lambda_aRU8 ::
LTSym0 ~ Let1627597129Scrutinee_1627597071Sym2 x_aRTx y_aRTy =>
Sing (Case_1627597137_aRTI x_aRTx y_aRTy LTSym0 :: Bool)
lambda_aRU8 = STrue
in lambda_aRU8;
SEQ
-> let
lambda_aRU9 ::
EQSym0 ~ Let1627597129Scrutinee_1627597071Sym2 x_aRTx y_aRTy =>
Sing (Case_1627597137_aRTI x_aRTx y_aRTy EQSym0 :: Bool)
lambda_aRU9 = STrue
in lambda_aRU9;
SGT
-> let
lambda_aRUa ::
GTSym0 ~ Let1627597129Scrutinee_1627597071Sym2 x_aRTx y_aRTy =>
Sing (Case_1627597137_aRTI x_aRTx y_aRTy GTSym0 :: Bool)
lambda_aRUa = SFalse
in lambda_aRUa } ::
Sing (Case_1627597137_aRTI x_aRTx y_aRTy (Let1627597129Scrutinee_1627597071Sym2 x_aRTx y_aRTy) :: Bool)
in lambda_aRU5 sX sY
