singletons-2.5: tests/compile-and-dump/Singletons/NatSymbolReflexive.hs

module NatSymbolReflexive where

import Data.Singletons.Prelude
import Data.Type.Equality ((:~:)(..))
import GHC.TypeLits

test1 :: forall (a :: Nat). Sing a -> (a == a) :~: True
test1 _ = Refl

test2 :: forall (a :: Symbol). Sing a -> (a == a) :~: True
test2 _ = Refl