T160.golden

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)
    data Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
      where
        Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference :: SameKind (Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 arg) (Let0123456789876543210Scrutinee_0123456789876543210Sym1 arg) =>
                                                                                Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210
    type instance Apply Let0123456789876543210Scrutinee_0123456789876543210Sym0 x0123456789876543210 = Let0123456789876543210Scrutinee_0123456789876543210Sym1 x0123456789876543210
    instance SuppressUnusedWarnings Let0123456789876543210Scrutinee_0123456789876543210Sym0 where
      suppressUnusedWarnings
        = snd
            (((,)
                Let0123456789876543210Scrutinee_0123456789876543210Sym0KindInference)
               ())
    type Let0123456789876543210Scrutinee_0123456789876543210Sym1 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 FooSym0 :: (~>) a a
    data FooSym0 a0123456789876543210
      where
        FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
                                FooSym0 a0123456789876543210
    type instance Apply FooSym0 a0123456789876543210 = FooSym1 a0123456789876543210
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings = snd (((,) FooSym0KindInference) ())
    type FooSym1 (a0123456789876543210 :: a) =
        Foo a0123456789876543210 :: a
    type Foo :: a -> a
    type family Foo 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
          (id
             @(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: a)))
            (case sScrutinee_0123456789876543210 of
               STrue -> sFromInteger (sing :: Sing 1)
               SFalse
                 -> (applySing
                       ((applySing ((singFun2 @($@#@$)) (%$)))
                          ((singFun1 @TypeErrorSym0) sTypeError)))
                      ((applySing ((singFun1 @ShowTypeSym0) SShowType)) sX))
    instance (SNum a, SEq a) => SingI (FooSym0 :: (~>) a a) where
      sing = (singFun1 @FooSym0) sFoo

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