FunDeps.ghc80.template

Singletons/FunDeps.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| t1 = meth True
          
          class FD a b | a -> b where
            meth :: a -> a
            l2r :: a -> b
          
          instance FD Bool Nat where
            meth = not
            l2r False = 0
            l2r True = 1 |]
  ======>
    class FD a b | a -> b where
      meth :: a -> a
      l2r :: a -> b
    instance FD Bool Nat where
      meth = not
      l2r False = 0
      l2r True = 1
    t1 = meth True
    type T1Sym0 = T1
    type family T1 where
      T1 = Apply MethSym0 TrueSym0
    type MethSym1 (t :: a0123456789) = Meth t
    instance SuppressUnusedWarnings MethSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) MethSym0KindInference GHC.Tuple.())
    data MethSym0 (l :: TyFun a0123456789 a0123456789)
      = forall arg. KindOf (Apply MethSym0 arg) ~ KindOf (MethSym1 arg) =>
        MethSym0KindInference
    type instance Apply MethSym0 l = MethSym1 l
    type L2rSym1 (t :: a0123456789) = L2r t
    instance SuppressUnusedWarnings L2rSym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) L2rSym0KindInference GHC.Tuple.())
    data L2rSym0 (l :: TyFun a0123456789 b0123456789)
      = forall arg. KindOf (Apply L2rSym0 arg) ~ KindOf (L2rSym1 arg) =>
        L2rSym0KindInference
    type instance Apply L2rSym0 l = L2rSym1 l
    class (kproxy ~ Proxy, kproxy ~ Proxy) => PFD (kproxy :: Proxy a)
                                                  (kproxy :: Proxy b) | a -> b where
      type Meth (arg :: a) :: a
      type L2r (arg :: a) :: b
    type family Meth_0123456789 (a :: Bool) :: Bool where
      Meth_0123456789 a_0123456789 = Apply NotSym0 a_0123456789
    type Meth_0123456789Sym1 (t :: Bool) = Meth_0123456789 t
    instance SuppressUnusedWarnings Meth_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) Meth_0123456789Sym0KindInference GHC.Tuple.())
    data Meth_0123456789Sym0 (l :: TyFun Bool Bool)
      = forall arg. KindOf (Apply Meth_0123456789Sym0 arg) ~ KindOf (Meth_0123456789Sym1 arg) =>
        Meth_0123456789Sym0KindInference
    type instance Apply Meth_0123456789Sym0 l = Meth_0123456789Sym1 l
    type family L2r_0123456789 (a :: Bool) :: Nat where
      L2r_0123456789 False = FromInteger 0
      L2r_0123456789 True = FromInteger 1
    type L2r_0123456789Sym1 (t :: Bool) = L2r_0123456789 t
    instance SuppressUnusedWarnings L2r_0123456789Sym0 where
      suppressUnusedWarnings _
        = snd (GHC.Tuple.(,) L2r_0123456789Sym0KindInference GHC.Tuple.())
    data L2r_0123456789Sym0 (l :: TyFun Bool Nat)
      = forall arg. KindOf (Apply L2r_0123456789Sym0 arg) ~ KindOf (L2r_0123456789Sym1 arg) =>
        L2r_0123456789Sym0KindInference
    type instance Apply L2r_0123456789Sym0 l = L2r_0123456789Sym1 l
    instance PFD (Proxy :: Proxy Bool) (Proxy :: Proxy Nat) where
      type Meth (a :: Bool) = Apply Meth_0123456789Sym0 a
      type L2r (a :: Bool) = Apply L2r_0123456789Sym0 a
    sT1 :: Sing T1Sym0
    sT1 = applySing (singFun1 (Proxy :: Proxy MethSym0) sMeth) STrue
    class SFD a b | a -> b where
      sMeth :: forall (t :: a). Sing t -> Sing (Apply MethSym0 t :: a)
      sL2r :: forall (t :: a). Sing t -> Sing (Apply L2rSym0 t :: b)
    instance SFD Bool Nat where
      sMeth ::
        forall (t :: Bool). Sing t -> Sing (Apply MethSym0 t :: Bool)
      sL2r :: forall (t :: Bool). Sing t -> Sing (Apply L2rSym0 t :: Nat)
      sMeth sA_0123456789
        = let
            lambda ::
              forall a_0123456789.
              t ~ a_0123456789 =>
              Sing a_0123456789 -> Sing (Apply MethSym0 t :: Bool)
            lambda a_0123456789
              = applySing (singFun1 (Proxy :: Proxy NotSym0) sNot) a_0123456789
          in lambda sA_0123456789
      sL2r SFalse
        = let
            lambda :: t ~ FalseSym0 => Sing (Apply L2rSym0 t :: Nat)
            lambda = sFromInteger (sing :: Sing 0)
          in lambda
      sL2r STrue
        = let
            lambda :: t ~ TrueSym0 => Sing (Apply L2rSym0 t :: Nat)
            lambda = sFromInteger (sing :: Sing 1)
          in lambda