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