Copyright | (c) Galois Inc 2019 |
---|---|

Safe Haskell | None |

Language | Haskell98 |

This module declares a class with a single method that can be used to
derive a `KnownRepr`

constraint from an explicit `Repr`

argument.
Clients of this method need only create an empty instance. The default
implementation suffices.

For example, suppose we have defined a `Repr`

type for `Peano`

numbers:

data Peano = Z | S Peano data PeanoRepr p where ZRepr :: PeanoRepr Z SRepr :: PeanoRepr p -> PeanoRepr (S p) -- KnownRepr instances

Then the instance for this class
```
instance IsRepr PeanoRepr
```

means that functions with `KnownRepr`

constraints can be used after
pattern matching.

f :: KnownRepr PeanoRepr a => ... example :: PeanoRepr n -> ... example ZRepr = ... example (SRepr (pm::PeanoRepr m)) = ... withRepr pm f ...

NOTE: The type `f`

must be a *singleton* type--- i.e. for a given
type `a`

there should be only one value that inhabits 'f a'. If that
is not the case, this operation can be used to subvert coherence.

Credit: the unsafe implementation of `withRepr`

is taken from the
`withSingI`

function in the singletons library
http://hackage.haskell.org/package/singletons-2.5.1/. Packaging
this method in a class here makes it more flexible---we do not have to
define a dedicated `Sing`

type, but can use any convenient singleton
as a `Repr`

.

NOTE: if this module is compiled without 1, the default method will not be available.

# Documentation

class IsRepr (f :: k -> *) where Source #

Turn an explicit Repr value into an implict KnownRepr constraint

Nothing

## Instances

IsRepr BoolRepr Source # | |

IsRepr NatRepr Source # | |

IsRepr SymbolRepr Source # | |

Defined in Data.Parameterized.WithRepr withRepr :: SymbolRepr a -> (KnownRepr SymbolRepr a -> r) -> r Source # | |

IsRepr PeanoRepr Source # | |

IsRepr f => IsRepr (List f :: [k] -> Type) Source # | |

IsRepr f => IsRepr (Assignment f :: Ctx k -> Type) Source # | |

Defined in Data.Parameterized.WithRepr withRepr :: Assignment f a -> (KnownRepr (Assignment f) a -> r) -> r Source # |