Explicit NoStarIsType with Data.Kind.Type and increasing do indentation (for GHC 8.6)

This commit is contained in:
Kevin Quick 2018-11-20 09:43:48 +00:00
parent 5f75652a37
commit 7a64cb614f
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
12 changed files with 139 additions and 115 deletions

View File

@ -3,7 +3,7 @@ version: 0.3.2
author: Galois, Inc.
maintainer: jhendrix@galois.com
build-type: Simple
cabal-version: >= 1.9.2
cabal-version: >= 1.10
license: BSD3
license-file: LICENSE
description:
@ -80,3 +80,7 @@ library
ghc-options: -Wall
ghc-options: -fno-warn-unticked-promoted-constructors
ghc-prof-options: -O2 -fprof-auto-top
default-language: Haskell2010
if impl(ghc >= 8.6)
default-extensions: NoStarIsType

View File

@ -66,6 +66,7 @@ import Data.Bits
import Data.Foldable
import Data.Functor
import Data.Int
import qualified Data.Kind as Kind
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
@ -1316,7 +1317,7 @@ transferApp r a = do
_ -> TopV
-- | Minimal information needed to parse a function call/system call
data CallParams (r :: Type -> *)
data CallParams (r :: Type -> Kind.Type)
= CallParams { postCallStackDelta :: Integer
-- ^ Amount stack should shift by when going before/after call.
, preserveReg :: forall tp . r tp -> Bool

View File

@ -34,6 +34,7 @@ module Data.Macaw.Analysis.FunctionArgs
import Control.Lens
import Control.Monad.State.Strict
import Data.Foldable as Fold (traverse_)
import qualified Data.Kind as Kind
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
@ -81,13 +82,13 @@ import Data.Macaw.Types
-- demanded?
-- | A set of registrs
type RegisterSet (r :: Type -> *) = Set (Some r)
type RegisterSet (r :: Type -> Kind.Type) = Set (Some r)
-- | A memory segment offset compatible with the architecture registers.
type RegSegmentOff r = MemSegmentOff (RegAddrWidth r)
-- | This stores the registers needed by a specific address
data DemandSet (r :: Type -> *) =
data DemandSet (r :: Type -> Kind.Type) =
DemandSet { registerDemands :: !(RegisterSet r)
-- | This maps a function address to the registers
-- that it needs.

View File

@ -21,6 +21,7 @@ module Data.Macaw.CFG.App
, ppAppA
) where
import qualified Data.Kind as Kind
import Control.Monad.Identity
import Data.Parameterized.Classes
import qualified Data.Parameterized.List as P
@ -40,7 +41,7 @@ import Data.Macaw.Utils.Pretty
-- These operations are all total functions. Different architecture tend to have
-- different ways of raising signals or exceptions, and so partial functions are
-- all architecture specific.
data App (f :: Type -> *) (tp :: Type) where
data App (f :: Type -> Kind.Type) (tp :: Type) where
-- Compare for equality.
Eq :: !(f tp) -> !(f tp) -> App f BoolType

View File

@ -6,6 +6,8 @@
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.CFG.AssignRhs
( AssignRhs(..)
-- * MemRepr
@ -25,6 +27,7 @@ module Data.Macaw.CFG.AssignRhs
, ArchMemAddr
) where
import qualified Data.Kind as Kind
import Data.Macaw.CFG.App
import Data.Macaw.Memory (Endianness(..), MemSegmentOff, MemWord, MemAddr)
import Data.Macaw.Types
@ -36,8 +39,11 @@ import Data.Parameterized.TraversableFC (FoldableFC(..))
import Data.Proxy
import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
import Prelude
-- | Width of register used to store addresses.
type family RegAddrWidth (r :: Type -> *) :: Nat
type family RegAddrWidth (r :: Type -> Kind.Type) :: Nat
-- | A word for the given architecture register type.
type RegAddrWord r = MemWord (RegAddrWidth r)
@ -46,7 +52,7 @@ type RegAddrWord r = MemWord (RegAddrWidth r)
--
-- Registers include things like the general purpose registers, any flag
-- registers that can be read and written without side effects,
type family ArchReg (arch :: *) = (reg :: Type -> *) | reg -> arch
type family ArchReg (arch :: Kind.Type) = (reg :: Type -> Kind.Type) | reg -> arch
-- Note the injectivity constraint. This makes GHC quit bothering us
-- about ambigous types for functions taking ArchRegs as arguments.
@ -57,13 +63,13 @@ type family ArchReg (arch :: *) = (reg :: Type -> *) | reg -> arch
--
-- The function may depend on the set of registers defined so far, and the type
-- of the result.
type family ArchFn (arch :: *) = (fn :: (Type -> *) -> Type -> *) | fn -> arch
type family ArchFn (arch :: Kind.Type) = (fn :: (Type -> Kind.Type) -> Type -> Kind.Type) | fn -> arch
-- | A type family for defining architecture-specific statements.
--
-- The second parameter is used to denote the underlying values in the
-- statements so that we can use ArchStmts with multiple CFGs.
type family ArchStmt (arch :: *) = (stmt :: (Type -> *) -> *) | stmt -> arch
type family ArchStmt (arch :: Kind.Type) = (stmt :: (Type -> Kind.Type) -> Kind.Type) | stmt -> arch
-- | A type family for defining architecture-specific statements that
-- may have instruction-specific effects on control-flow and register state.
@ -75,7 +81,7 @@ type family ArchStmt (arch :: *) = (stmt :: (Type -> *) -> *) | stmt -> arch
-- values, it may or may not return to the current function. If it does return to the
-- current function, it is assumed to be at most one location, and the block-translator
-- must provide that value at translation time.
type family ArchTermStmt (arch :: *) :: * -> *
type family ArchTermStmt (arch :: Kind.Type) :: Kind.Type -> Kind.Type
-- NOTE: Not injective because PPC32 and PPC64 use the same type.
-- | Number of bits in addreses for architecture.
@ -134,7 +140,7 @@ instance HasRepr MemRepr TypeRepr where
-- | The right hand side of an assignment is an expression that
-- returns a value.
data AssignRhs (arch :: *) (f :: Type -> *) tp where
data AssignRhs (arch :: Kind.Type) (f :: Type -> Kind.Type) tp where
-- | An expression that is computed from evaluating subexpressions.
EvalApp :: !(App f tp)
-> AssignRhs arch f tp

View File

@ -6,6 +6,8 @@ This exports the pre-classification term statement and block data
types.
-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.CFG.Block
( Block(..)
, ppBlock

View File

@ -7,6 +7,7 @@ Defines data types needed to represent values, assignments, and statements from
This is a low-level CFG representation where the entire program is a
single CFG.
-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
@ -21,7 +22,8 @@ single CFG.
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Macaw.CFG.Core
( -- * Stmt level declarations
Stmt(..)
@ -84,6 +86,7 @@ import Control.Monad.Identity
import Control.Monad.State.Strict
import Data.Bits
import Data.Int (Int64)
import qualified Data.Kind as Kind
import Data.Maybe (isNothing, catMaybes)
import Data.Parameterized.Classes
import Data.Parameterized.Map (MapF)
@ -125,7 +128,7 @@ class PrettyPrec v where
prettyPrec :: Int -> v -> Doc
-- | Pretty print over all instances of a type.
class PrettyF (f :: k -> *) where
class PrettyF (f :: k -> Kind.Type) where
prettyF :: f tp -> Doc
-- | Pretty print a document with parens if condition is true
@ -153,7 +156,7 @@ addrWidthTypeRepr Addr64 = BVTypeRepr knownNat
-- form. 'AssignId's are typed, and also include a type variable @ids@
-- that intuitively denotes the set of identifiers from which they are
-- drawn.
newtype AssignId (ids :: *) (tp :: Type) = AssignId (Nonce ids tp)
newtype AssignId (ids :: Kind.Type) (tp :: Type) = AssignId (Nonce ids tp)
ppAssignId :: AssignId ids tp -> Doc
ppAssignId (AssignId w) = text ("r" ++ show (indexValue w))
@ -392,7 +395,7 @@ class IPAlignment arch where
-- RegState
-- | This represents the state of the processor registers.
newtype RegState (r :: k -> *) (f :: k -> *) = RegState (MapF.MapF r f)
newtype RegState (r :: k -> Kind.Type) (f :: k -> Kind.Type) = RegState (MapF.MapF r f)
deriving instance (OrdF r, EqF f) => Eq (RegState r f)
@ -539,7 +542,7 @@ instance RegisterInfo (ArchReg arch) => Show (Value arch ids tp) where
show = show . pretty
-- | Typeclass for architecture-specific functions
class IsArchFn (f :: (Type -> *) -> Type -> *) where
class IsArchFn (f :: (Type -> Kind.Type) -> Type -> Kind.Type) where
-- | A function for pretty printing an archFn of a given type.
ppArchFn :: Applicative m
=> (forall u . v u -> m Doc)
@ -548,7 +551,7 @@ class IsArchFn (f :: (Type -> *) -> Type -> *) where
-> m Doc
-- | Typeclass for architecture-specific statements
class IsArchStmt (f :: (Type -> *) -> *) where
class IsArchStmt (f :: (Type -> Kind.Type) -> Kind.Type) where
-- | A function for pretty printing an architecture statement of a given type.
ppArchStmt :: (forall u . v u -> Doc)
-- ^ Function for pretty printing value.
@ -642,7 +645,7 @@ ppValueAssignmentList vals =
-- | This class provides a way of optionally pretty printing the contents
-- of a register or omitting them.
class PrettyRegValue r (f :: Type -> *) where
class PrettyRegValue r (f :: Type -> Kind.Type) where
-- | ppValueEq should return a doc if the contents of the given register
-- should be printed, and Nothing if the contents should be ignored.
ppValueEq :: r tp -> f tp -> Maybe Doc

View File

@ -125,7 +125,7 @@ appendRewrittenStmt stmt = Rewriter $ do
stmts <- use rwRevStmts
let stmts' = stmt : stmts
seq stmt $ seq stmts' $ do
rwRevStmts .= stmts'
rwRevStmts .= stmts'
-- | Add a statment to the list
appendRewrittenArchStmt :: ArchStmt arch (Value arch tgt) -> Rewriter arch s src tgt ()
@ -151,10 +151,10 @@ addBinding :: AssignId src tp -> Value arch tgt tp -> Rewriter arch s src tgt ()
addBinding srcId val = Rewriter $ do
ref <- gets $ rwctxCache . rwContext
lift $ do
m <- readSTRef ref
when (MapF.member srcId m) $ do
fail $ "Assignment " ++ show srcId ++ " is already bound."
writeSTRef ref $! MapF.insert srcId val m
m <- readSTRef ref
when (MapF.member srcId m) $ do
fail $ "Assignment " ++ show srcId ++ " is already bound."
writeSTRef ref $! MapF.insert srcId val m
-- | Return true if values are identical
identValue :: TestEquality (ArchReg arch) => Value arch tgt tp -> Value arch tgt tp -> Bool
@ -171,7 +171,7 @@ rewriteApp :: App (Value arch tgt) tp -> Rewriter arch s src tgt (Value arch tgt
rewriteApp app = do
ctx <- Rewriter $ gets rwContext
rwctxConstraints ctx $ do
case app of
case app of
Trunc (BVValue _ x) w -> do
pure $ BVValue w $ toUnsigned w x

View File

@ -415,13 +415,13 @@ mergeIntraJump :: ArchSegmentOff arch
mergeIntraJump src ab tgt = do
info <- uses curFunCtx archInfo
withArchConstraints info $ do
when (not (absStackHasReturnAddr ab)) $ do
when (not (absStackHasReturnAddr ab)) $ do
debug DCFG ("WARNING: Missing return value in jump from " ++ show src ++ " to\n" ++ show ab) $
pure ()
let rsn = NextIP src
-- Associate a new abstract state with the code region.
foundMap <- use foundAddrs
case Map.lookup tgt foundMap of
let rsn = NextIP src
-- Associate a new abstract state with the code region.
foundMap <- use foundAddrs
case Map.lookup tgt foundMap of
-- We have seen this block before, so need to join and see if
-- the results is changed.
Just old_info -> do
@ -764,8 +764,8 @@ recordWriteStmt arch_info mem regs stmt = do
WriteMem _addr repr v
| Just Refl <- testEquality repr (addrMemRepr arch_info) -> do
withArchConstraints arch_info $ do
let addrs = identifyConcreteAddresses mem (transferValue regs v)
writtenCodeAddrs %= (filter isExecutableSegOff addrs ++)
let addrs = identifyConcreteAddresses mem (transferValue regs v)
writtenCodeAddrs %= (filter isExecutableSegOff addrs ++)
_ -> return ()
------------------------------------------------------------------------
@ -840,10 +840,10 @@ parseFetchAndExecute ctx idx stmts regs s = do
let ainfo= pctxArchInfo ctx
let absProcState' = absEvalStmts ainfo regs stmts
withArchConstraints ainfo $ do
-- See if next statement appears to end with a call.
-- We define calls as statements that end with a write that
-- stores the pc to an address.
case () of
-- See if next statement appears to end with a call.
-- We define calls as statements that end with a write that
-- stores the pc to an address.
case () of
_ | Just (Mux _ c t f) <- valueAsApp (s^.boundValue ip_reg) -> do
mapM_ (recordWriteStmt ainfo mem absProcState') stmts
@ -876,19 +876,19 @@ parseFetchAndExecute ctx idx stmts regs s = do
mapM_ (recordWriteStmt ainfo mem absProcState') prev_stmts
let abst = finalAbsBlockState absProcState' s
seq abst $ do
-- Merge caller return information
intraJumpTargets %= ((ret, postCallAbsState ainfo abst ret):)
-- Use the abstract domain to look for new code pointers for the current IP.
addNewFunctionAddrs $
identifyCallTargets mem abst s
-- Use the call-specific code to look for new IPs.
-- Merge caller return information
intraJumpTargets %= ((ret, postCallAbsState ainfo abst ret):)
-- Use the abstract domain to look for new code pointers for the current IP.
addNewFunctionAddrs $
identifyCallTargets mem abst s
-- Use the call-specific code to look for new IPs.
let r = StatementList { stmtsIdent = idx
, stmtsNonterm = toList prev_stmts
, stmtsTerm = ParsedCall s (Just ret)
, stmtsAbsState = absProcState'
}
pure (r, idx+1)
let r = StatementList { stmtsIdent = idx
, stmtsNonterm = toList prev_stmts
, stmtsTerm = ParsedCall s (Just ret)
, stmtsAbsState = absProcState'
}
pure (r, idx+1)
-- This block ends with a return as identified by the
-- architecture-specific processing. Basic return
@ -993,16 +993,16 @@ parseFetchAndExecute ctx idx stmts regs s = do
let abst = finalAbsBlockState absProcState' s
seq abst $ do
-- Look for new instruction pointers
addNewFunctionAddrs $
identifyConcreteAddresses mem (abst^.absRegState^.curIP)
-- Look for new instruction pointers
addNewFunctionAddrs $
identifyConcreteAddresses mem (abst^.absRegState^.curIP)
let ret = StatementList { stmtsIdent = idx
, stmtsNonterm = stmts
, stmtsTerm = ParsedCall s Nothing
, stmtsAbsState = absProcState'
}
seq ret $ pure (ret,idx+1)
let ret = StatementList { stmtsIdent = idx
, stmtsNonterm = stmts
, stmtsTerm = ParsedCall s Nothing
, stmtsAbsState = absProcState'
}
seq ret $ pure (ret,idx+1)
-- | this evalutes the statements in a block to expand the information known
-- about control flow targets of this block.
@ -1019,7 +1019,7 @@ parseBlock ctx idx b regs = do
let mem = pctxMemory ctx
let ainfo = pctxArchInfo ctx
withArchConstraints ainfo $ do
case blockTerm b of
case blockTerm b of
Branch c lb rb -> do
let blockMap = pctxBlockMap ctx
-- FIXME: we should propagate c back to the initial block, not just b
@ -1136,56 +1136,56 @@ transfer addr = do
s <- use curFunCtx
let ainfo = archInfo s
withArchConstraints ainfo $ do
mfinfo <- use $ foundAddrs . at addr
let finfo = fromMaybe (error $ "transfer called on unfound address " ++ show addr ++ ".") $
mfinfo
let mem = memory s
nonceGen <- gets funNonceGen
prev_block_map <- use $ curFunBlocks
-- Get maximum number of bytes to disassemble
let maxSize :: Int
maxSize =
case Map.lookupGT addr prev_block_map of
Just (next,_) | Just o <- diffSegmentOff next addr -> fromInteger o
_ -> fromInteger (segoffBytesLeft addr)
let ab = foundAbstractState finfo
(bs0, sz, maybeError) <- liftST $ disassembleFn ainfo nonceGen addr maxSize ab
mfinfo <- use $ foundAddrs . at addr
let finfo = fromMaybe (error $ "transfer called on unfound address " ++ show addr ++ ".") $
mfinfo
let mem = memory s
nonceGen <- gets funNonceGen
prev_block_map <- use $ curFunBlocks
-- Get maximum number of bytes to disassemble
let maxSize :: Int
maxSize =
case Map.lookupGT addr prev_block_map of
Just (next,_) | Just o <- diffSegmentOff next addr -> fromInteger o
_ -> fromInteger (segoffBytesLeft addr)
let ab = foundAbstractState finfo
(bs0, sz, maybeError) <- liftST $ disassembleFn ainfo nonceGen addr maxSize ab
#ifdef USE_REWRITER
bs1 <- do
let archStmt = rewriteArchStmt ainfo
let secAddrMap = memSectionIndexMap mem
liftST $ do
ctx <- mkRewriteContext nonceGen (rewriteArchFn ainfo) archStmt secAddrMap
traverse (rewriteBlock ainfo ctx) bs0
bs1 <- do
let archStmt = rewriteArchStmt ainfo
let secAddrMap = memSectionIndexMap mem
liftST $ do
ctx <- mkRewriteContext nonceGen (rewriteArchFn ainfo) archStmt secAddrMap
traverse (rewriteBlock ainfo ctx) bs0
#else
bs1 <- pure bs0
bs1 <- pure bs0
#endif
-- If no blocks are returned, then we just add an empty parsed block.
if null bs1 then do
let errMsg = Text.pack $ fromMaybe "Unknown error" maybeError
let stmts = StatementList
{ stmtsIdent = 0
, stmtsNonterm = []
, stmtsTerm = ParsedTranslateError errMsg
, stmtsAbsState = initAbsProcessorState mem (foundAbstractState finfo)
}
let pb = ParsedBlock { pblockAddr = addr
, blockSize = sz
, blockReason = foundReason finfo
, blockAbstractState = foundAbstractState finfo
, blockStatementList = stmts
}
id %= addFunBlock addr pb
else do
-- Rewrite returned blocks to simplify expressions
-- If no blocks are returned, then we just add an empty parsed block.
if null bs1 then do
let errMsg = Text.pack $ fromMaybe "Unknown error" maybeError
let stmts = StatementList
{ stmtsIdent = 0
, stmtsNonterm = []
, stmtsTerm = ParsedTranslateError errMsg
, stmtsAbsState = initAbsProcessorState mem (foundAbstractState finfo)
}
let pb = ParsedBlock { pblockAddr = addr
, blockSize = sz
, blockReason = foundReason finfo
, blockAbstractState = foundAbstractState finfo
, blockStatementList = stmts
}
id %= addFunBlock addr pb
else do
-- Rewrite returned blocks to simplify expressions
-- Compute demand set
let bs = bs1 -- eliminateDeadStmts ainfo bs1
-- Call transfer blocks to calculate parsedblocks
let blockMap = Map.fromList [ (blockLabel b, b) | b <- bs ]
addBlocks addr finfo sz blockMap
-- Compute demand set
let bs = bs1 -- eliminateDeadStmts ainfo bs1
-- Call transfer blocks to calculate parsedblocks
let blockMap = Map.fromList [ (blockLabel b, b) | b <- bs ]
addBlocks addr finfo sz blockMap
------------------------------------------------------------------------
-- Main loop

View File

@ -156,6 +156,8 @@ import Data.Parameterized.NatRepr
import qualified Data.Macaw.Memory.Permissions as Perm
import Prelude
------------------------------------------------------------------------
-- AddrWidthRepr

View File

@ -72,7 +72,7 @@ import qualified Data.IntervalMap.Strict as IMap
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe
import Data.Monoid
import Data.Semigroup
import Data.Set (Set)
import qualified Data.Set as Set
import qualified Data.Vector as V
@ -85,6 +85,9 @@ import Data.Macaw.Memory.LoadCommon
import qualified Data.Macaw.Memory.Permissions as Perm
import Data.Macaw.Memory.Symbols
import Prelude
-- | Return a subrange of a bytestring.
sliceL :: Integral w => Elf.Range w -> L.ByteString -> L.ByteString
sliceL (i,c) = L.take (fromIntegral c) . L.drop (fromIntegral i)
@ -888,8 +891,8 @@ insertElfSegment :: RegionIndex
-> MemLoader w ()
insertElfSegment regIdx addrOff shdrMap contents relocMap phdr = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
when (Elf.phdrMemSize phdr > 0) $ do
reprConstraints w $
when (Elf.phdrMemSize phdr > 0) $ do
let segIdx = Elf.phdrSegmentIndex phdr
seg <- do
let linkBaseOff = fromIntegral (Elf.phdrSegmentVirtAddr phdr)
@ -932,21 +935,21 @@ memoryForElfSegments regIndex addrOff e = do
let hdr = Elf.elfLayoutHeader l
let w = elfAddrWidth (elfClass e)
reprConstraints w $ do
let ph = Elf.allPhdrs l
let contents = elfLayoutBytes l
-- Create relocation map
relocMap <- dynamicRelocationMap hdr ph contents
let ph = Elf.allPhdrs l
let contents = elfLayoutBytes l
-- Create relocation map
relocMap <- dynamicRelocationMap hdr ph contents
let intervals :: ElfFileSectionMap (ElfWordType w)
intervals = IMap.fromList
let intervals :: ElfFileSectionMap (ElfWordType w)
intervals = IMap.fromList
[ (IntervalCO start end, sec)
| shdr <- Map.elems (l ^. Elf.shdrs)
, let start = shdr^._3
, let sec = shdr^._1
, let end = start + elfSectionFileSize sec
]
mapM_ (insertElfSegment regIndex addrOff intervals contents relocMap)
(filter (\p -> Elf.phdrSegmentType p == Elf.PT_LOAD) ph)
mapM_ (insertElfSegment regIndex addrOff intervals contents relocMap)
(filter (\p -> Elf.phdrSegmentType p == Elf.PT_LOAD) ph)
------------------------------------------------------------------------
-- Elf section loading
@ -1008,8 +1011,8 @@ insertAllocatedSection :: Elf.ElfHeader w
insertAllocatedSection hdr symtab sectionMap regIdx nm = do
w <- uses mlsMemory memAddrWidth
reprConstraints w $ do
msec <- findSection sectionMap nm
case msec of
msec <- findSection sectionMap nm
case msec of
Nothing -> pure ()
Just sec -> do
mRelBuffer <- fmap (fmap (L.fromStrict . elfSectionData)) $

View File

@ -29,6 +29,7 @@ module Data.Macaw.Types
, Data.Parameterized.NatRepr.knownNat
) where
import qualified Data.Kind as Kind
import Data.Parameterized.Classes
import qualified Data.Parameterized.List as P
import Data.Parameterized.NatRepr
@ -251,7 +252,7 @@ instance OrdF FloatInfoRepr where
-- | A multi-parameter type class that allows one to represent that a
-- parameterized type value has some representative type such as a TypeRepr.
class HasRepr (f :: k -> *) (v :: k -> *) | f -> v where
class HasRepr (f :: k -> Kind.Type) (v :: k -> Kind.Type) | f -> v where
typeRepr :: f tp -> v tp
typeWidth :: HasRepr f TypeRepr => f (BVType w) -> NatRepr w