{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeApplications #-} module Data.Type.Natural.Utils where import Data.Type.Equality (type (:~:) (..)) import Unsafe.Coerce (unsafeCoerce) trustMe :: x :~: y trustMe :: x :~: y trustMe = (() :~: ()) -> x :~: y forall a b. a -> b unsafeCoerce (() :~: () forall k (a :: k). a :~: a Refl @())