| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Util.StubbedProof
Description
Utilities for (slightly unsafely) stubbing typelevel proofs.
Synopsis
- assumeKnown :: forall xs. Stubbed => KList xs
- assumeSing :: forall x. Stubbed => Sing x
- stubProof :: forall a b. (Stubbed => a :~: b) -> a :~: b
Documentation
assumeKnown :: forall xs. Stubbed => KList xs Source #
Assume a KnownList by providing a fake KList. Can only be done inside a
Stubbed proof. This is not entirely safe due to the existence of things
like Any, and with enough effort one could theoretically get an
unsafeCoerce out of a proof that uses this, but arguably it's "safe
enough".
assumeSing :: forall x. Stubbed => Sing x Source #
Assume SingI by providing a fake Sing. Can only be done inside a
Stubbed proof. Same caveats apply as with assumeKnown.