parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

Copyright | (c) Galois Inc 2014-2021
Safe Haskell | Unsafe
Language | Haskell2010

Data.Parameterized.Axiom

Description

An unsafe module that provides functionality for constructing equality proofs that GHC cannot prove on its own.

Synopsis

- unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b
- unsafeHeteroAxiom :: forall {k1} {k2} (a :: k1) (b :: k2). a :~~: b

# Documentation

unsafeAxiom :: forall {k} (a :: k) (b :: k). a :~: b Source #

Assert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!

unsafeHeteroAxiom :: forall {k1} {k2} (a :: k1) (b :: k2). a :~~: b Source #

Assert a proof of heterogeneous equality between two types. This is unsafe if used improperly, so use this with caution!