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

module NatSymbolReflexive where

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

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

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