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)
    type family LamCases_0123456789876543210 (x0123456789876543210 :: a0123456789876543210) a_0123456789876543210 where
      LamCases_0123456789876543210 x 'True = FromInteger 1
      LamCases_0123456789876543210 x 'False = Apply (Apply ($@#@$) TypeErrorSym0) (Apply ShowTypeSym0 x)
    data LamCases_0123456789876543210Sym0 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210
      where
        LamCases_0123456789876543210Sym0KindInference :: SameKind (Apply (LamCases_0123456789876543210Sym0 x0123456789876543210) arg) (LamCases_0123456789876543210Sym1 x0123456789876543210 arg) =>
                                                         LamCases_0123456789876543210Sym0 x0123456789876543210 a_01234567898765432100123456789876543210
    type instance Apply @_ @_ (LamCases_0123456789876543210Sym0 x0123456789876543210) a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
    instance SuppressUnusedWarnings (LamCases_0123456789876543210Sym0 x0123456789876543210) where
      suppressUnusedWarnings
        = snd ((,) LamCases_0123456789876543210Sym0KindInference ())
    type family LamCases_0123456789876543210Sym1 (x0123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 where
      LamCases_0123456789876543210Sym1 x0123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 a_01234567898765432100123456789876543210
    type FooSym0 :: (~>) a a
    data FooSym0 :: (~>) a a
      where
        FooSym0KindInference :: SameKind (Apply FooSym0 arg) (FooSym1 arg) =>
                                FooSym0 a0123456789876543210
    type instance Apply @a @a FooSym0 a0123456789876543210 = Foo a0123456789876543210
    instance SuppressUnusedWarnings FooSym0 where
      suppressUnusedWarnings = snd ((,) FooSym0KindInference ())
    type FooSym1 :: a -> a
    type family FooSym1 @a (a0123456789876543210 :: a) :: a where
      FooSym1 a0123456789876543210 = Foo a0123456789876543210
    type Foo :: a -> a
    type family Foo @a (a :: a) :: a where
      Foo x = Apply (LamCases_0123456789876543210Sym0 x) (Apply (Apply (==@#@$) x) (FromInteger 0))
    sFoo ::
      (forall (t :: a).
       (SNum a, SEq a) => Sing t -> Sing (Foo t :: a) :: Type)
    sFoo (sX :: Sing x)
      = applySing
          (singFun1
             @(LamCases_0123456789876543210Sym0 x)
             (\cases
                STrue -> sFromInteger (sing :: Sing 1)
                SFalse
                  -> applySing
                       (applySing
                          (singFun2 @($@#@$) (%$)) (singFun1 @TypeErrorSym0 sTypeError))
                       (applySing (singFun1 @ShowTypeSym0 SShowType) sX)))
          (applySing
             (applySing (singFun2 @(==@#@$) (%==)) sX)
             (sFromInteger (sing :: Sing 0)))
    instance (SNum a, SEq a) => SingI (FooSym0 :: (~>) a a) where
      sing = singFun1 @FooSym0 sFoo
Singletons/T160.hs:0:0: error: [GHC-64725]
    • 1
    • In the expression: Refl
      In an equation for ‘f’: f = Refl
   |
13 | f = Refl
   |     ^^^^