Remove redundant (?lc :: TypeContext) constraints on llvmTypeAsRepr e…

…t al. (#958)

Fixes #957.

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Expr.hs

@@ -204,8 +204,7 @@ pointerAsBitvectorExpr w ex =
 -- | Given a list of LLVMExpressions, "unpack" them into an assignment
 --   of crucible expressions.
 unpackArgs :: forall s a arch
-    . (?lc :: TypeContext
-      ,?err :: String -> a
+    . (?err :: String -> a
       ,HasPtrWidth (ArchWidth arch)
       )
    => [LLVMExpr s arch]
@@ -221,7 +220,7 @@ unpackArgs = go Ctx.Empty Ctx.Empty
        go ctx asgn (v:vs) k = unpackOne v (\_ tyr ex -> go (ctx :> tyr) (asgn :> ex) vs k)
 
 unpackOne
-   :: (?lc :: TypeContext, ?err :: String -> a, HasPtrWidth (ArchWidth arch))
+   :: (?err :: String -> a, HasPtrWidth (ArchWidth arch))
    => LLVMExpr s arch
    -> (forall tpr. Proxy# arch -> TypeRepr tpr -> Expr LLVM s tpr -> a)
    -> a
@@ -235,7 +234,7 @@ unpackOne (VecExpr tp vs) k =
   llvmTypeAsRepr tp $ \tpr -> unpackVec proxy# tpr (toList vs) $ k proxy# (VectorRepr tpr)
 
 unpackVec :: forall tpr s arch a
-    . (?lc :: TypeContext, ?err :: String -> a
+    . ( ?err :: String -> a
       , HasPtrWidth (ArchWidth arch)
       )
    => Proxy# arch
@@ -251,7 +250,7 @@ unpackVec _archProxy tpr = go [] . reverse
                              Just Refl -> go (v:vs) xs k
                              Nothing -> ?err $ unwords ["type mismatch in array value", show tpr, show tpr']
 
-zeroExpand :: (?lc :: TypeContext, ?err :: String -> a, HasPtrWidth (ArchWidth arch))
+zeroExpand :: (?err :: String -> a, HasPtrWidth (ArchWidth arch))
            => Proxy# arch
            -> MemType
            -> (forall tp. Proxy# arch -> TypeRepr tp -> Expr LLVM s tp -> a)
@@ -278,7 +277,7 @@ zeroExpand proxyArch DoubleType  k  = k proxyArch (FloatRepr DoubleFloatRepr) (A
 zeroExpand _prxyArch X86_FP80Type _ = ?err "Cannot zero expand x86_fp80 values"
 zeroExpand _prxyArch MetadataType _ = ?err "Cannot zero expand metadata"
 
-undefExpand :: (?lc :: TypeContext, ?err :: String -> a
+undefExpand :: ( ?err :: String -> a
                , HasPtrWidth (ArchWidth arch)
                )
             => Proxy# arch

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Monad.hs

@@ -236,7 +236,7 @@ initialState d llvmctx args asgn warnRef =
 --
 --   This procedure is used to set up the initial state of the
 --   registers at the entry point of a function.
-packType :: (?lc :: TypeContext, HasPtrWidth wptr)
+packType :: HasPtrWidth wptr
          => MemType
          -> CtxRepr ctx
          -> Ctx.Assignment (Atom s) ctx

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Types.hs

@@ -103,7 +103,7 @@ allModuleDeclares m = L.modDeclares m ++ def_decls
 -- | Translate a list of LLVM expressions into a crucible type context,
 --   which is passed into the given continuation.
 llvmTypesAsCtx :: forall a wptr
-                . (?lc :: TypeContext, HasPtrWidth wptr)
+                . HasPtrWidth wptr
                => [MemType]
                -> (forall ctx. CtxRepr ctx -> a)
                -> a
@@ -115,7 +115,7 @@ llvmTypesAsCtx xs f = go (concatMap (toList . llvmTypeToRepr) xs) Ctx.empty
 -- | Translate an LLVM type into a crucible type, which is passed into
 --   the given continuation
 llvmTypeAsRepr :: forall a wptr
-                . (?lc :: TypeContext, HasPtrWidth wptr)
+                . HasPtrWidth wptr
                => MemType
                -> (forall tp. TypeRepr tp -> a)
                -> a
@@ -127,15 +127,15 @@ llvmTypeAsRepr xs f = go (llvmTypeToRepr xs)
 -- | Translate an LLVM return type into a crucible type, which is passed into
 --   the given continuation
 llvmRetTypeAsRepr :: forall a wptr
-                   . (?lc :: TypeContext, HasPtrWidth wptr)
+                   . HasPtrWidth wptr
                   => Maybe MemType
                   -> (forall tp. TypeRepr tp -> a)
                   -> a
 llvmRetTypeAsRepr Nothing   f = f UnitRepr
 llvmRetTypeAsRepr (Just tp) f = llvmTypeAsRepr tp f
 
 -- | Actually perform the type translation
-llvmTypeToRepr :: (HasPtrWidth wptr, ?lc :: TypeContext) => MemType -> Maybe (Some TypeRepr)
+llvmTypeToRepr :: HasPtrWidth wptr => MemType -> Maybe (Some TypeRepr)
 llvmTypeToRepr (ArrayType _ tp)  = Just $ llvmTypeAsRepr tp (\t -> Some (VectorRepr t))
 llvmTypeToRepr (VecType _ tp)    = Just $ llvmTypeAsRepr tp (\t-> Some (VectorRepr t))
 llvmTypeToRepr (StructType si)   = Just $ llvmTypesAsCtx tps (\ts -> Some (StructRepr ts))
@@ -154,7 +154,7 @@ llvmTypeToRepr (IntType n) =
 -- | Compute the function Crucible function signature
 --   that corresponds to the given LLVM function declaration.
 llvmDeclToFunHandleRepr
-   :: (?lc :: TypeContext, HasPtrWidth wptr)
+   :: HasPtrWidth wptr
    => FunDecl
    -> (forall args ret. CtxRepr args -> TypeRepr ret -> a)
    -> a