search

goldfirere / ghc

Mirror of ghc repository. DO NOT SUBMIT PULL REQUESTS HERE
http://www.haskell.org/ghc/
Other
25 stars 1 forks source link

Not in scope while type-checking #69

Open goldfirere opened 8 years ago

goldfirere commented 8 years ago 
{-# 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