Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Not in scope while type-checking #69

Open
goldfirere opened this issue Jun 13, 2016 · 0 comments
Open

Not in scope while type-checking #69

goldfirere opened this issue Jun 13, 2016 · 0 comments

Comments

@goldfirere
Copy link
Owner 

{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@goldfirere