Singletons/T160.hs:(0,0)-(0,0): Splicing declarations
    singletons
      [d| foo :: (Num a, Eq a) => a -> a
          foo x = if x == 0 then 1 else typeError $ ShowType x |]
  ======>
    foo :: (Num a, Eq a) => a -> a
    foo x = if (x == 0) then 1 else (typeError $ ShowType x)
    type Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210 =
        Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
               ())
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: forall x0123456789876543210
                                                                                       arg. SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210 x0123456789876543210
    type family Let0123456789876543210Scrutinee_0123456789876543210 x where
      Let0123456789876543210Scrutinee_0123456789876543210 x = Apply (Apply (==@#@$) x) (FromInteger 0)
    type family Case_0123456789876543210 x t where
      Case_0123456789876543210 x  'True = FromInteger 1
      Case_0123456789876543210 x  'False = Apply (Apply ($@#@$) TypeErrorSym0) (Apply ShowTypeSym0 x)
    type FooSym1 (a0123456789876543210 :: a0123456789876543210) =
        Foo a0123456789876543210
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings = snd (((,) FooSym0KindInference) ())
    data FooSym0 :: forall a0123456789876543210.
                    (~>) a0123456789876543210 a0123456789876543210
      where
        FooSym0KindInference :: forall a0123456789876543210
                                       arg. SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
                                FooSym0 a0123456789876543210
    type instance Apply FooSym0 a0123456789876543210 = Foo a0123456789876543210
    type family Foo (a :: a) :: a where
      Foo x = Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)
    sFoo ::
      forall a (t :: a).
      (SNum a, SEq a) => Sing t -> Sing (Apply FooSym0 t :: a)
    sFoo (sX :: Sing x)
      = let
          sScrutinee_0123456789876543210 ::
            Sing (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)
          sScrutinee_0123456789876543210
            = (applySing ((applySing ((singFun2 @(==@#@$)) (%==))) sX))
                (sFromInteger (sing :: Sing 0))
        in  (case sScrutinee_0123456789876543210 of
               STrue -> sFromInteger (sing :: Sing 1)
               SFalse
                 -> (applySing ((applySing ((singFun2 @($@#@$)) (%$))) sTypeError))
                      ((applySing ((singFun1 @ShowTypeSym0) SShowType)) sX)) ::
              Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: a)
    instance (SNum a, SEq a) => SingI (FooSym0 :: (~>) a a) where
      sing = (singFun1 @FooSym0) sFoo

Singletons/T160.hs:0:0: error:
    • t
    • In the expression:
        (applySing ((applySing ((singFun2 @($@#@$)) (%$))) sTypeError))
          ((applySing ((singFun1 @ShowTypeSym0) SShowType)) sX)
      In a case alternative:
          SFalse
            -> (applySing ((applySing ((singFun2 @($@#@$)) (%$))) sTypeError))
                 ((applySing ((singFun1 @ShowTypeSym0) SShowType)) sX)
      In the expression:
          (case sScrutinee_0123456789876543210 of
             STrue -> sFromInteger (sing :: Sing 1)
             SFalse
               -> (applySing ((applySing ((singFun2 @($@#@$)) (%$))) sTypeError))
                    ((applySing ((singFun1 @ShowTypeSym0) SShowType)) sX)) ::
            Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: a)
  |
7 | $(singletons
  |   ^^^^^^^^^^...

Singletons/T160.hs:0:0: error:
    • 1
    • In the expression: Refl
      In an equation for ‘f’: f = Refl
   |
13 | f = Refl
   |     ^^^^